From 913ef6832f7f2b7f9ff8c2bc0009f5caec17ab82 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias <emilio@lean-fro.org>
Date: Wed, 28 Jan 2026 23:08:45 +0100
Subject: [PATCH 1/2] chore: Test for behavior on infoview for math elements

This shows strange behavior when clicking on display math elements.
---
 .../test-cases/infoview_verso.lean            | 27 +++++++++++++++++++
 .../infoview_verso.lean.expected.out          | 18 +++++++++++++
 2 files changed, 45 insertions(+)
 create mode 100644 src/tests/interactive/test-cases/infoview_verso.lean
 create mode 100644 src/tests/interactive/test-cases/infoview_verso.lean.expected.out

diff --git a/src/tests/interactive/test-cases/infoview_verso.lean b/src/tests/interactive/test-cases/infoview_verso.lean
new file mode 100644
index 00000000..cea11c2f
--- /dev/null
+++ b/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
+`
diff --git a/src/tests/interactive/test-cases/infoview_verso.lean.expected.out b/src/tests/interactive/test-cases/infoview_verso.lean.expected.out
new file mode 100644
index 00000000..6617d2e2
--- /dev/null
+++ b/src/tests/interactive/test-cases/infoview_verso.lean.expected.out
@@ -0,0 +1,18 @@
+{"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}}
+{"range":
+ {"start": {"line": 23, "character": 3}, "end": {"line": 26, "character": 0}},
+ "goal": "docReconstInBlock✝ : Verso.Doc.DocReconstruction\n⊢ String"}

From 34ae2d8ea022595369397f3b4372404d4de55fe7 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias <emilio@lean-fro.org>
Date: Thu, 5 Feb 2026 20:00:40 +0100
Subject: [PATCH 2/2] fix: Don't include syntax information in elaboration of
 math elements

This avoids spurious infoview display of the internal elaborated
constant type.

This bug is only observable after applying the fix in #700 ; will wait
for #700 and #699 to merge this so we can properly provide a test.

Co-authored-by: David Thrane Christiansen <david@lean-fro.org>
---
 .../interactive/test-cases/infoview_verso.lean.expected.out   | 4 +---
 src/verso/Verso/Doc/Elab.lean                                 | 4 ++--
 2 files changed, 3 insertions(+), 5 deletions(-)

diff --git a/src/tests/interactive/test-cases/infoview_verso.lean.expected.out b/src/tests/interactive/test-cases/infoview_verso.lean.expected.out
index 6617d2e2..18995cc3 100644
--- a/src/tests/interactive/test-cases/infoview_verso.lean.expected.out
+++ b/src/tests/interactive/test-cases/infoview_verso.lean.expected.out
@@ -13,6 +13,4 @@ null
 {"textDocument":
  {"uri": "file:///src/tests/interactive/test-cases/infoview_verso.lean"},
  "position": {"line": 24, "character": 8}}
-{"range":
- {"start": {"line": 23, "character": 3}, "end": {"line": 26, "character": 0}},
- "goal": "docReconstInBlock✝ : Verso.Doc.DocReconstruction\n⊢ String"}
+null
diff --git a/src/verso/Verso/Doc/Elab.lean b/src/verso/Verso/Doc/Elab.lean
index 0313aa2e..a4281c99 100644
--- a/src/verso/Verso/Doc/Elab.lean
+++ b/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