From 9b7fcd28a4453bf1c948a6c22faee3657e485872 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Thu, 26 Feb 2026 19:57:59 +0100 Subject: [PATCH 1/2] fix: improve syntax precision for start of #doc blocks As of today, we used a synthetic placeholder for title syntax. This confused the LSP extension as it overgeralized the start of the span, which after the TOC-merge phase made the entry to appear as the parents of all other entries, for example existing declarations. --- doc/UsersGuide/Releases/v4_29_0_rc2.lean | 1 + .../folding_verso.lean.expected.out | 4 +-- .../interactive/test-cases/symbols_verso.lean | 18 ++++++++++++ .../symbols_verso.lean.expected.out | 28 +++++++++++++++++++ src/verso/Verso/Doc/Concrete.lean | 6 ++-- 5 files changed, 52 insertions(+), 5 deletions(-) create mode 100644 src/tests/interactive/test-cases/symbols_verso.lean create mode 100644 src/tests/interactive/test-cases/symbols_verso.lean.expected.out diff --git a/doc/UsersGuide/Releases/v4_29_0_rc2.lean b/doc/UsersGuide/Releases/v4_29_0_rc2.lean index 56e2eca3..c2723b46 100644 --- a/doc/UsersGuide/Releases/v4_29_0_rc2.lean +++ b/doc/UsersGuide/Releases/v4_29_0_rc2.lean @@ -18,3 +18,4 @@ file := "v4.29.0-rc2" %%% * [fix: Verso folding ranges / TOC for Lean.Doc syntax and #doc](https://github.com/leanprover/verso/pull/768) +* fix: preserve incremental `#doc` command source range for LSP TOC/folding diff --git a/src/tests/interactive/test-cases/folding_verso.lean.expected.out b/src/tests/interactive/test-cases/folding_verso.lean.expected.out index 55960bf5..35646f20 100644 --- a/src/tests/interactive/test-cases/folding_verso.lean.expected.out +++ b/src/tests/interactive/test-cases/folding_verso.lean.expected.out @@ -12,7 +12,7 @@ "position": {"line": 29, "character": 2}} [{"startLine": 0, "endLine": 28}, {"startLine": 20, "endLine": 28}, - {"startLine": 0, "endLine": 42}, + {"startLine": 32, "endLine": 42}, {"startLine": 33, "endLine": 42}, {"startLine": 11, "endLine": 13}, {"startLine": 26, "endLine": 28}, @@ -32,7 +32,7 @@ "position": {"line": 41, "character": 2}} [{"startLine": 0, "endLine": 28}, {"startLine": 20, "endLine": 28}, - {"startLine": 0, "endLine": 42}, + {"startLine": 32, "endLine": 42}, {"startLine": 33, "endLine": 42}, {"startLine": 11, "endLine": 13}, {"startLine": 26, "endLine": 28}, diff --git a/src/tests/interactive/test-cases/symbols_verso.lean b/src/tests/interactive/test-cases/symbols_verso.lean new file mode 100644 index 00000000..32986bca --- /dev/null +++ b/src/tests/interactive/test-cases/symbols_verso.lean @@ -0,0 +1,18 @@ +import Verso +import VersoManual + +set_option doc.verso true + +open Verso Genre Manual InlineLean + +#docs (Manual) docsSym "Docs heading" := +::::::: +# Docs heading +Text +::::::: +--^ textDocument/documentSymbol + +#doc (Manual) "Doc heading" => +# Doc heading +Text +--^ textDocument/documentSymbol diff --git a/src/tests/interactive/test-cases/symbols_verso.lean.expected.out b/src/tests/interactive/test-cases/symbols_verso.lean.expected.out new file mode 100644 index 00000000..c79de538 --- /dev/null +++ b/src/tests/interactive/test-cases/symbols_verso.lean.expected.out @@ -0,0 +1,28 @@ +{"textDocument": + {"uri": "file:///src/tests/interactive/test-cases/symbols_verso.lean"}, + "position": {"line": 11, "character": 2}} +[] +{"textDocument": + {"uri": "file:///src/tests/interactive/test-cases/symbols_verso.lean"}, + "position": {"line": 16, "character": 2}} +[{"selectionRange": + {"start": {"line": 0, "character": 0}, "end": {"line": 0, "character": 12}}, + "range": + {"start": {"line": 0, "character": 0}, "end": {"line": 11, "character": 0}}, + "name": "Docs heading", + "kind": 15}, + {"selectionRange": + {"start": {"line": 14, "character": 0}, "end": {"line": 14, "character": 30}}, + "range": + {"start": {"line": 14, "character": 0}, "end": {"line": 18, "character": 0}}, + "name": "Doc heading", + "kind": 15, + "children": + [{"selectionRange": + {"start": {"line": 15, "character": 0}, + "end": {"line": 15, "character": 13}}, + "range": + {"start": {"line": 15, "character": 0}, + "end": {"line": 18, "character": 0}}, + "name": "Doc heading", + "kind": 15}]}] diff --git a/src/verso/Verso/Doc/Concrete.lean b/src/verso/Verso/Doc/Concrete.lean index 7fc944ec..b0d97e70 100644 --- a/src/verso/Verso/Doc/Concrete.lean +++ b/src/verso/Verso/Doc/Concrete.lean @@ -322,13 +322,13 @@ 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 Unit := do +private meta def startDoc (docStx : Syntax) (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) + let initPartState : PartElabM.State := .init docStx modifyEnv (docEnvironmentExt.setState · ⟨genreSyntax, ctx, initDocState, initPartState⟩) runPartElabInEnv <| do @@ -361,7 +361,7 @@ elab_rules : command | `(command|#doc ( $genreSyntax:term ) $title:str =>%$tok) => open Lean Parser Elab Command in do elabCommand <| ← `(open scoped Lean.Doc.Syntax) - startDoc genreSyntax title + startDoc (← getRef) genreSyntax title -- Sets up basic incremental evaluation of documents by replacing Lean's command-by-command parser -- with a top-level-block parser. From ae34aa9d5a7c6f65642f0c5de5f1b574574abfdc Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Thu, 26 Feb 2026 23:49:52 +0100 Subject: [PATCH 2/2] fix: preserve #docs syntax range and expand LSP regressions --- .../interactive/test-cases/folding_verso.lean | 27 ++++- .../folding_verso.lean.expected.out | 103 ++++++++++++------ .../interactive/test-cases/symbols_verso.lean | 30 ++++- .../symbols_verso.lean.expected.out | 49 ++++++--- src/verso/Verso/Doc/Concrete.lean | 13 ++- 5 files changed, 157 insertions(+), 65 deletions(-) diff --git a/src/tests/interactive/test-cases/folding_verso.lean b/src/tests/interactive/test-cases/folding_verso.lean index f23db678..4298a8d0 100644 --- a/src/tests/interactive/test-cases/folding_verso.lean +++ b/src/tests/interactive/test-cases/folding_verso.lean @@ -16,10 +16,13 @@ def ds : Nat := 0 --^ textDocument/foldingRange -#docs (Manual) docsFold "Docs heading" := +#docs (Manual) docsFoldOne "Docs heading one" := ::::::: -# Docs heading -Text +# Docs heading one +Text one + +## Docs subheading one +More text one * one * two @@ -30,14 +33,30 @@ Text ::::::: --^ textDocument/foldingRange +#docs (Manual) docsFoldTwo "Docs heading two" := +::::::: +# Docs heading two +Text two + +## Docs subheading two +More text two + +* three +* four +::::::: +--^ textDocument/foldingRange + #doc (Manual) "Doc heading" => # Doc heading Text and text +## Doc subheading +More text + * one * two +--^ textDocument/foldingRange ```lean #check Nat.succ ``` ---^ textDocument/foldingRange diff --git a/src/tests/interactive/test-cases/folding_verso.lean.expected.out b/src/tests/interactive/test-cases/folding_verso.lean.expected.out index 35646f20..762175c0 100644 --- a/src/tests/interactive/test-cases/folding_verso.lean.expected.out +++ b/src/tests/interactive/test-cases/folding_verso.lean.expected.out @@ -4,46 +4,87 @@ [{"startLine": 0, "kind": "imports", "endLine": 1}, {"startLine": 7, "kind": "comment", "endLine": 13}, {"startLine": 14, "kind": "region", "endLine": 15}, - {"startLine": 18, "kind": "region", "endLine": 29}, - {"startLine": 39, "kind": "region", "endLine": 41}, - {"startLine": 42, "kind": "region", "endLine": 43}] + {"startLine": 18, "kind": "region", "endLine": 32}, + {"startLine": 35, "kind": "region", "endLine": 45}, + {"startLine": 59, "kind": "region", "endLine": 61}] {"textDocument": {"uri": "file:///src/tests/interactive/test-cases/folding_verso.lean"}, - "position": {"line": 29, "character": 2}} -[{"startLine": 0, "endLine": 28}, - {"startLine": 20, "endLine": 28}, - {"startLine": 32, "endLine": 42}, - {"startLine": 33, "endLine": 42}, + "position": {"line": 32, "character": 2}} +[{"startLine": 18, "endLine": 31}, + {"startLine": 20, "endLine": 31}, + {"startLine": 23, "endLine": 31}, + {"startLine": 35, "endLine": 44}, + {"startLine": 37, "endLine": 44}, + {"startLine": 40, "endLine": 44}, + {"startLine": 48, "endLine": 61}, + {"startLine": 49, "endLine": 61}, + {"startLine": 52, "endLine": 61}, {"startLine": 11, "endLine": 13}, - {"startLine": 26, "endLine": 28}, - {"startLine": 39, "endLine": 41}, - {"startLine": 23, "endLine": 24}, - {"startLine": 23, "endLine": 24}, - {"startLine": 36, "endLine": 37}, - {"startLine": 36, "endLine": 37}, + {"startLine": 29, "endLine": 31}, + {"startLine": 59, "endLine": 61}, + {"startLine": 26, "endLine": 27}, + {"startLine": 26, "endLine": 27}, + {"startLine": 43, "endLine": 44}, + {"startLine": 43, "endLine": 44}, + {"startLine": 55, "endLine": 57}, + {"startLine": 55, "endLine": 57}, {"startLine": 0, "kind": "imports", "endLine": 1}, {"startLine": 7, "kind": "comment", "endLine": 13}, {"startLine": 14, "kind": "region", "endLine": 15}, - {"startLine": 18, "kind": "region", "endLine": 29}, - {"startLine": 39, "kind": "region", "endLine": 41}, - {"startLine": 42, "kind": "region", "endLine": 43}] + {"startLine": 18, "kind": "region", "endLine": 32}, + {"startLine": 35, "kind": "region", "endLine": 45}, + {"startLine": 59, "kind": "region", "endLine": 61}] {"textDocument": {"uri": "file:///src/tests/interactive/test-cases/folding_verso.lean"}, - "position": {"line": 41, "character": 2}} -[{"startLine": 0, "endLine": 28}, - {"startLine": 20, "endLine": 28}, - {"startLine": 32, "endLine": 42}, - {"startLine": 33, "endLine": 42}, + "position": {"line": 45, "character": 2}} +[{"startLine": 18, "endLine": 31}, + {"startLine": 20, "endLine": 31}, + {"startLine": 23, "endLine": 31}, + {"startLine": 35, "endLine": 44}, + {"startLine": 37, "endLine": 44}, + {"startLine": 40, "endLine": 44}, + {"startLine": 48, "endLine": 61}, + {"startLine": 49, "endLine": 61}, + {"startLine": 52, "endLine": 61}, {"startLine": 11, "endLine": 13}, - {"startLine": 26, "endLine": 28}, - {"startLine": 39, "endLine": 41}, - {"startLine": 23, "endLine": 24}, - {"startLine": 23, "endLine": 24}, - {"startLine": 36, "endLine": 37}, - {"startLine": 36, "endLine": 37}, + {"startLine": 29, "endLine": 31}, + {"startLine": 59, "endLine": 61}, + {"startLine": 26, "endLine": 27}, + {"startLine": 26, "endLine": 27}, + {"startLine": 43, "endLine": 44}, + {"startLine": 43, "endLine": 44}, + {"startLine": 55, "endLine": 57}, + {"startLine": 55, "endLine": 57}, {"startLine": 0, "kind": "imports", "endLine": 1}, {"startLine": 7, "kind": "comment", "endLine": 13}, {"startLine": 14, "kind": "region", "endLine": 15}, - {"startLine": 18, "kind": "region", "endLine": 29}, - {"startLine": 39, "kind": "region", "endLine": 41}, - {"startLine": 42, "kind": "region", "endLine": 43}] + {"startLine": 18, "kind": "region", "endLine": 32}, + {"startLine": 35, "kind": "region", "endLine": 45}, + {"startLine": 59, "kind": "region", "endLine": 61}] +{"textDocument": + {"uri": "file:///src/tests/interactive/test-cases/folding_verso.lean"}, + "position": {"line": 56, "character": 2}} +[{"startLine": 18, "endLine": 31}, + {"startLine": 20, "endLine": 31}, + {"startLine": 23, "endLine": 31}, + {"startLine": 35, "endLine": 44}, + {"startLine": 37, "endLine": 44}, + {"startLine": 40, "endLine": 44}, + {"startLine": 48, "endLine": 61}, + {"startLine": 49, "endLine": 61}, + {"startLine": 52, "endLine": 61}, + {"startLine": 11, "endLine": 13}, + {"startLine": 29, "endLine": 31}, + {"startLine": 59, "endLine": 61}, + {"startLine": 26, "endLine": 27}, + {"startLine": 26, "endLine": 27}, + {"startLine": 43, "endLine": 44}, + {"startLine": 43, "endLine": 44}, + {"startLine": 55, "endLine": 57}, + {"startLine": 55, "endLine": 57}, + {"startLine": 0, "kind": "imports", "endLine": 1}, + {"startLine": 7, "kind": "comment", "endLine": 13}, + {"startLine": 14, "kind": "region", "endLine": 15}, + {"startLine": 18, "kind": "region", "endLine": 32}, + {"startLine": 35, "kind": "region", "endLine": 45}, + {"startLine": 59, "kind": "region", "endLine": 61}] diff --git a/src/tests/interactive/test-cases/symbols_verso.lean b/src/tests/interactive/test-cases/symbols_verso.lean index 32986bca..4a18b132 100644 --- a/src/tests/interactive/test-cases/symbols_verso.lean +++ b/src/tests/interactive/test-cases/symbols_verso.lean @@ -5,14 +5,32 @@ set_option doc.verso true open Verso Genre Manual InlineLean -#docs (Manual) docsSym "Docs heading" := +#docs (Manual) docsSymOne "Docs heading one" := ::::::: -# Docs heading -Text +# Docs heading one +Text one + +## Docs subheading one +More text one ::::::: --^ textDocument/documentSymbol -#doc (Manual) "Doc heading" => -# Doc heading -Text +#docs (Manual) docsSymTwo "Docs heading two" := +::::::: +# Docs heading two +Text two + +## Docs subheading two +More text two +::::::: + +#docs (Manual) docsSymThree "Docs heading three" := +::::::: +# Docs heading three +Text three + +## Docs subheading three +More text three +::::::: +--^ textDocument/foldingRange --^ textDocument/documentSymbol diff --git a/src/tests/interactive/test-cases/symbols_verso.lean.expected.out b/src/tests/interactive/test-cases/symbols_verso.lean.expected.out index c79de538..03befaa7 100644 --- a/src/tests/interactive/test-cases/symbols_verso.lean.expected.out +++ b/src/tests/interactive/test-cases/symbols_verso.lean.expected.out @@ -1,28 +1,41 @@ {"textDocument": {"uri": "file:///src/tests/interactive/test-cases/symbols_verso.lean"}, - "position": {"line": 11, "character": 2}} + "position": {"line": 14, "character": 2}} [] {"textDocument": {"uri": "file:///src/tests/interactive/test-cases/symbols_verso.lean"}, - "position": {"line": 16, "character": 2}} + "position": {"line": 33, "character": 2}} +[{"startLine": 7, "endLine": 13}, + {"startLine": 9, "endLine": 13}, + {"startLine": 12, "endLine": 13}, + {"startLine": 17, "endLine": 23}, + {"startLine": 19, "endLine": 23}, + {"startLine": 22, "endLine": 23}, + {"startLine": 26, "endLine": 32}, + {"startLine": 28, "endLine": 32}, + {"startLine": 31, "endLine": 32}, + {"startLine": 0, "kind": "imports", "endLine": 1}, + {"startLine": 7, "kind": "region", "endLine": 14}, + {"startLine": 17, "kind": "region", "endLine": 24}, + {"startLine": 26, "kind": "region", "endLine": 33}] +{"textDocument": + {"uri": "file:///src/tests/interactive/test-cases/symbols_verso.lean"}, + "position": {"line": 33, "character": 2}} [{"selectionRange": - {"start": {"line": 0, "character": 0}, "end": {"line": 0, "character": 12}}, + {"start": {"line": 7, "character": 0}, "end": {"line": 14, "character": 7}}, + "range": + {"start": {"line": 7, "character": 0}, "end": {"line": 14, "character": 0}}, + "name": "Docs heading one", + "kind": 15}, + {"selectionRange": + {"start": {"line": 17, "character": 0}, "end": {"line": 24, "character": 7}}, "range": - {"start": {"line": 0, "character": 0}, "end": {"line": 11, "character": 0}}, - "name": "Docs heading", + {"start": {"line": 17, "character": 0}, "end": {"line": 24, "character": 0}}, + "name": "Docs heading two", "kind": 15}, {"selectionRange": - {"start": {"line": 14, "character": 0}, "end": {"line": 14, "character": 30}}, + {"start": {"line": 26, "character": 0}, "end": {"line": 33, "character": 7}}, "range": - {"start": {"line": 14, "character": 0}, "end": {"line": 18, "character": 0}}, - "name": "Doc heading", - "kind": 15, - "children": - [{"selectionRange": - {"start": {"line": 15, "character": 0}, - "end": {"line": 15, "character": 13}}, - "range": - {"start": {"line": 15, "character": 0}, - "end": {"line": 18, "character": 0}}, - "name": "Doc heading", - "kind": 15}]}] + {"start": {"line": 26, "character": 0}, "end": {"line": 33, "character": 0}}, + "name": "Docs heading three", + "kind": 15}] diff --git a/src/verso/Verso/Doc/Concrete.lean b/src/verso/Verso/Doc/Concrete.lean index b0d97e70..fddd5e08 100644 --- a/src/verso/Verso/Doc/Concrete.lean +++ b/src/verso/Verso/Doc/Concrete.lean @@ -79,13 +79,13 @@ All-at-once elaboration of verso document syntax to syntax denoting a verso `Par elaboration of the `#docs` command and `#doc` term. The `#doc` command is incremental, and thus splits the logic in this function across multiple functions. -/ -private meta def elabDoc (genre: Term) (title: StrLit) (topLevelBlocks : Array Syntax) (endPos: String.Pos.Raw) : TermElabM Term := do +private meta def elabDoc (rootStx : Syntax) (genre: Term) (title: StrLit) (topLevelBlocks : Array Syntax) (endPos: String.Pos.Raw) : TermElabM Term := do let env ← getEnv let titleParts ← stringToInlines title let titleString := inlinesToString env titleParts let ctx ← DocElabContext.fromGenreTerm genre let initDocState : DocElabM.State := { highlightDeduplicationTable := .some {} } - let initPartState : PartElabM.State := .init (.node .none nullKind titleParts) + let initPartState : PartElabM.State := .init rootStx let ((), docElabState, partElabState) ← PartElabM.run ctx initDocState initPartState <| do @@ -118,7 +118,8 @@ elab "#docs" "(" genre:term ")" n:ident title:str ":=" ":::::::" text:document " | some x => x | none => panic! "No final token!" | _ => panic! "Nothing" - let doc ← Command.runTermElabM fun _ => elabDoc genre title text.raw.getArgs endTok.getPos! + let rootStx ← getRef + let doc ← Command.runTermElabM fun _ => elabDoc rootStx genre title text.raw.getArgs endTok.getPos! Command.elabCommand (← `(def $n : VersoDoc $genre := $doc)) public syntax docTermBody := @@ -147,17 +148,17 @@ elab_rules : term if let some g := genre then findGenreTm g.raw pure g - else + else `((_ : Genre)) let endPos := body.raw.getTailPos? |>.getD (← getFileMap).source.rawEndPos - let docu ← elabDoc genre title body.raw[0][1].getArgs endPos + let docu ← elabDoc (← getRef) genre title body.raw[0][1].getArgs endPos Term.elabTerm (← ``( ($(docu) : VersoDoc $genre))) none elab "#doc" "(" genre:term ")" title:str "=>" text:completeDocument eoi : term => do findGenreTm genre let endPos := (← getFileMap).source.rawEndPos - let doc ← elabDoc genre title text.raw.getArgs endPos + let doc ← elabDoc (← getRef) genre title text.raw.getArgs endPos Term.elabTerm (← `( ($(doc) : Part $genre))) none