fix: Don't include syntax information in elaboration of math elements

src/tests/interactive/test-cases/infoview_verso.lean

@@ -0,0 +1,27 @@
+import Verso
+import VersoManual
+
+set_option doc.verso true
+
+/-- This shows $`\forall n, n = n`
+               --^ $/lean/plainTermGoal
+-/
+theorem test0 : ∀ (n : Nat), n = n := by
+  intros
+  rfl
+
+open Verso.Genre
+
+-- Can we avoid using the Manual Genre here?
+#doc (Manual) "Test for verso math elaboration" =>
+
+This is a standard paragraph, see some *inline* text decorations.
+                                      --^ $/lean/plainTermGoal
+
+Our previous theorem showed $`\forall n, n = n`, which is equivalent to
+                            --^ $/lean/plainTermGoal
+
+$$`
+\forall n, n = n
+      --^ $/lean/plainTermGoal
+`

src/tests/interactive/test-cases/infoview_verso.lean.expected.out

@@ -0,0 +1,16 @@
+{"textDocument":
+ {"uri": "file:///src/tests/interactive/test-cases/infoview_verso.lean"},
+ "position": {"line": 5, "character": 17}}
+null
+{"textDocument":
+ {"uri": "file:///src/tests/interactive/test-cases/infoview_verso.lean"},
+ "position": {"line": 17, "character": 40}}
+null
+{"textDocument":
+ {"uri": "file:///src/tests/interactive/test-cases/infoview_verso.lean"},
+ "position": {"line": 20, "character": 30}}
+null
+{"textDocument":
+ {"uri": "file:///src/tests/interactive/test-cases/infoview_verso.lean"},
+ "position": {"line": 24, "character": 8}}
+null

src/verso/Verso/Doc/Elab.lean

@@ -194,13 +194,13 @@ public meta def _root_.Lean.Doc.Syntax.code.expand : InlineExpander
 @[inline_expander Lean.Doc.Syntax.inline_math]
 public meta def _root_.Lean.Doc.Syntax.inline_math.expand : InlineExpander
   |  `(inline| \math code( $s )) =>
-    ``(Inline.math MathMode.inline $s)
+    ``(Inline.math MathMode.inline $(quote s.getString))
   | _ => throwUnsupportedSyntax
 
 @[inline_expander Lean.Doc.Syntax.display_math]
 public meta def _root_.Lean.Doc.Syntax.display_math.expand : InlineExpander
   |  `(inline| \displaymath code( $s )) =>
-    ``(Inline.math MathMode.display $s)
+    ``(Inline.math MathMode.display $(quote s.getString))
   | _ => throwUnsupportedSyntax