fix: create well-spanned syntax on verso blocks

doc/UsersGuide/Releases/v4_28_0.lean

@@ -17,4 +17,5 @@ tag := "release-v4.28.0"
 file := "v4.28.0"
 %%%
 
-* Add Release Notes / Changelog to Verso Users guide (@ejgallego, #708)
+* Add Release Notes / Changelog to Verso Users guide (@david-christiansen, @ejgallego, #708)
+* Fix infoview display for inline lean code (@david-christiansen, @ejgallego, #700)

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

@@ -8,11 +8,12 @@ open Verso.Genre Manual InlineLean
 ```lean
 theorem test : ∀ (n : Nat), n = n := by
   intros
-     --^ textDocument/completion
+    --^ textDocument/completion
   rfl
 
-def a : Nat := Nat.add 3 2
-                --^ textDocument/completion
+def a (x y z : Nat) : x + y + z = x + (y + z):=
+  Nat.add_assoc x y z
+           --^ textDocument/completion
 
 #print a
 ```

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

@@ -1,8 +1,25 @@
 {"textDocument":
  {"uri": "file:///src/tests/interactive/test-cases/completion_inline.lean"},
- "position": {"line": 9, "character": 7}}
+ "position": {"line": 9, "character": 6}}
 {"items": [], "isIncomplete": true}
 {"textDocument":
  {"uri": "file:///src/tests/interactive/test-cases/completion_inline.lean"},
- "position": {"line": 13, "character": 18}}
-{"items": [], "isIncomplete": true}
+ "position": {"line": 14, "character": 13}}
+{"items":
+ [{"label": "add_sub_assoc",
+   "kind": 23,
+   "data":
+   ["«external:file:///src/tests/interactive/test-cases/completion_inline.lean»",
+    14,
+    13,
+    0,
+    "cNat.add_sub_assoc"]},
+  {"label": "add_assoc",
+   "kind": 23,
+   "data":
+   ["«external:file:///src/tests/interactive/test-cases/completion_inline.lean»",
+    14,
+    13,
+    0,
+    "cNat.add_assoc"]}],
+ "isIncomplete": false}

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

@@ -19,4 +19,5 @@
 {"textDocument":
  {"uri": "file:///src/tests/interactive/test-cases/inline_goals.lean"},
  "position": {"line": 20, "character": 7}}
-null
+{"rendered": "```lean\nn✝ : Nat\n⊢ n✝ = n✝\n```",
+ "goals": ["n✝ : Nat\n⊢ n✝ = n✝"]}

src/verso/Verso/Doc/Concrete.lean

@@ -161,8 +161,8 @@ elab "#doc" "(" genre:term ")" title:str "=>" text:completeDocument eoi : term =
   Term.elabTerm (← `( ($(doc) : Part $genre))) none
 
 
-scoped syntax (name := addBlockCmd) block term:max : command
-scoped syntax (name := addLastBlockCmd) block term:max str : command
+scoped syntax (name := addBlockCmd) block : command
+scoped syntax (name := addLastBlockCmd) block : command
 
 /-!
 Unlike `#doc` expressions and `#docs` commands, which are elaborated all at once, `#doc` commands
@@ -246,7 +246,7 @@ private meta partial def getTailContext? (source : String) (stx : Syntax) : Opti
 Parses each top-level block as either an `addBlockCmd` or an `addLastBlockCmd`. (This is what
 Verso uses to replace the command parser.)
 -/
-private meta def versoBlockCommandFn (genre : Term) (title : String) : ParserFn := fun c s =>
+private meta def versoBlockCommandFn : ParserFn := fun c s =>
   let iniSz  := s.stackSize
   let lastPos? := lastVersoEndPosExt.getState c.env
   let s := lastPos? |>.map s.setPos |>.getD s
@@ -255,10 +255,8 @@ private meta def versoBlockCommandFn (genre : Term) (title : String) : ParserFn
   else
     let s := ignoreFn (manyFn blankLine) c s
     let s := updateTrailing c s
-    let s := s.pushSyntax genre
     let i := s.pos
     if c.atEnd i then
-      let s := s.pushSyntax (Syntax.mkStrLit title)
       s.mkNode ``addLastBlockCmd iniSz
     else
       s.mkNode ``addBlockCmd iniSz
@@ -281,6 +279,7 @@ be used to thread state between the separate top level blocks. These environment
 the state that needs to exist across top-level-block parsing events.
 -/
 public meta structure DocElabEnvironment where
+  genreSyntax : Term := ⟨.missing⟩
   ctx : DocElabContext := ⟨.missing, mkConst ``Unit, .always, .none⟩
   docState : DocElabM.State := { highlightDeduplicationTable := some {} }
   partState : PartElabM.State := .init (.node .none nullKind #[])
@@ -323,18 +322,17 @@ in `elabDoc` across three functions: the prelude in `startDoc`, the loop body in
 and the postlude in `finishDoc`.
 -/
 
-private meta def startDoc (genreSyntax : Term) (title: StrLit) : Command.CommandElabM String := do
+private meta def startDoc (genreSyntax : Term) (title: StrLit) : Command.CommandElabM Unit := do
   let env ← getEnv
   let titleParts ← stringToInlines title
   let titleString := inlinesToString env titleParts
   let ctx ← Command.runTermElabM fun _ => DocElabContext.fromGenreTerm genreSyntax
   let initDocState : DocElabM.State := { highlightDeduplicationTable := .some {} }
   let initPartState : PartElabM.State := .init (.node .none nullKind titleParts)
 
-  modifyEnv (docEnvironmentExt.setState · ⟨ctx, initDocState, initPartState⟩)
+  modifyEnv (docEnvironmentExt.setState · ⟨genreSyntax, ctx, initDocState, initPartState⟩)
   runPartElabInEnv <| do
     PartElabM.setTitle titleString (← titleParts.mapM (elabInline ⟨·⟩))
-  return titleString
 
 private meta def runVersoBlock (block : TSyntax `block) : Command.CommandElabM Unit := do
   runPartElabInEnv <| partCommand block
@@ -344,29 +342,30 @@ private meta def runVersoBlock (block : TSyntax `block) : Command.CommandElabM U
   saveRefsInEnv
 
 open PartElabM in
-private meta def finishDoc (genreSyntax : Term) (title : StrLit) : Command.CommandElabM Unit:= do
+private meta def finishDoc : Command.CommandElabM Unit:= do
   let endPos := (← getFileMap).source.rawEndPos
   runPartElabInEnv <| do closePartsUntil 0 endPos
 
   let versoEnv := docEnvironmentExt.getState (← getEnv)
   let finished := versoEnv.partState.partContext.toPartFrame.close endPos
 
-  let n := mkIdentFrom title (← currentDocName)
-  let doc ← Command.runTermElabM fun _ => finished.toVersoDoc genreSyntax versoEnv.ctx versoEnv.docState versoEnv.partState
-  let ty ← ``(VersoDoc $genreSyntax)
+  let n := mkIdent (← currentDocName)
+  let doc ← Command.runTermElabM fun _ => finished.toVersoDoc versoEnv.genreSyntax versoEnv.ctx versoEnv.docState versoEnv.partState
+
+  let ty ← ``(VersoDoc $versoEnv.genreSyntax)
   Command.elabCommand (← `(def $n : $ty := $doc))
 
 syntax (name := replaceDoc) "#doc " "(" term ") " str " =>" : command
 elab_rules : command
   | `(command|#doc ( $genreSyntax:term ) $title:str =>%$tok) => open Lean Parser Elab Command in do
   elabCommand <| ← `(open scoped Lean.Doc.Syntax)
 
-  let titleString ← startDoc genreSyntax title
+  startDoc genreSyntax title
 
   -- Sets up basic incremental evaluation of documents by replacing Lean's command-by-command parser
   -- with a top-level-block parser.
   modifyEnv fun env => originalCatParserExt.setState env (categoryParserFnExtension.getState env)
-  replaceCategoryParser `command (versoBlockCommandFn genreSyntax titleString)
+  replaceCategoryParser `command versoBlockCommandFn
 
   if let some stopPos := tok.getTailPos? then
     let txt ← getFileMap
@@ -387,7 +386,7 @@ elab_rules : command
     -- Edge case: if there's no blocks after the =>, the replacement command parser won't get called,
     -- so we detect that case and call finishDoc.
     if stopPos.extract txt.source txt.source.rawEndPos |>.all Char.isWhitespace then
-      finishDoc genreSyntax title
+      finishDoc
 
 open Command in
 /--
@@ -403,16 +402,16 @@ private meta def updatePos (b : TSyntax `block) : CommandElabM Unit := do
 
 @[command_elab addBlockCmd]
 public meta def elabVersoBlock : Command.CommandElab
-  | `(addBlockCmd| $b:block $_:term) => do
+  | `(addBlockCmd| $b:block) => do
     updatePos b
     runVersoBlock b
   | _ => throwUnsupportedSyntax
 
 @[command_elab addLastBlockCmd]
 public meta def elabVersoLastBlock : Command.CommandElab
-  | `(addLastBlockCmd| $b:block $genre:term $title:str) => do
+  | `(addLastBlockCmd| $b:block) => do
     updatePos b
     runVersoBlock b
     -- Finish up the document
-    finishDoc genre title
+    finishDoc
   | _ => throwUnsupportedSyntax