fix: remove old comment

LeanInk/Annotation/DataTypes.lean

@@ -21,8 +21,6 @@ namespace Compound
   def getFragments (self : Compound b) : List b := self.fragments.map (λ f => f.2)
 
   def empty { x : Type u } (headPos : String.Pos) : Compound x := { headPos := headPos, tailPos := none, fragments := [] }
-
-  -- def empty { x : Type u } (headPos : String.Pos) : Compound x := { headPos := headPos, tailPos := headPos, fragments := [] }
 end Compound
 
 instance {a : Type u} [ToString a] : ToString (Compound a) where

test/playground/playground_2.lean

@@ -0,0 +1,13 @@
+/-| 
+Hello World!
+-/
+#print "Hello World!"
+
+/-|
+A literate comment!
+-/
+
+theorem exampleTheorem (p q : Prop) (hp : p) (hq : q) : p ∧ q ∧ p := by
+  apply And.intro
+  . exact hp
+  . sorry

test/playground/playground_2.lean.leanInk.expected

@@ -0,0 +1 @@
+[{"contents":[{"typeinfo":null,"semanticType":null,"raw":"/-| \nHello World!\n-/\n","link":null,"docstring":null,"_type":"token"}],"_type":"text"},{"messages":[{"contents":"Hello World!","_type":"message"}],"goals":[],"contents":[{"typeinfo":null,"semanticType":"Keyword","raw":"#print","link":null,"docstring":null,"_type":"token"}],"_type":"sentence"},{"contents":[{"typeinfo":null,"semanticType":null,"raw":" \"Hello World!\"\n\n/-|\nA literate comment!\n-/\n\n","link":null,"docstring":null,"_type":"token"},{"typeinfo":null,"semanticType":"Keyword","raw":"theorem","link":null,"docstring":null,"_type":"token"},{"typeinfo":null,"semanticType":null,"raw":" ","link":null,"docstring":null,"_type":"token"},{"typeinfo":{"type":"∀ (p q : Prop), p → q → p ∧ q ∧ p","name":"exampleTheorem","_type":"typeinfo"},"semanticType":null,"raw":"exampleTheorem","link":null,"docstring":null,"_type":"token"},{"typeinfo":null,"semanticType":null,"raw":" (","link":null,"docstring":null,"_type":"token"},{"typeinfo":{"type":"Prop","name":"p","_type":"typeinfo"},"semanticType":"Name.Variable","raw":"p","link":null,"docstring":null,"_type":"token"},{"typeinfo":null,"semanticType":null,"raw":" ","link":null,"docstring":null,"_type":"token"},{"typeinfo":{"type":"Prop","name":"q","_type":"typeinfo"},"semanticType":"Name.Variable","raw":"q","link":null,"docstring":null,"_type":"token"},{"typeinfo":null,"semanticType":null,"raw":" : ","link":null,"docstring":null,"_type":"token"},{"typeinfo":{"type":"Type","name":"Prop","_type":"typeinfo"},"semanticType":null,"raw":"Prop","link":null,"docstring":null,"_type":"token"},{"typeinfo":null,"semanticType":null,"raw":") (","link":null,"docstring":null,"_type":"token"},{"typeinfo":{"type":"p","name":"hp","_type":"typeinfo"},"semanticType":"Name.Variable","raw":"hp","link":null,"docstring":null,"_type":"token"},{"typeinfo":null,"semanticType":null,"raw":" : ","link":null,"docstring":null,"_type":"token"},{"typeinfo":{"type":"Prop","name":"p","_type":"typeinfo"},"semanticType":"Name.Variable","raw":"p","link":null,"docstring":null,"_type":"token"},{"typeinfo":null,"semanticType":null,"raw":") (","link":null,"docstring":null,"_type":"token"},{"typeinfo":{"type":"q","name":"hq","_type":"typeinfo"},"semanticType":"Name.Variable","raw":"hq","link":null,"docstring":null,"_type":"token"},{"typeinfo":null,"semanticType":null,"raw":" : ","link":null,"docstring":null,"_type":"token"},{"typeinfo":{"type":"Prop","name":"q","_type":"typeinfo"},"semanticType":"Name.Variable","raw":"q","link":null,"docstring":null,"_type":"token"},{"typeinfo":null,"semanticType":null,"raw":") : ","link":null,"docstring":null,"_type":"token"},{"typeinfo":{"type":"Prop","name":"p","_type":"typeinfo"},"semanticType":"Name.Variable","raw":"p","link":null,"docstring":null,"_type":"token"},{"typeinfo":null,"semanticType":null,"raw":" ∧ ","link":null,"docstring":null,"_type":"token"},{"typeinfo":{"type":"Prop","name":"q","_type":"typeinfo"},"semanticType":"Name.Variable","raw":"q","link":null,"docstring":null,"_type":"token"},{"typeinfo":null,"semanticType":null,"raw":" ∧ ","link":null,"docstring":null,"_type":"token"},{"typeinfo":{"type":"Prop","name":"p","_type":"typeinfo"},"semanticType":"Name.Variable","raw":"p","link":null,"docstring":null,"_type":"token"},{"typeinfo":null,"semanticType":null,"raw":" := ","link":null,"docstring":null,"_type":"token"}],"_type":"text"},{"messages":[],"goals":[{"name":"","hypotheses":[{"type":"Prop","names":["p","q"],"body":"","_type":"hypothesis"},{"type":"p","names":["hp"],"body":"","_type":"hypothesis"},{"type":"q","names":["hq"],"body":"","_type":"hypothesis"}],"conclusion":"p ∧ q ∧ p","_type":"goal"}],"contents":[{"typeinfo":null,"semanticType":"Keyword","raw":"by","link":null,"docstring":null,"_type":"token"},{"typeinfo":null,"semanticType":null,"raw":"\n  ","link":null,"docstring":null,"_type":"token"}],"_type":"sentence"},{"messages":[],"goals":[{"name":"left","hypotheses":[{"type":"Prop","names":["p","q"],"body":"","_type":"hypothesis"},{"type":"p","names":["hp"],"body":"","_type":"hypothesis"},{"type":"q","names":["hq"],"body":"","_type":"hypothesis"}],"conclusion":"p","_type":"goal"},{"name":"right","hypotheses":[{"type":"Prop","names":["p","q"],"body":"","_type":"hypothesis"},{"type":"p","names":["hp"],"body":"","_type":"hypothesis"},{"type":"q","names":["hq"],"body":"","_type":"hypothesis"}],"conclusion":"q ∧ p","_type":"goal"}],"contents":[{"typeinfo":null,"semanticType":"Keyword","raw":"apply","link":null,"docstring":"`apply e` tries to match the current goal against the conclusion of `e`'s type.\nIf it succeeds, then the tactic returns as many subgoals as the number of premises that\nhave not been fixed by type inference or type class resolution.\nNon-dependent premises are added before dependent ones.\n\nThe `apply` tactic uses higher-order pattern matching, type class resolution, and first-order unification with dependent types.\n","_type":"token"},{"typeinfo":null,"semanticType":null,"raw":" ","link":null,"docstring":"`apply e` tries to match the current goal against the conclusion of `e`'s type.\nIf it succeeds, then the tactic returns as many subgoals as the number of premises that\nhave not been fixed by type inference or type class resolution.\nNon-dependent premises are added before dependent ones.\n\nThe `apply` tactic uses higher-order pattern matching, type class resolution, and first-order unification with dependent types.\n","_type":"token"},{"typeinfo":{"type":"∀ {a b : Prop}, a → b → a ∧ b","name":"And.intro","_type":"typeinfo"},"semanticType":null,"raw":"And.intro","link":null,"docstring":null,"_type":"token"}],"_type":"sentence"},{"messages":[],"goals":[{"name":"","hypotheses":[{"type":"Prop","names":["p","q"],"body":"","_type":"hypothesis"},{"type":"p","names":["hp"],"body":"","_type":"hypothesis"},{"type":"q","names":["hq"],"body":"","_type":"hypothesis"}],"conclusion":"p ∧ q ∧ p","_type":"goal"}],"contents":[{"typeinfo":null,"semanticType":null,"raw":"\n  ","link":null,"docstring":null,"_type":"token"}],"_type":"sentence"},{"messages":[],"goals":[{"name":"left","hypotheses":[{"type":"Prop","names":["p","q"],"body":"","_type":"hypothesis"},{"type":"p","names":["hp"],"body":"","_type":"hypothesis"},{"type":"q","names":["hq"],"body":"","_type":"hypothesis"}],"conclusion":"p","_type":"goal"}],"contents":[{"typeinfo":null,"semanticType":null,"raw":".","link":null,"docstring":"`· tac` focuses on the main goal and tries to solve it using `tac`, or else fails. ","_type":"token"}],"_type":"sentence"},{"messages":[],"goals":[{"name":"left","hypotheses":[{"type":"Prop","names":["p","q"],"body":"","_type":"hypothesis"},{"type":"p","names":["hp"],"body":"","_type":"hypothesis"},{"type":"q","names":["hq"],"body":"","_type":"hypothesis"}],"conclusion":"p","_type":"goal"},{"name":"right","hypotheses":[{"type":"Prop","names":["p","q"],"body":"","_type":"hypothesis"},{"type":"p","names":["hp"],"body":"","_type":"hypothesis"},{"type":"q","names":["hq"],"body":"","_type":"hypothesis"}],"conclusion":"q ∧ p","_type":"goal"}],"contents":[{"typeinfo":null,"semanticType":null,"raw":" ","link":null,"docstring":"`· tac` focuses on the main goal and tries to solve it using `tac`, or else fails. ","_type":"token"}],"_type":"sentence"},{"messages":[],"goals":[{"name":"","hypotheses":[],"conclusion":"Goals accomplished! 🐙","_type":"goal"}],"contents":[{"typeinfo":null,"semanticType":"Keyword","raw":"exact","link":null,"docstring":"`exact e` closes the main goal if its target type matches that of `e`.\n","_type":"token"},{"typeinfo":null,"semanticType":null,"raw":" ","link":null,"docstring":"`exact e` closes the main goal if its target type matches that of `e`.\n","_type":"token"},{"typeinfo":{"type":"p","name":"hp","_type":"typeinfo"},"semanticType":"Name.Variable","raw":"hp","link":null,"docstring":null,"_type":"token"}],"_type":"sentence"},{"messages":[],"goals":[{"name":"","hypotheses":[{"type":"Prop","names":["p","q"],"body":"","_type":"hypothesis"},{"type":"p","names":["hp"],"body":"","_type":"hypothesis"},{"type":"q","names":["hq"],"body":"","_type":"hypothesis"}],"conclusion":"p ∧ q ∧ p","_type":"goal"}],"contents":[{"typeinfo":null,"semanticType":null,"raw":"\n  ","link":null,"docstring":null,"_type":"token"}],"_type":"sentence"},{"messages":[],"goals":[{"name":"right","hypotheses":[{"type":"Prop","names":["p","q"],"body":"","_type":"hypothesis"},{"type":"p","names":["hp"],"body":"","_type":"hypothesis"},{"type":"q","names":["hq"],"body":"","_type":"hypothesis"}],"conclusion":"q ∧ p","_type":"goal"}],"contents":[{"typeinfo":null,"semanticType":null,"raw":".","link":null,"docstring":"`· tac` focuses on the main goal and tries to solve it using `tac`, or else fails. ","_type":"token"}],"_type":"sentence"},{"messages":[],"goals":[{"name":"right","hypotheses":[{"type":"Prop","names":["p","q"],"body":"","_type":"hypothesis"},{"type":"p","names":["hp"],"body":"","_type":"hypothesis"},{"type":"q","names":["hq"],"body":"","_type":"hypothesis"}],"conclusion":"q ∧ p","_type":"goal"}],"contents":[{"typeinfo":null,"semanticType":null,"raw":" ","link":null,"docstring":"`· tac` focuses on the main goal and tries to solve it using `tac`, or else fails. ","_type":"token"}],"_type":"sentence"},{"messages":[{"contents":"Warning: declaration uses 'sorry'","_type":"message"}],"goals":[{"name":"","hypotheses":[],"conclusion":"Goals accomplished! 🐙","_type":"goal"}],"contents":[{"typeinfo":null,"semanticType":"Keyword","raw":"sorry","link":null,"docstring":"The `sorry` tactic is a shorthand for `exact sorry`. ","_type":"token"}],"_type":"sentence"},{"contents":[],"_type":"text"}]