Skip to content

fix: improve syntax precision for start of #doc blocks #771

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
ejgallego wants to merge 2 commits into
base: main
Choose a base branch
from
Open

fix: improve syntax precision for start of #doc blocks #771

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
9b7fcd2
fix: improve syntax precision for start of #doc blocks
ejgallego Feb 26, 2026
ae34aa9
fix: preserve #docs syntax range and expand LSP regressions
ejgallego Feb 26, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
1 change: 1 addition & 0 deletions doc/UsersGuide/Releases/v4_29_0_rc2.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
27 changes: 23 additions & 4 deletions src/tests/interactive/test-cases/folding_verso.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -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
103 changes: 72 additions & 31 deletions src/tests/interactive/test-cases/folding_verso.lean.expected.out
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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": 0, "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": 0, "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}]
36 changes: 36 additions & 0 deletions src/tests/interactive/test-cases/symbols_verso.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,36 @@
import Verso
import VersoManual

set_option doc.verso true

open Verso Genre Manual InlineLean

#docs (Manual) docsSymOne "Docs heading one" :=
:::::::
# Docs heading one
Text one

## Docs subheading one
More text one
:::::::
--^ textDocument/documentSymbol
Copy link
Contributor Author

@ejgallego ejgallego Feb 26, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Not sure this call is worth the effort, I'll keep it as a witness of the non-incrementality of documentSymbol


#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
41 changes: 41 additions & 0 deletions src/tests/interactive/test-cases/symbols_verso.lean.expected.out
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,41 @@
{"textDocument":
{"uri": "file:///src/tests/interactive/test-cases/symbols_verso.lean"},
"position": {"line": 14, "character": 2}}
[]
{"textDocument":
{"uri": "file:///src/tests/interactive/test-cases/symbols_verso.lean"},
"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": 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": 17, "character": 0}, "end": {"line": 24, "character": 0}},
"name": "Docs heading two",
"kind": 15},
{"selectionRange":
{"start": {"line": 26, "character": 0}, "end": {"line": 33, "character": 7}},
"range":
{"start": {"line": 26, "character": 0}, "end": {"line": 33, "character": 0}},
Copy link
Contributor Author

@ejgallego ejgallego Feb 26, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

There is a violation of the LSP spec here, selectionRange must be contained in range.

Working on a fix.

Copy link
Collaborator

@david-christiansen david-christiansen Feb 27, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Seems like we should fix that. Do you plan to do that in this PR?

Copy link
Contributor Author

@ejgallego ejgallego Feb 27, 2026 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Yes, the fix turned out to be more involved than I wanted, due to header{} being a synthetic token, which actually made the headings not carry location and not appear on the outline view.

Copy link
Contributor Author

@ejgallego ejgallego Feb 27, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This is indeed a serious violation, so I'll add a panic for this problem. In this case the origin of the issue was a little typo in the code getPos vs getTailPos.

"name": "Docs heading three",
"kind": 15}]
19 changes: 10 additions & 9 deletions src/verso/Verso/Doc/Concrete.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Copy link
Collaborator

@david-christiansen david-christiansen Feb 27, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

The meaning of rootStx isn't particularly apparent to me when just reading here. How about explaining in the docstring that it's the syntax of the complete #doc ... => line?

Copy link
Collaborator

@david-christiansen david-christiansen Feb 27, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

We might also want to call it ref for consistency with Lean internals if you think that makes sense

Copy link
Collaborator

@david-christiansen david-christiansen Feb 27, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Or could we drop the parameter and just call getRef here?

Copy link
Contributor Author

@ejgallego ejgallego Feb 27, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I'll find a better name, I agree.

Let me look into using getRef, as of now, in working branch, I'm doing a little bit of surgery but I agree it'd be better if we could use getRef.

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
Expand Down Expand Up @@ -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 :=
Expand Down Expand Up @@ -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


Expand Down Expand Up @@ -322,13 +323,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
Expand Down Expand Up @@ -361,7 +362,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.
Expand Down