diff --git a/doc/UsersGuide/Releases/Entries.lean b/doc/UsersGuide/Releases/Entries.lean index 1607f8159..89919c2f9 100644 --- a/doc/UsersGuide/Releases/Entries.lean +++ b/doc/UsersGuide/Releases/Entries.lean @@ -18,6 +18,7 @@ public import UsersGuide.Releases.Entries.FoldingRanges public import UsersGuide.Releases.Entries.FullPageSearch public import UsersGuide.Releases.Entries.InlineLeanInfoview public import UsersGuide.Releases.Entries.LegacyInlineRoles +public import UsersGuide.Releases.Entries.LinkFootnoteResolution public import UsersGuide.Releases.Entries.LiterateHtmlKatex public import UsersGuide.Releases.Entries.LiterateProgramming public import UsersGuide.Releases.Entries.ManualMarginalia diff --git a/doc/UsersGuide/Releases/Entries/LinkFootnoteResolution.lean b/doc/UsersGuide/Releases/Entries/LinkFootnoteResolution.lean new file mode 100644 index 000000000..76f8bb78d --- /dev/null +++ b/doc/UsersGuide/Releases/Entries/LinkFootnoteResolution.lean @@ -0,0 +1,35 @@ +/- +Copyright (c) 2026 Lean FRO LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Author: David Thrane Christiansen +-/ +module + +public import UsersGuide.Releases.Entry + +open Verso.Genre Manual InlineLean UsersGuide.Releases + +release_note + version := ⟨4, 35, 0⟩ + breaking := true + tag := "link-footnote-resolution" + prs := [1014] + +#doc (Manual) "Link and Footnote Label Resolution" => + +Both footnotes and links with labels instead of URLs (e.g. `see [link][somewhere]`) are now internally resolved through Verso's document reconstruction data instead of by generating class instances for each label. +Go-to-definition and document highlights for labels now work before elaboration is complete. +Footnote contents can now use labels that are defined later. +This is a breaking change for code that defines or looks up labels: the type classes `HasLink` and `HasNote` are gone, {name}`Verso.Doc.DocReconstruction` takes the genre as a parameter, and several functions and fields are renamed or removed. + +This fixes issues with Lean files that contain multiple documents and improves error messages. +Furthermore, more roles now work inside footnotes. + +There are {ref "link-footnote-resolution"}[breaking changes]: + +* {name}`Verso.Doc.DocReconstruction` takes the genre as a parameter. +* {name}`Verso.Doc.Elab.DocRefInfo` describes a single definition or use. +* {name}`Verso.Doc.Elab.DocDef` has the required fields `fileName` and `position`. +* Removed: the type classes `HasLink` and `HasNote`, `DocRefInfo.syntax`, `Verso.Doc.Elab.internalRefs` and `Verso.Doc.Concrete.saveRefs`. +* Renamed to `labelStx`: the field `defSite` of {name}`Verso.Doc.Elab.DocDef`, and the `refName` parameter of {name}`Verso.Doc.Elab.PartElabM.addLinkDef`, {name}`Verso.Doc.Elab.DocElabM.addLinkRef`, {name}`Verso.Doc.Elab.PartElabM.addFootnoteDef` and {name}`Verso.Doc.Elab.DocElabM.addFootnoteRef`. +* {name}`Verso.Doc.Elab.DocElabM.addLinkRef` and {name}`Verso.Doc.Elab.DocElabM.addFootnoteRef` report an error for text elaborated outside a document, such as the title of a literate module in a manual. Before, they failed with an instance error. diff --git a/src/tests/VersoTests/Elab.lean b/src/tests/VersoTests/Elab.lean index 72af1873c..9a5202fd6 100644 --- a/src/tests/VersoTests/Elab.lean +++ b/src/tests/VersoTests/Elab.lean @@ -43,7 +43,7 @@ def totallyUndefined : RoleExpanderOf Unit /-- error: don't know how to synthesize placeholder for argument `head` context: -docReconstInBlock✝ : Doc.DocReconstruction +docReconstInBlock✝ : Doc.DocReconstruction Doc.Genre.none ⊢ Doc.Inline Doc.Genre.none -/ #test_msgs in diff --git a/src/tests/VersoTests/Refs.lean b/src/tests/VersoTests/Refs.lean index d6adce14f..a6c91e5af 100644 --- a/src/tests/VersoTests/Refs.lean +++ b/src/tests/VersoTests/Refs.lean @@ -8,6 +8,19 @@ import Verso namespace Verso.RefsTest set_option guard_msgs.diff true +/-! +These tests check link and footnote resolution in documents elaborated with `#docs`, which doesn't +do block-level incrementality. They also check the messages about undefined uses, unused +definitions and duplicate definitions. + +A use of a label resolves to the definition with that label in the same document. When Verso +finishes the document, it checks the links and footnotes. A use without a definition is an error, +and a definition without a use is a warning. + +Each test elaborates a small document. Some tests observe the messages and their order. Others +evaluate `toPart` and observe the URL or footnote contents that each use resolved to. +-/ + /- ----- -/ #docs (.none) regularLink "Regular link" := @@ -165,8 +178,15 @@ info: Verso.Doc.Part.mk #test_msgs in #eval refAndLinkRecursion.toPart +/- +A duplicate link definition error states where the first definition is. + +The document defines the link label `foo` twice. The error is at the second definition. It specifies +the label, the position of the first definition, and both URLs. +-/ + /-- -error: Already defined link [foo] as 'https://example.com' +error: Duplicate definition of link label [foo]. It is already defined at line 194, column 1, with the URL 'https://example.com'. This definition has the URL 'http://example.com'. -/ #test_msgs in #docs (.none) failDupLink "Fail" := @@ -177,8 +197,14 @@ error: Already defined link [foo] as 'https://example.com' [Go to foo][foo]! ::::::: +/- +A duplicate footnote definition error states where the first definition is. + +The document defines the footnote label `note` twice. The error is at the second definition. +-/ + /-- -error: Already defined footnote [^note] +error: Duplicate definition of footnote label [^note]. It is already defined at line 212, column 2. -/ #test_msgs in #docs (.none) failDupFoot "Fail" := @@ -190,37 +216,136 @@ error: Already defined footnote [^note] There are no caveats.[^note] ::::::: +/- +A footnote's contents may use a footnote that is defined later in the document. +-/ + +#docs (.none) footnoteUsesLaterFootnote "Later footnote" := +::::::: +A sentence with a footnote.[^foo] + +[^foo]: A footnote that uses a later one.[^bar] + +[^bar]: The later footnote. +::::::: + /-- -error: Footnote reference [^bar] does not have a definition +info: Verso.Doc.Part.mk + #[Verso.Doc.Inline.text "Later footnote"] + "Later footnote" + none + #[Verso.Doc.Block.para + #[Verso.Doc.Inline.text "A sentence with a footnote.", + Verso.Doc.Inline.footnote + "foo" + #[(Verso.Doc.Inline.text "A footnote that uses a later one."), + (Verso.Doc.Inline.footnote "bar" #[(Verso.Doc.Inline.text "The later footnote.")])]]] + #[] -/ #test_msgs in -#docs (.none) failForwardRefFootnote "Fail" := + #eval footnoteUsesLaterFootnote.toPart + +/- +A footnote's contents may use a link that is defined later in the document. +-/ + +#docs (.none) footnoteUsesLaterLink "Later link" := ::::::: -[^foo]: Disallowing forward reference in footnotes[^bar] +A sentence with a footnote.[^foo] -[^bar]: Even though it's defined later +[^foo]: A footnote with a [later link][bar]. -And used[^bar] +[bar]: http://example.com ::::::: /-- -error: Link reference [bar] does not have a definition +info: Verso.Doc.Part.mk + #[Verso.Doc.Inline.text "Later link"] + "Later link" + none + #[Verso.Doc.Block.para + #[Verso.Doc.Inline.text "A sentence with a footnote.", + Verso.Doc.Inline.footnote + "foo" + #[(Verso.Doc.Inline.text "A footnote with a "), + (Verso.Doc.Inline.link #[(Verso.Doc.Inline.text "later link")] "http://example.com"), + (Verso.Doc.Inline.text ".")]]] + #[] -/ #test_msgs in -#docs (.none) failForwardRefLink "Fail" := + #eval footnoteUsesLaterLink.toPart + +/- +A footnote whose contents use the footnote itself, directly or through other footnotes, is an +error. The error lists the labels of the other footnotes in the cycle. The use that closes the cycle +has empty contents. +-/ + +/-- +error: Footnote [^x] is used inside its own contents, through [^y] +--- +error: Footnote [^self] is used inside its own contents +--- +error: Footnote [^p] is used inside its own contents, through [^q] and [^r] +-/ +#test_msgs in +#docs (.none) footnoteCycle "Footnote cycle" := ::::::: -[^foo]: Disallowing [forward reference in footnotes][bar] +A sentence with three footnotes.[^x][^self][^p] -[bar]: http://example.com +[^x]: The first footnote uses the second.[^y] -[And used][bar] +[^y]: The second footnote uses the first.[^x] + +[^self]: A footnote that uses itself.[^self] + +[^p]: The first of three uses the second.[^q] + +[^q]: The second of three uses the third.[^r] + +[^r]: The third of three uses the first.[^p] ::::::: +/-- +info: Verso.Doc.Part.mk + #[Verso.Doc.Inline.text "Footnote cycle"] + "Footnote cycle" + none + #[Verso.Doc.Block.para + #[Verso.Doc.Inline.text "A sentence with three footnotes.", + Verso.Doc.Inline.footnote + "x" + #[(Verso.Doc.Inline.text "The first footnote uses the second."), + (Verso.Doc.Inline.footnote + "y" + #[(Verso.Doc.Inline.text "The second footnote uses the first."), (Verso.Doc.Inline.footnote "x" #[])])], + Verso.Doc.Inline.footnote + "self" + #[(Verso.Doc.Inline.text "A footnote that uses itself."), (Verso.Doc.Inline.footnote "self" #[])], + Verso.Doc.Inline.footnote + "p" + #[(Verso.Doc.Inline.text "The first of three uses the second."), + (Verso.Doc.Inline.footnote + "q" + #[(Verso.Doc.Inline.text "The second of three uses the third."), + (Verso.Doc.Inline.footnote + "r" + #[(Verso.Doc.Inline.text "The third of three uses the first."), + (Verso.Doc.Inline.footnote "p" #[])])])]]] + #[] +-/ +#test_msgs in + #eval footnoteCycle.toPart + + +/- +Warnings about unused definitions appear in source order. +-/ /-- -warning: Unused footnote [^hidden] ---- warning: Unused footnote [^baz] +--- +warning: Unused footnote [^hidden] -/ #test_msgs in #docs (.none) fail4 "Fail" := @@ -256,3 +381,234 @@ error: No definition for link [fourOhFour] ::::::: There's no [destination][fourOhFour] ::::::: + +/- +Every undefined use and every unused definition is reported, in source order. + +The document has undefined uses, including two uses of `[one]`, and definitions without uses. Each +undefined use gets its own error, and each unused definition gets a warning. +-/ + +/-- +error: No definition for link [one] +--- +warning: Unused footnote [^unused] +--- +error: No definition for footnote [^two] +--- +error: No definition for link [one] +--- +warning: Unused link [spare] +--- +error: No definition for link [three] +-/ +#test_msgs in +#docs (.none) severalUndefined "Several undefined uses" := +::::::: +First [use][one]. + +[^unused]: A footnote that nothing uses. + +A footnote use.[^two] + +Second [use][one]. + +[spare]: https://example.com/spare + +Third [use][three]. +::::::: + +/- +A document with undefined uses is still defined, and its blocks still compile. +-/ + +/-- +error: No definition for link [missing] +--- +error: No definition for footnote [^absent] +-/ +#test_msgs in +#docs (.none) undefinedStillCompiles "Undefined uses" := +::::::: +A [link][missing] and a footnote.[^absent] A [defined link][present]. + +[present]: https://example.com/present +::::::: + +/-- +info: Verso.Doc.Part.mk + #[Verso.Doc.Inline.text "Undefined uses"] + "Undefined uses" + none + #[Verso.Doc.Block.para + #[Verso.Doc.Inline.text "A ", Verso.Doc.Inline.link #[(Verso.Doc.Inline.text "link")] "", + Verso.Doc.Inline.text " and a footnote.", Verso.Doc.Inline.footnote "absent" #[], Verso.Doc.Inline.text " A ", + Verso.Doc.Inline.link #[(Verso.Doc.Inline.text "defined link")] "https://example.com/present", + Verso.Doc.Inline.text "."]] + #[] +-/ +#test_msgs in + #eval undefinedStillCompiles.toPart + +/- +Each use resolves to the definition in its own document, even when another document in the same +module defines the same label. +-/ + +#docs (.none) sameNameFirst "First" := +::::::: +A [link][shared].[^shared] + +[shared]: https://example.com/first +[^shared]: The first document's footnote. +::::::: + +#docs (.none) sameNameSecond "Second" := +::::::: +[shared]: https://example.com/second +[^shared]: The second document's footnote. + +A [link][shared].[^shared] +::::::: + +/-- +info: Verso.Doc.Part.mk + #[Verso.Doc.Inline.text "First"] + "First" + none + #[Verso.Doc.Block.para + #[Verso.Doc.Inline.text "A ", Verso.Doc.Inline.link #[(Verso.Doc.Inline.text "link")] "https://example.com/first", + Verso.Doc.Inline.text ".", + Verso.Doc.Inline.footnote "shared" #[(Verso.Doc.Inline.text "The first document's footnote.")]]] + #[] +-/ +#test_msgs in + #eval sameNameFirst.toPart + +/-- +info: Verso.Doc.Part.mk + #[Verso.Doc.Inline.text "Second"] + "Second" + none + #[Verso.Doc.Block.para + #[Verso.Doc.Inline.text "A ", + Verso.Doc.Inline.link #[(Verso.Doc.Inline.text "link")] "https://example.com/second", Verso.Doc.Inline.text ".", + Verso.Doc.Inline.footnote "shared" #[(Verso.Doc.Inline.text "The second document's footnote.")]]] + #[] +-/ +#test_msgs in + #eval sameNameSecond.toPart + +/- +A link use in a header's title resolves. + +A header's title is elaborated in the document's root term, outside any block. The URL in the value +of the document shows that uses in the root term resolve too. +-/ + +#docs (.none) headerLink "Header link" := +::::::: +# A [header][h] + +[h]: https://example.com/header +::::::: + +/-- +info: Verso.Doc.Part.mk + #[Verso.Doc.Inline.text "Header link"] + "Header link" + none + #[] + #[Verso.Doc.Part.mk + #[Verso.Doc.Inline.text "A ", + Verso.Doc.Inline.link #[(Verso.Doc.Inline.text "header")] "https://example.com/header"] + "A header" + none + #[] + #[]] +-/ +#test_msgs in + #eval headerLink.toPart + +/- +Link uses resolve in a block that a part command adds without its own +`blockInternalDocReconstructionPlaceholder`. + +The part command `plainDirective` adds such a block. The value of the document shows the URL of the +link use in it. For such a block, `addBlock` binds the context's `docReconstructionPlaceholder`. +Without this binding, elaboration would fail with an unknown identifier. +-/ + +section +open Lean Elab Lean.Doc.Syntax Verso.Doc.Elab PartElabM + +@[part_command Lean.Doc.Syntax.directive] +meta def plainDirective : PartCommand + | `(block|:::%$_ $name $_args* { $contents* }%$_) => do + unless name.getId == `plain do throwUnsupportedSyntax + let blocks ← liftDocElabM <| contents.mapM elabBlock + addBlock (← ``(Verso.Doc.Block.concat #[$blocks,*])) + | _ => throwUnsupportedSyntax + +end + +#docs (.none) partCommandBlock "Part command block" := +::::::: +[ref]: https://example.com/part-command + +:::plain +A [link][ref]. +::: +::::::: + +/-- +info: Verso.Doc.Part.mk + #[Verso.Doc.Inline.text "Part command block"] + "Part command block" + none + #[Verso.Doc.Block.concat + #[(Verso.Doc.Block.para + #[Verso.Doc.Inline.text "A ", + Verso.Doc.Inline.link #[(Verso.Doc.Inline.text "link")] "https://example.com/part-command", + Verso.Doc.Inline.text "."])]] + #[] +-/ +#test_msgs in + #eval partCommandBlock.toPart + +/- +An error in a footnote's contents is reported once, at the footnote. + +The role `illTyped` gives the footnote's contents a type error, and the error appears once. +Footnote contents are elaborated twice: at the definition, where their errors are reported, and in +the document's root term. Contents with errors are recorded as empty, so the root term has no error +to report. +-/ + +section +open Verso.Doc.Elab + +/-- A role that elaborates to an ill-typed inline. -/ +@[role] +def illTyped : RoleExpanderOf Unit + | (), _ => ``(Verso.Doc.Inline.text (5 : Nat)) + +end + +/-- +error: Application type mismatch: The argument + 5 +has type + Nat +but is expected to have type + String +in the application + Doc.Inline.text 5 +-/ +#test_msgs in +#docs (.none) footnoteError "Footnote error" := +::::::: +Text.[^a] + +[^a]: A {illTyped}[] body. +::::::: diff --git a/src/tests/VersoTests/Refs/AcrossBlocks.lean b/src/tests/VersoTests/Refs/AcrossBlocks.lean new file mode 100644 index 000000000..472553d8b --- /dev/null +++ b/src/tests/VersoTests/Refs/AcrossBlocks.lean @@ -0,0 +1,32 @@ +/- +Copyright (c) 2026 Lean FRO LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Author: David Thrane Christiansen +-/ +import Verso + +/-! +A document for the tests in `VersoTests.Refs.DocCommand`. Its links and footnotes are used in +top-level blocks before and after their definitions, and some footnote bodies use earlier links +and footnotes. +-/ + +#doc (.none) "Across blocks" => + +A [forward link][later] and a forward footnote.[^later] + +[earlier]: https://example.com/earlier + +[^earlier]: An earlier footnote with a [link][earlier]. + +# A section with an [earlier link][earlier] + +> A quote with a [forward link][later] and a footnote.[^earlier] + +* A list item with a [backward link][earlier]. + +[later]: https://example.com/later + +[^later]: A later footnote that uses an earlier one.[^earlier] + +A [backward link][later] after the definitions.[^later] diff --git a/src/tests/VersoTests/Refs/DocCommand.lean b/src/tests/VersoTests/Refs/DocCommand.lean new file mode 100644 index 000000000..7ee22a4a4 --- /dev/null +++ b/src/tests/VersoTests/Refs/DocCommand.lean @@ -0,0 +1,505 @@ +/- +Copyright (c) 2026 Lean FRO LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Author: David Thrane Christiansen +-/ +import Errata +import Verso +import VersoManual +import VersoTests.Refs.AcrossBlocks +import VersoTests.Refs.ManualFootnote +import VersoTests.Refs.SameName + +/-! +These tests check link and footnote label resolution in documents that the {lit}`#doc` command +elaborates block by block. They also check that Verso finishes such a document even when its last +block fails. + +Each top-level block of a {lit}`#doc` document is its own Lean command, so a label definition and +its uses can be in different commands. Verso finishes the document in the command parsed from the +last block. That's when it checks the links and footnotes and defines the document constant. + +The first tests evaluate documents from other modules and observe their values. The later tests +elaborate a document from a string with Lean's command loop. They observe which command reported +each message, and the value of the document. +-/ + +set_option guard_msgs.diff true + +namespace Verso.RefsTest.DocCommand + +open Lean Elab Command +open Verso.Doc + +/- +Uses resolve across top-level blocks, whether the definition comes before or after the use. + +The document in `VersoTests.Refs.AcrossBlocks` has link and footnote uses before and after their +definitions. The uses are in paragraphs, a header, a quote and a list, and some footnote bodies use +earlier links and footnotes. In the value of the document, each use has the URL or contents of its +definition. A use that didn't resolve would have the empty URL or empty contents. The contents of +`[^later]` include a nested footnote, which shows that a footnote body can use the footnotes defined +before it. +-/ + +/-- +info: Verso.Doc.Part.mk + #[Verso.Doc.Inline.text "Across blocks"] + "Across blocks" + none + #[Verso.Doc.Block.para + #[Verso.Doc.Inline.text "A ", + Verso.Doc.Inline.link #[(Verso.Doc.Inline.text "forward link")] "https://example.com/later", + Verso.Doc.Inline.text " and a forward footnote.", + Verso.Doc.Inline.footnote + "later" + #[(Verso.Doc.Inline.text "A later footnote that uses an earlier one."), + (Verso.Doc.Inline.footnote + "earlier" + #[(Verso.Doc.Inline.text "An earlier footnote with a "), + (Verso.Doc.Inline.link #[(Verso.Doc.Inline.text "link")] "https://example.com/earlier"), + (Verso.Doc.Inline.text ".")])]]] + #[Verso.Doc.Part.mk + #[Verso.Doc.Inline.text "A section with an ", + Verso.Doc.Inline.link #[(Verso.Doc.Inline.text "earlier link")] "https://example.com/earlier"] + "A section with an earlier link" + none + #[Verso.Doc.Block.blockquote + #[(Verso.Doc.Block.para + #[Verso.Doc.Inline.text "A quote with a ", + Verso.Doc.Inline.link #[(Verso.Doc.Inline.text "forward link")] "https://example.com/later", + Verso.Doc.Inline.text " and a footnote.", + Verso.Doc.Inline.footnote + "earlier" + #[(Verso.Doc.Inline.text "An earlier footnote with a "), + (Verso.Doc.Inline.link #[(Verso.Doc.Inline.text "link")] "https://example.com/earlier"), + (Verso.Doc.Inline.text ".")]])], + Verso.Doc.Block.ul + #[{ contents := #[Verso.Doc.Block.para + #[Verso.Doc.Inline.text "A list item with a ", + Verso.Doc.Inline.link + #[(Verso.Doc.Inline.text "backward link")] + "https://example.com/earlier", + Verso.Doc.Inline.text "."]] }], + Verso.Doc.Block.para + #[Verso.Doc.Inline.text "A ", + Verso.Doc.Inline.link #[(Verso.Doc.Inline.text "backward link")] "https://example.com/later", + Verso.Doc.Inline.text " after the definitions.", + Verso.Doc.Inline.footnote + "later" + #[(Verso.Doc.Inline.text "A later footnote that uses an earlier one."), + (Verso.Doc.Inline.footnote + "earlier" + #[(Verso.Doc.Inline.text "An earlier footnote with a "), + (Verso.Doc.Inline.link #[(Verso.Doc.Inline.text "link")] "https://example.com/earlier"), + (Verso.Doc.Inline.text ".")])], + Verso.Doc.Inline.linebreak "\n"]] + #[]] +-/ +#test_msgs in +#eval %doc VersoTests.Refs.AcrossBlocks + +/- +Each use resolves to the definition in its own document, even when other documents in the same +module define the same labels. + +The module `VersoTests.Refs.SameName` has two `#docs` documents and one `#doc` document. All three +define the same link and footnote labels with different values. The value of each document shows +its own URL and footnote contents. +-/ + +/-- +info: Verso.Doc.Part.mk + #[Verso.Doc.Inline.text "Third"] + "Third" + none + #[Verso.Doc.Block.para + #[Verso.Doc.Inline.text "A ", Verso.Doc.Inline.link #[(Verso.Doc.Inline.text "link")] "https://example.com/third", + Verso.Doc.Inline.text ".", + Verso.Doc.Inline.footnote + "shared" + #[(Verso.Doc.Inline.text "The third footnote."), (Verso.Doc.Inline.linebreak "\n")]]] + #[] +-/ +#test_msgs in +#eval %doc VersoTests.Refs.SameName + +/-- +info: Verso.Doc.Part.mk + #[Verso.Doc.Inline.text "First"] + "First" + none + #[Verso.Doc.Block.para + #[Verso.Doc.Inline.text "A ", Verso.Doc.Inline.link #[(Verso.Doc.Inline.text "link")] "https://example.com/first", + Verso.Doc.Inline.text ".", Verso.Doc.Inline.footnote "shared" #[(Verso.Doc.Inline.text "The first footnote.")]]] + #[] +-/ +#test_msgs in +#eval Verso.RefsTest.SameName.first.toPart + +/-- +info: Verso.Doc.Part.mk + #[Verso.Doc.Inline.text "Second"] + "Second" + none + #[Verso.Doc.Block.para + #[Verso.Doc.Inline.text "A ", + Verso.Doc.Inline.link #[(Verso.Doc.Inline.text "link")] "https://example.com/second", Verso.Doc.Inline.text ".", + Verso.Doc.Inline.footnote "shared" #[(Verso.Doc.Inline.text "The second footnote.")]]] + #[] +-/ +#test_msgs in +#eval Verso.RefsTest.SameName.second.toPart + +/- +A {lit}`{lean}` role works inside a footnote of a {lit}`Manual` document. + +The module `VersoTests.Refs.ManualFootnote` has such a footnote in a {lit}`#docs` document and in +the {lit}`#doc` document. The summary of each footnote's contents shows an inline +{lit}`Verso.Genre.Manual.InlineLean.Inline.lean` whose data mentions {lit}`Nat.succ`. This shows +that the role elaborated and that its highlighted code was restored from the document reconstruction +data. In prior versions of the link and footnote resolution, footnote contents were elaborated with +the {lit}`docReconstructionPlaceholder` unbound, and the role failed with "Unknown identifier +docReconst". +-/ + +/-- The contents of the first footnote with the label {lit}`label` in {lit}`part`'s own blocks. -/ +def footnoteIn (label : String) (part : Part Genre.Manual) : Option (Array (Inline Genre.Manual)) := + part.content.findSome? block +where + block : Block Genre.Manual → Option (Array (Inline Genre.Manual)) + | .para xs => xs.findSome? inline + | _ => none + inline : Inline Genre.Manual → Option (Array (Inline Genre.Manual)) + | .footnote l xs => if l == label then some xs else none + | _ => none + +/-- +A summary of footnote contents: the text, and for each other inline, its name and whether its data +mentions {lit}`Nat.succ`. +-/ +def summarize (xs : Array (Inline Genre.Manual)) : List String := + xs.toList.map fun + | .text s => s!"text {s.quote}" + | .other i _ => s!"other {i.name} (mentions Nat.succ: {(i.data.compress.find? "Nat.succ").isSome})" + | .link _ url => s!"link {url.quote}" + | _ => "other inline" + +/-- +info: some + ["text \"A note about \"", "other Verso.Genre.Manual.InlineLean.Inline.lean (mentions Nat.succ: true)", "text \".\""] +-/ +#test_msgs in +#eval (footnoteIn "note" Verso.RefsTest.ManualFootnote.allAtOnce.toPart).map summarize + +/-- +info: some + ["text \"A note about \"", "other Verso.Genre.Manual.InlineLean.Inline.lean (mentions Nat.succ: true)", + "text \", with a \"", "link \"https://example.com\"", "text \".\"", "other inline"] +-/ +#test_msgs in +#eval (footnoteIn "note" (%doc VersoTests.Refs.ManualFootnote)).map summarize + +/-! +The remaining tests elaborate a {lit}`#doc` command from a string with Lean's command loop, so that +documents with errors can be checked. Messages are shown with the number of the command that +reported them. Command 0 is the {lit}`#doc` command itself, and command {lit}`k` is the document's +{lit}`k`-th top-level block. +-/ + +/-- Renders a message with its position. -/ +def showMessage (m : Message) : IO String := do + let severity := match m.severity with + | .error => "error" + | .warning => "warning" + | .information => "info" + return s!"{m.pos.line}:{m.pos.column}: {severity}: {← m.data.toString}" + +/-- +Elaborates {lit}`input` as the rest of a module, in the current environment. Returns the resulting +environment, and each command's messages rendered with the command's number. +-/ +def elabModuleRest (input : String) : CommandElabM (Environment × String) := do + let inputCtx := Parser.mkInputContext input "RefsInput.lean" + let st ← IO.processCommandsIncrementally inputCtx {} + (Command.mkState (← getEnv) {} (← getOptions)) none + let mut out := #[] + let mut snap := st.initialSnap + let mut i := 0 + repeat + let msgs := Language.toSnapshotTree snap.elabSnap |>.getAll + |>.map (·.diagnostics.msgLog) |>.foldl (· ++ ·) MessageLog.empty + for m in msgs.toList do + out := out.push s!"command {i}: {← showMessage m}" + i := i + 1 + match snap.nextCmdSnap? with + | some next => snap := next.task.get + | none => break + return (st.commandState.env, "\n".intercalate out.toList) + +unsafe def evalDocUnsafe (env : Environment) (opts : Options) (n : Name) : IO (VersoDoc Genre.none) := + IO.ofExcept <| env.evalConst (VersoDoc Genre.none) opts n + +/-- Evaluates the document constant {lit}`n` of {lit}`env`. -/ +@[implemented_by evalDocUnsafe] +opaque evalDoc (env : Environment) (opts : Options) (n : Name) : IO (VersoDoc Genre.none) + +/-- +Elaborates {lit}`input`, which ends with a {lit}`#doc` command, and logs its messages and its +document. +-/ +def checkDocInput (input : String) : CommandElabM Unit := do + let (env, msgs) ← elabModuleRest input + logInfo msgs + let docName := Verso.Doc.docName (← getMainModule) + if env.contains docName then + match ← (evalDoc env (← getOptions) docName).toBaseIO with + | .ok doc => logInfo m!"{repr doc.toPart}" + | .error _ => logInfo m!"The document is defined, and it contains errors, so it can't be evaluated." + else + logInfo m!"The document {docName} is not defined." + +/- +In a {lit}`#doc` document, every message about links and footnotes appears, and the document is +still defined. +-/ + +/-- +info: command 5: 11:1: error: Duplicate definition of link label [dup]. It is already defined at line 9, column 1, with the URL 'https://example.com/a'. This definition has the URL 'https://example.com/b'. +command 7: 15:2: error: Duplicate definition of footnote label [^dupNote]. It is already defined at line 13, column 2. +command 10: 3:12: error: No definition for link [one] +command 10: 5:2: warning: Unused footnote [^unused] +command 10: 7:17: error: No definition for footnote [^two] +command 10: 19:12: error: No definition for link [three] +--- +info: Verso.Doc.Part.mk + #[Verso.Doc.Inline.text "Errors"] + "Errors" + none + #[Verso.Doc.Block.para + #[Verso.Doc.Inline.text "First ", Verso.Doc.Inline.link #[(Verso.Doc.Inline.text "use")] "", + Verso.Doc.Inline.text "."], + Verso.Doc.Block.para #[Verso.Doc.Inline.text "A footnote use.", Verso.Doc.Inline.footnote "two" #[]], + Verso.Doc.Block.para + #[Verso.Doc.Inline.text "Uses of ", + Verso.Doc.Inline.link #[(Verso.Doc.Inline.text "dup")] "https://example.com/a", + Verso.Doc.Inline.text " and a note.", + Verso.Doc.Inline.footnote "dupNote" #[(Verso.Doc.Inline.text "The first.")]], + Verso.Doc.Block.para + #[Verso.Doc.Inline.text "Third ", Verso.Doc.Inline.link #[(Verso.Doc.Inline.text "use")] "", + Verso.Doc.Inline.text " and ", + Verso.Doc.Inline.link #[(Verso.Doc.Inline.text "a defined link")] "https://example.com/defined", + Verso.Doc.Inline.text "."]] + #[] +-/ +#test_msgs in +#eval checkDocInput "#doc (.none) \"Errors\" => + +First [use][one]. + +[^unused]: A footnote that nothing uses. + +A footnote use.[^two] + +[dup]: https://example.com/a + +[dup]: https://example.com/b + +[^dupNote]: The first. + +[^dupNote]: The second. + +Uses of [dup][dup] and a note.[^dupNote] + +Third [use][three] and [a defined link][defined]. + +[defined]: https://example.com/defined +" + +/- +Verso finishes a {lit}`#doc` document even when its last block fails. This ensures that errors in +the last block don't obliterate info from earlier blocks that should be saved. +-/ + +/-- +info: command 3: 7:1: error: Duplicate definition of link label [d]. It is already defined at line 5, column 1, with the URL 'https://example.com/a'. This definition has the URL 'https://example.com/b'. +command 3: 3:12: error: No definition for link [one] +command 3: 5:1: warning: Unused link [d] +--- +info: Verso.Doc.Part.mk + #[Verso.Doc.Inline.text "Last block is a duplicate"] + "Last block is a duplicate" + none + #[Verso.Doc.Block.para + #[Verso.Doc.Inline.text "First ", Verso.Doc.Inline.link #[(Verso.Doc.Inline.text "use")] "", + Verso.Doc.Inline.text "."]] + #[] +-/ +#test_msgs in +#eval checkDocInput "#doc (.none) \"Last block is a duplicate\" => + +First [use][one]. + +[d]: https://example.com/a + +[d]: https://example.com/b +" + +/-- +info: command 2: 5:3: error: No registered directive `nosuch`. +command 2: 3:12: error: No definition for link [one] +--- +info: Verso.Doc.Part.mk + #[Verso.Doc.Inline.text "Last block is an unknown directive"] + "Last block is an unknown directive" + none + #[Verso.Doc.Block.para + #[Verso.Doc.Inline.text "First ", Verso.Doc.Inline.link #[(Verso.Doc.Inline.text "use")] "", + Verso.Doc.Inline.text "."]] + #[] +-/ +#test_msgs in +#eval checkDocInput "#doc (.none) \"Last block is an unknown directive\" => + +First [use][one]. + +:::nosuch +Text. +::: +" + +/-- +info: command 2: 5:0: error: Wrong header nesting - got ### but expected at most # +command 2: 3:12: error: No definition for link [one] +--- +info: Verso.Doc.Part.mk + #[Verso.Doc.Inline.text "Last block is a header that is too deep"] + "Last block is a header that is too deep" + none + #[Verso.Doc.Block.para + #[Verso.Doc.Inline.text "First ", Verso.Doc.Inline.link #[(Verso.Doc.Inline.text "use")] "", + Verso.Doc.Inline.text "."]] + #[] +-/ +#test_msgs in +#eval checkDocInput "#doc (.none) \"Last block is a header that is too deep\" => + +First [use][one]. + +### A header that is too deep +" + +/- +In a {lit}`#doc` document, an error in a footnote's contents is reported once, in the footnote's own +block. +-/ + +open Verso.Doc.Elab in +/-- A role that elaborates to an ill-typed inline. -/ +@[role] +def illTyped : RoleExpanderOf Unit + | (), _ => ``(Verso.Doc.Inline.text (5 : Nat)) + +/-- +info: command 2: 5:8: error: Application type mismatch: The argument + 5 +has type + Nat +but is expected to have type + String +in the application + Verso.Doc.Inline.text 5 +--- +info: Verso.Doc.Part.mk + #[Verso.Doc.Inline.text "Footnote error"] + "Footnote error" + none + #[Verso.Doc.Block.para #[Verso.Doc.Inline.text "Text.", Verso.Doc.Inline.footnote "f" #[]], + Verso.Doc.Block.para #[Verso.Doc.Inline.text "A later paragraph.", Verso.Doc.Inline.linebreak "\n"]] + #[] +-/ +#test_msgs in +#eval checkDocInput "#doc (.none) \"Footnote error\" => + +Text.[^f] + +[^f]: A {Verso.RefsTest.DocCommand.illTyped}[] body. + +A later paragraph. +" + +/- +A parse error in the last block doesn't hide the messages about links and footnotes in earlier +blocks. +-/ + +/-- +info: command 3: 3:12: error: No definition for link [one] +--- +info: Verso.Doc.Part.mk + #[Verso.Doc.Inline.text "Last block has a parse error"] + "Last block has a parse error" + none + #[Verso.Doc.Block.para + #[Verso.Doc.Inline.text "First ", Verso.Doc.Inline.link #[(Verso.Doc.Inline.text "use")] "", + Verso.Doc.Inline.text "."], + Verso.Doc.Block.para #[Verso.Doc.Inline.text "Second."]] + #[] +-/ +#test_msgs in +#eval checkDocInput "#doc (.none) \"Last block has a parse error\" => + +First [use][one]. + +Second. + +A *bold never closed {role +" + +/- +A parse error that leaves the last block without a source range doesn't hide these messages either. +-/ + +/-- +info: command 2: 3:12: error: No definition for link [one] +--- +info: The document is defined, and it contains errors, so it can't be evaluated. +-/ +#test_msgs in +#eval checkDocInput "#doc (.none) \"Unclosed role with a use\" => + +First [use][one]. + +Broken [u][two] then {role +" + +/-- +info: command 3: 3:12: error: No definition for link [one] +command 3: 5:1: warning: Unused link [d] +--- +info: The document is defined, and it contains errors, so it can't be evaluated. +-/ +#test_msgs in +#eval checkDocInput "#doc (.none) \"Unclosed role after a definition\" => + +First [use][one]. + +[d]: https://example.com/d + +Broken then {role +" + +/-- +info: command 3: 3:12: error: No definition for link [one] +--- +info: The document is defined, and it contains errors, so it can't be evaluated. +-/ +#test_msgs in +#eval checkDocInput "#doc (.none) \"Unclosed role after a paragraph\" => + +First [use][one]. + +Second. + +Broken then {role +" diff --git a/src/tests/VersoTests/Refs/ManualFootnote.lean b/src/tests/VersoTests/Refs/ManualFootnote.lean new file mode 100644 index 000000000..88479308b --- /dev/null +++ b/src/tests/VersoTests/Refs/ManualFootnote.lean @@ -0,0 +1,33 @@ +/- +Copyright (c) 2026 Lean FRO LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Author: David Thrane Christiansen +-/ +import VersoManual + +/-! +Two {lit}`Manual` documents for the tests in `VersoTests.Refs.DocCommand`, each with a +{lit}`{lean}` role inside a footnote. {lit}`#docs` elaborates the first all at once, and +{lit}`#doc` elaborates the second block by block. +-/ + +open Verso Genre Manual InlineLean + +namespace Verso.RefsTest.ManualFootnote + +#docs (Manual) allAtOnce "Footnote with Lean code" := +::::::: +Text.[^note] + +[^note]: A note about {lean}`Nat.succ 2`. +::::::: + +end Verso.RefsTest.ManualFootnote + +#doc (Manual) "Footnote with Lean code" => + +[example]: https://example.com + +Text.[^note] + +[^note]: A note about {lean}`Nat.succ 2`, with a [link][example]. diff --git a/src/tests/VersoTests/Refs/SameName.lean b/src/tests/VersoTests/Refs/SameName.lean new file mode 100644 index 000000000..94b810b55 --- /dev/null +++ b/src/tests/VersoTests/Refs/SameName.lean @@ -0,0 +1,39 @@ +/- +Copyright (c) 2026 Lean FRO LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Author: David Thrane Christiansen +-/ +import Verso + +/-! +Documents for the tests in `VersoTests.Refs.DocCommand`: three documents in one module that define +the same link and footnote labels with different values. +-/ + +namespace Verso.RefsTest.SameName + +#docs (.none) first "First" := +::::::: +A [link][shared].[^shared] + +[shared]: https://example.com/first +[^shared]: The first footnote. +::::::: + +#docs (.none) second "Second" := +::::::: +[shared]: https://example.com/second +[^shared]: The second footnote. + +A [link][shared].[^shared] +::::::: + +end Verso.RefsTest.SameName + +#doc (.none) "Third" => + +A [link][shared].[^shared] + +[shared]: https://example.com/third + +[^shared]: The third footnote. diff --git a/src/tests/interactive/test-cases/highlight_list_bullets.lean b/src/tests/interactive/test-cases/highlight_list_bullets.lean new file mode 100644 index 000000000..a9453374f --- /dev/null +++ b/src/tests/interactive/test-cases/highlight_list_bullets.lean @@ -0,0 +1,43 @@ +import Verso + +/-! +Document highlight on a list bullet applies to all the bullets of that list and no others. +-/ + +#docs (.none) docsList "A list in #docs" := +::::::: +* One +--⬑ sync +--⬑ textDocument/documentHighlight +* Two +::::::: + +#doc (.none) "Lists" => + +* One +* Two +--⬑ textDocument/documentHighlight +* Three + +1. One +2. Two +--⬑ textDocument/documentHighlight +3. Three + +* Outer one + + * Inner one + --⬑ textDocument/documentHighlight + * Inner two + +* Outer two +--⬑ textDocument/documentHighlight + +: First term + + First description + +: Second term +--⬑ textDocument/documentHighlight + + Second description diff --git a/src/tests/interactive/test-cases/highlight_list_bullets.lean.expected.out b/src/tests/interactive/test-cases/highlight_list_bullets.lean.expected.out new file mode 100644 index 000000000..2ba807dab --- /dev/null +++ b/src/tests/interactive/test-cases/highlight_list_bullets.lean.expected.out @@ -0,0 +1,52 @@ +{"textDocument": + {"uri": + "file:///src/tests/interactive/test-cases/highlight_list_bullets.lean"}, + "position": {"line": 8, "character": 0}} +[{"range": + {"start": {"line": 8, "character": 0}, "end": {"line": 8, "character": 1}}}, + {"range": + {"start": {"line": 11, "character": 0}, "end": {"line": 11, "character": 1}}}] +{"textDocument": + {"uri": + "file:///src/tests/interactive/test-cases/highlight_list_bullets.lean"}, + "position": {"line": 17, "character": 0}} +[{"range": + {"start": {"line": 16, "character": 0}, "end": {"line": 16, "character": 1}}}, + {"range": + {"start": {"line": 17, "character": 0}, "end": {"line": 17, "character": 1}}}, + {"range": + {"start": {"line": 19, "character": 0}, "end": {"line": 19, "character": 1}}}] +{"textDocument": + {"uri": + "file:///src/tests/interactive/test-cases/highlight_list_bullets.lean"}, + "position": {"line": 22, "character": 0}} +[{"range": + {"start": {"line": 21, "character": 0}, "end": {"line": 21, "character": 2}}}, + {"range": + {"start": {"line": 22, "character": 0}, "end": {"line": 22, "character": 2}}}, + {"range": + {"start": {"line": 24, "character": 0}, "end": {"line": 24, "character": 2}}}] +{"textDocument": + {"uri": + "file:///src/tests/interactive/test-cases/highlight_list_bullets.lean"}, + "position": {"line": 28, "character": 2}} +[{"range": + {"start": {"line": 28, "character": 2}, "end": {"line": 28, "character": 3}}}, + {"range": + {"start": {"line": 30, "character": 2}, "end": {"line": 30, "character": 3}}}] +{"textDocument": + {"uri": + "file:///src/tests/interactive/test-cases/highlight_list_bullets.lean"}, + "position": {"line": 32, "character": 0}} +[{"range": + {"start": {"line": 26, "character": 0}, "end": {"line": 26, "character": 1}}}, + {"range": + {"start": {"line": 32, "character": 0}, "end": {"line": 32, "character": 1}}}] +{"textDocument": + {"uri": + "file:///src/tests/interactive/test-cases/highlight_list_bullets.lean"}, + "position": {"line": 39, "character": 0}} +[{"range": + {"start": {"line": 35, "character": 0}, "end": {"line": 35, "character": 1}}}, + {"range": + {"start": {"line": 39, "character": 0}, "end": {"line": 39, "character": 1}}}] diff --git a/src/tests/interactive/test-cases/refs_across_blocks.lean b/src/tests/interactive/test-cases/refs_across_blocks.lean new file mode 100644 index 000000000..fad8abf29 --- /dev/null +++ b/src/tests/interactive/test-cases/refs_across_blocks.lean @@ -0,0 +1,188 @@ +import Verso + +/-! +These tests check go to definition and document highlight for links and footnotes whose definitions +and uses are in different top-level blocks. They cover requests while the document elaborates and +after it has finished. They matter when changing how Verso records link and footnote definitions +and uses for the editor, or the language server handlers that answer these requests. + +In this section, each top-level block of the `#doc` document is its own command, so each answer +combines definitions and uses from several snapshots. The requests are, in order: go to definition +and highlight from a link use and a footnote use before their definitions, highlight from the link +definition, and go to definition from a link use and a footnote use after their definitions. The +`#docs` document `otherDoc` defines the same link label `site`. Highlight on its use lists only its +own use and definition. + +Each answer lists the definition, or the definition and every use, of the label in the same +document. An answer without a definition in a later block would mean that the request read only +the snapshot under the cursor. An answer with a range in `otherDoc` would mean that the requests +confused the two documents. +-/ + +#docs (.none) otherDoc "Other" := +::::::: +Another [use][site]. + --^ sync + --^ textDocument/documentHighlight + +[site]: https://example.org +::::::: + +#doc (.none) "Links and footnotes across blocks" => + +A [forward link][site] and a forward footnote.[^note] + --^ textDocument/definition + --^ textDocument/documentHighlight + --^ textDocument/definition + --^ textDocument/documentHighlight + +[site]: https://example.com +--^ textDocument/documentHighlight + +[^note]: A footnote. + +A [backward link][site] and a backward footnote.[^note] + --^ textDocument/definition + --^ textDocument/definition +-- RESET +import Verso + +/-! +Go to definition and highlight answer while the document is still elaborating. The answers use the +top-level blocks that have finished. + +The `waitFor` directive waits for the error message of the block `{marker}[]`, so the blocks before +it have finished. The role `slow` then keeps the document elaborating for ten seconds, well after +the requests are answered. The answers list the definitions and uses before `{slow}[]`, and none of +the uses in the last block. An answer with the last block's uses would mean that the request +waited for the end of the document. +-/ + +open Verso Doc Elab + +@[role] +def slow : RoleExpanderOf Unit + | (), _ => do + IO.sleep 10000 + ``(Inline.text "slow") + +#doc (.none) "Before the document finishes" => +--^ waitFor: No registered role `marker`. + +A [forward link][site] and a forward footnote.[^note] + --^ textDocument/definition + --^ textDocument/documentHighlight + --^ textDocument/definition + --^ textDocument/documentHighlight + +[site]: https://example.com + +[^note]: A footnote. + +A [backward link][site] and a backward footnote.[^note] + --^ textDocument/definition + +{marker}[] + +{slow}[] + +A [late link][site] and a late footnote.[^note] +-- RESET +import Verso + +/-! +A link and a footnote with the same label are separate. Definitions and uses in different parts of +one document are related. + +In the `#docs` document, a link and a footnote both have the label `same`. Go to definition and +highlight from the link list only the link's definition and use. Highlight from the footnote lists +only the footnote's. An answer that mixed them would mean that the requests ignored which kind of +label each is. + +In the `#doc` document, the uses are in the first section, and the definitions are in a subsection +of the second section. The third section has another use. Go to definition and highlight find the +definitions and uses in the other sections. An answer without the definitions would mean that each +part was treated as its own document. +-/ + +#docs (.none) kinds "Kinds" := +::::::: +A [link][same] and a footnote.[^same] + --^ sync + --^ textDocument/definition + --^ textDocument/documentHighlight + --^ textDocument/documentHighlight + +[same]: https://example.com/same + +[^same]: The footnote. +::::::: + +#doc (.none) "Parts" => + +# First section + +A [link][same] and a footnote.[^same] + --^ textDocument/definition + --^ textDocument/documentHighlight + --^ textDocument/definition + --^ textDocument/documentHighlight + +# Second section + +## A subsection + +[same]: https://example.com/same + +[^same]: The footnote. + +# Third section + +Another [link][same]. + --^ textDocument/definition +-- RESET +import Verso + +/-! +Requests from a use in a failing block work, and their answers include that use. + +A failing block leaves its definitions and uses out of the document's state in the environment. Go +to definition and highlight from the use of `site` in the failing block still work, and the +highlight lists that use. An answer taken only from the environment would leave out the use under +the cursor. +-/ + +#doc (.none) "Failing block" => + +A [link][site]. + +A failing block with a [link][site] and {nosuchrole}[x]. + --^ sync + --^ textDocument/definition + --^ textDocument/documentHighlight + +[site]: https://example.com/site + +The end. +-- RESET +import Verso + +/-! +Go to definition and highlight work from uses in a footnote's contents whose definitions come later +in the document. The answers point into this file. +-/ + +#doc (.none) "Footnote contents" => + +A sentence with a footnote.[^note] + +[^note]: A footnote with a [link][site] and another footnote.[^later] + --^ sync + --^ textDocument/definition + --^ textDocument/documentHighlight + --^ textDocument/definition + --^ textDocument/documentHighlight + +[site]: https://example.com/site + +[^later]: The later footnote. diff --git a/src/tests/interactive/test-cases/refs_across_blocks.lean.expected.out b/src/tests/interactive/test-cases/refs_across_blocks.lean.expected.out new file mode 100644 index 000000000..519347036 --- /dev/null +++ b/src/tests/interactive/test-cases/refs_across_blocks.lean.expected.out @@ -0,0 +1,293 @@ +{"textDocument": + {"uri": "file:///src/tests/interactive/test-cases/refs_across_blocks.lean"}, + "position": {"line": 23, "character": 14}} +[{"range": + {"start": {"line": 23, "character": 14}, + "end": {"line": 23, "character": 18}}}, + {"range": + {"start": {"line": 27, "character": 1}, "end": {"line": 27, "character": 5}}}] +{"textDocument": + {"uri": "file:///src/tests/interactive/test-cases/refs_across_blocks.lean"}, + "position": {"line": 32, "character": 17}} +[{"targetUri": + "file:///src/tests/interactive/test-cases/refs_across_blocks.lean", + "targetSelectionRange": + {"start": {"line": 38, "character": 1}, "end": {"line": 38, "character": 5}}, + "targetRange": + {"start": {"line": 38, "character": 1}, "end": {"line": 38, "character": 5}}, + "originSelectionRange": + {"start": {"line": 32, "character": 17}, + "end": {"line": 32, "character": 21}}}] +{"textDocument": + {"uri": "file:///src/tests/interactive/test-cases/refs_across_blocks.lean"}, + "position": {"line": 32, "character": 17}} +[{"range": + {"start": {"line": 32, "character": 17}, + "end": {"line": 32, "character": 21}}}, + {"range": + {"start": {"line": 38, "character": 1}, "end": {"line": 38, "character": 5}}}, + {"range": + {"start": {"line": 43, "character": 18}, + "end": {"line": 43, "character": 22}}}] +{"textDocument": + {"uri": "file:///src/tests/interactive/test-cases/refs_across_blocks.lean"}, + "position": {"line": 32, "character": 48}} +[{"targetUri": + "file:///src/tests/interactive/test-cases/refs_across_blocks.lean", + "targetSelectionRange": + {"start": {"line": 41, "character": 2}, "end": {"line": 41, "character": 6}}, + "targetRange": + {"start": {"line": 41, "character": 2}, "end": {"line": 41, "character": 6}}, + "originSelectionRange": + {"start": {"line": 32, "character": 48}, + "end": {"line": 32, "character": 52}}}] +{"textDocument": + {"uri": "file:///src/tests/interactive/test-cases/refs_across_blocks.lean"}, + "position": {"line": 32, "character": 48}} +[{"range": + {"start": {"line": 32, "character": 48}, + "end": {"line": 32, "character": 52}}}, + {"range": + {"start": {"line": 41, "character": 2}, "end": {"line": 41, "character": 6}}}, + {"range": + {"start": {"line": 43, "character": 50}, + "end": {"line": 43, "character": 54}}}] +{"textDocument": + {"uri": "file:///src/tests/interactive/test-cases/refs_across_blocks.lean"}, + "position": {"line": 38, "character": 2}} +[{"range": + {"start": {"line": 32, "character": 17}, + "end": {"line": 32, "character": 21}}}, + {"range": + {"start": {"line": 38, "character": 1}, "end": {"line": 38, "character": 5}}}, + {"range": + {"start": {"line": 43, "character": 18}, + "end": {"line": 43, "character": 22}}}] +{"textDocument": + {"uri": "file:///src/tests/interactive/test-cases/refs_across_blocks.lean"}, + "position": {"line": 43, "character": 18}} +[{"targetUri": + "file:///src/tests/interactive/test-cases/refs_across_blocks.lean", + "targetSelectionRange": + {"start": {"line": 38, "character": 1}, "end": {"line": 38, "character": 5}}, + "targetRange": + {"start": {"line": 38, "character": 1}, "end": {"line": 38, "character": 5}}, + "originSelectionRange": + {"start": {"line": 43, "character": 18}, + "end": {"line": 43, "character": 22}}}] +{"textDocument": + {"uri": "file:///src/tests/interactive/test-cases/refs_across_blocks.lean"}, + "position": {"line": 43, "character": 50}} +[{"targetUri": + "file:///src/tests/interactive/test-cases/refs_across_blocks.lean", + "targetSelectionRange": + {"start": {"line": 41, "character": 2}, "end": {"line": 41, "character": 6}}, + "targetRange": + {"start": {"line": 41, "character": 2}, "end": {"line": 41, "character": 6}}, + "originSelectionRange": + {"start": {"line": 43, "character": 50}, + "end": {"line": 43, "character": 54}}}] +{"textDocument": + {"uri": "file:///src/tests/interactive/test-cases/refs_across_blocks.lean"}, + "position": {"line": 25, "character": 17}} +[{"targetUri": + "file:///src/tests/interactive/test-cases/refs_across_blocks.lean", + "targetSelectionRange": + {"start": {"line": 31, "character": 1}, "end": {"line": 31, "character": 5}}, + "targetRange": + {"start": {"line": 31, "character": 1}, "end": {"line": 31, "character": 5}}, + "originSelectionRange": + {"start": {"line": 25, "character": 17}, + "end": {"line": 25, "character": 21}}}] +{"textDocument": + {"uri": "file:///src/tests/interactive/test-cases/refs_across_blocks.lean"}, + "position": {"line": 25, "character": 17}} +[{"range": + {"start": {"line": 25, "character": 17}, + "end": {"line": 25, "character": 21}}}, + {"range": + {"start": {"line": 31, "character": 1}, "end": {"line": 31, "character": 5}}}, + {"range": + {"start": {"line": 35, "character": 18}, + "end": {"line": 35, "character": 22}}}] +{"textDocument": + {"uri": "file:///src/tests/interactive/test-cases/refs_across_blocks.lean"}, + "position": {"line": 25, "character": 48}} +[{"targetUri": + "file:///src/tests/interactive/test-cases/refs_across_blocks.lean", + "targetSelectionRange": + {"start": {"line": 33, "character": 2}, "end": {"line": 33, "character": 6}}, + "targetRange": + {"start": {"line": 33, "character": 2}, "end": {"line": 33, "character": 6}}, + "originSelectionRange": + {"start": {"line": 25, "character": 48}, + "end": {"line": 25, "character": 52}}}] +{"textDocument": + {"uri": "file:///src/tests/interactive/test-cases/refs_across_blocks.lean"}, + "position": {"line": 25, "character": 48}} +[{"range": + {"start": {"line": 25, "character": 48}, + "end": {"line": 25, "character": 52}}}, + {"range": + {"start": {"line": 33, "character": 2}, "end": {"line": 33, "character": 6}}}, + {"range": + {"start": {"line": 35, "character": 50}, + "end": {"line": 35, "character": 54}}}] +{"textDocument": + {"uri": "file:///src/tests/interactive/test-cases/refs_across_blocks.lean"}, + "position": {"line": 35, "character": 18}} +[{"targetUri": + "file:///src/tests/interactive/test-cases/refs_across_blocks.lean", + "targetSelectionRange": + {"start": {"line": 31, "character": 1}, "end": {"line": 31, "character": 5}}, + "targetRange": + {"start": {"line": 31, "character": 1}, "end": {"line": 31, "character": 5}}, + "originSelectionRange": + {"start": {"line": 35, "character": 18}, + "end": {"line": 35, "character": 22}}}] +{"textDocument": + {"uri": "file:///src/tests/interactive/test-cases/refs_across_blocks.lean"}, + "position": {"line": 20, "character": 9}} +[{"targetUri": + "file:///src/tests/interactive/test-cases/refs_across_blocks.lean", + "targetSelectionRange": + {"start": {"line": 26, "character": 1}, "end": {"line": 26, "character": 5}}, + "targetRange": + {"start": {"line": 26, "character": 1}, "end": {"line": 26, "character": 5}}, + "originSelectionRange": + {"start": {"line": 20, "character": 9}, + "end": {"line": 20, "character": 13}}}] +{"textDocument": + {"uri": "file:///src/tests/interactive/test-cases/refs_across_blocks.lean"}, + "position": {"line": 20, "character": 9}} +[{"range": + {"start": {"line": 20, "character": 9}, + "end": {"line": 20, "character": 13}}}, + {"range": + {"start": {"line": 26, "character": 1}, "end": {"line": 26, "character": 5}}}] +{"textDocument": + {"uri": "file:///src/tests/interactive/test-cases/refs_across_blocks.lean"}, + "position": {"line": 20, "character": 32}} +[{"range": + {"start": {"line": 20, "character": 32}, + "end": {"line": 20, "character": 36}}}, + {"range": + {"start": {"line": 28, "character": 2}, "end": {"line": 28, "character": 6}}}] +{"textDocument": + {"uri": "file:///src/tests/interactive/test-cases/refs_across_blocks.lean"}, + "position": {"line": 35, "character": 9}} +[{"targetUri": + "file:///src/tests/interactive/test-cases/refs_across_blocks.lean", + "targetSelectionRange": + {"start": {"line": 45, "character": 1}, "end": {"line": 45, "character": 5}}, + "targetRange": + {"start": {"line": 45, "character": 1}, "end": {"line": 45, "character": 5}}, + "originSelectionRange": + {"start": {"line": 35, "character": 9}, + "end": {"line": 35, "character": 13}}}] +{"textDocument": + {"uri": "file:///src/tests/interactive/test-cases/refs_across_blocks.lean"}, + "position": {"line": 35, "character": 9}} +[{"range": + {"start": {"line": 35, "character": 9}, + "end": {"line": 35, "character": 13}}}, + {"range": + {"start": {"line": 45, "character": 1}, "end": {"line": 45, "character": 5}}}, + {"range": + {"start": {"line": 51, "character": 15}, + "end": {"line": 51, "character": 19}}}] +{"textDocument": + {"uri": "file:///src/tests/interactive/test-cases/refs_across_blocks.lean"}, + "position": {"line": 35, "character": 32}} +[{"targetUri": + "file:///src/tests/interactive/test-cases/refs_across_blocks.lean", + "targetSelectionRange": + {"start": {"line": 47, "character": 2}, "end": {"line": 47, "character": 6}}, + "targetRange": + {"start": {"line": 47, "character": 2}, "end": {"line": 47, "character": 6}}, + "originSelectionRange": + {"start": {"line": 35, "character": 32}, + "end": {"line": 35, "character": 36}}}] +{"textDocument": + {"uri": "file:///src/tests/interactive/test-cases/refs_across_blocks.lean"}, + "position": {"line": 35, "character": 32}} +[{"range": + {"start": {"line": 35, "character": 32}, + "end": {"line": 35, "character": 36}}}, + {"range": + {"start": {"line": 47, "character": 2}, "end": {"line": 47, "character": 6}}}] +{"textDocument": + {"uri": "file:///src/tests/interactive/test-cases/refs_across_blocks.lean"}, + "position": {"line": 51, "character": 15}} +[{"targetUri": + "file:///src/tests/interactive/test-cases/refs_across_blocks.lean", + "targetSelectionRange": + {"start": {"line": 45, "character": 1}, "end": {"line": 45, "character": 5}}, + "targetRange": + {"start": {"line": 45, "character": 1}, "end": {"line": 45, "character": 5}}, + "originSelectionRange": + {"start": {"line": 51, "character": 15}, + "end": {"line": 51, "character": 19}}}] +{"textDocument": + {"uri": "file:///src/tests/interactive/test-cases/refs_across_blocks.lean"}, + "position": {"line": 16, "character": 30}} +[{"targetUri": + "file:///src/tests/interactive/test-cases/refs_across_blocks.lean", + "targetSelectionRange": + {"start": {"line": 21, "character": 1}, "end": {"line": 21, "character": 5}}, + "targetRange": + {"start": {"line": 21, "character": 1}, "end": {"line": 21, "character": 5}}, + "originSelectionRange": + {"start": {"line": 16, "character": 30}, + "end": {"line": 16, "character": 34}}}] +{"textDocument": + {"uri": "file:///src/tests/interactive/test-cases/refs_across_blocks.lean"}, + "position": {"line": 16, "character": 30}} +[{"range": + {"start": {"line": 14, "character": 9}, + "end": {"line": 14, "character": 13}}}, + {"range": + {"start": {"line": 16, "character": 30}, + "end": {"line": 16, "character": 34}}}, + {"range": + {"start": {"line": 21, "character": 1}, "end": {"line": 21, "character": 5}}}] +{"textDocument": + {"uri": "file:///src/tests/interactive/test-cases/refs_across_blocks.lean"}, + "position": {"line": 12, "character": 36}} +[{"targetUri": + "file:///src/tests/interactive/test-cases/refs_across_blocks.lean", + "targetSelectionRange": + {"start": {"line": 19, "character": 1}, "end": {"line": 19, "character": 5}}, + "targetRange": + {"start": {"line": 19, "character": 1}, "end": {"line": 19, "character": 5}}, + "originSelectionRange": + {"start": {"line": 12, "character": 34}, + "end": {"line": 12, "character": 38}}}] +{"textDocument": + {"uri": "file:///src/tests/interactive/test-cases/refs_across_blocks.lean"}, + "position": {"line": 12, "character": 36}} +[{"range": + {"start": {"line": 12, "character": 34}, + "end": {"line": 12, "character": 38}}}, + {"range": + {"start": {"line": 19, "character": 1}, "end": {"line": 19, "character": 5}}}] +{"textDocument": + {"uri": "file:///src/tests/interactive/test-cases/refs_across_blocks.lean"}, + "position": {"line": 12, "character": 64}} +[{"targetUri": + "file:///src/tests/interactive/test-cases/refs_across_blocks.lean", + "targetSelectionRange": + {"start": {"line": 21, "character": 2}, "end": {"line": 21, "character": 7}}, + "targetRange": + {"start": {"line": 21, "character": 2}, "end": {"line": 21, "character": 7}}, + "originSelectionRange": + {"start": {"line": 12, "character": 63}, + "end": {"line": 12, "character": 68}}}] +{"textDocument": + {"uri": "file:///src/tests/interactive/test-cases/refs_across_blocks.lean"}, + "position": {"line": 12, "character": 64}} +[{"range": + {"start": {"line": 12, "character": 63}, + "end": {"line": 12, "character": 68}}}, + {"range": + {"start": {"line": 21, "character": 2}, "end": {"line": 21, "character": 7}}}] diff --git a/src/verso-manual/VersoManual/InlineLean.lean b/src/verso-manual/VersoManual/InlineLean.lean index a93054b37..df9ef28e1 100644 --- a/src/verso-manual/VersoManual/InlineLean.lean +++ b/src/verso-manual/VersoManual/InlineLean.lean @@ -175,7 +175,7 @@ meta def reportMessages {m} [Monad m] [MonadLog m] [MonadError m] if messages.hasErrors then throwErrorAt blame "No error expected in code block, one occurred" -def reconstructHighlight (docReconst : DocReconstruction) (key : Export.Key) := +def reconstructHighlight (docReconst : DocReconstruction g) (key : Export.Key) := match docReconst.highlightDeduplication.toHighlighted key with | .error msg => panic! s!"Unable to export key {key}: {msg}" | .ok v => v diff --git a/src/verso-util/VersoUtil.lean b/src/verso-util/VersoUtil.lean index c271eb2a3..5a5fa8c64 100644 --- a/src/verso-util/VersoUtil.lean +++ b/src/verso-util/VersoUtil.lean @@ -5,6 +5,7 @@ Author: David Thrane Christiansen -/ module public import VersoUtil.BinFiles +public import VersoUtil.InfoTree public import VersoUtil.LzCompress public import VersoUtil.WfRec public import VersoUtil.Zip diff --git a/src/verso-util/VersoUtil/InfoTree.lean b/src/verso-util/VersoUtil/InfoTree.lean new file mode 100644 index 000000000..2bedd173e --- /dev/null +++ b/src/verso-util/VersoUtil/InfoTree.lean @@ -0,0 +1,71 @@ +/- +Copyright (c) 2026 Lean FRO LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Author: David Thrane Christiansen +-/ +module +public import Lean.Elab.InfoTree.Types +import Lean.Elab.InfoTree.Main + +set_option doc.verso true + +namespace Verso + +open Lean Elab + +/-- +Folds {name}`f` over the info nodes in {name}`infoState` whose syntax could potentially overlap the +range from {name}`start` to {name}`stop`. Nodes whose source range doesn't overlap the range are +skipped. +-/ +public partial def foldInfoIn (infoState : InfoState) (start stop : String.Pos.Raw) + (f : Info → α → α) (init : α) : α := + infoState.trees.foldl (init := init) fun acc t => go t acc +where + go : InfoTree → α → α + | .context _ t, acc => go t acc + | .node info children, acc => + if mayOverlap info.stx then + children.foldl (init := f info acc) fun acc t => go t acc + else acc + | .hole id, acc => + match infoState.assignment.find? id with + | some t => go t acc + | none => + match infoState.lazyAssignment.find? id with + | some t => go t.get acc + | none => acc + mayOverlap (stx : Syntax) : Bool := + match stx.getRange? with + | some r => r.start ≤ stop && start ≤ r.stop + | none => true + +/-- +Folds {name}`f` over the info nodes in {name}`infoState` whose syntax may contain {name}`pos`. +-/ +public def foldInfoAt (infoState : InfoState) (pos : String.Pos.Raw) + (f : Info → α → α) (init : α) : α := + foldInfoIn infoState pos pos f init + +/-- +Folds {name}`f` over the custom info nodes with data of type {name}`α` in {name}`infoState` whose +syntax could potentially overlap the range from {name}`start` to {name}`stop`. {name}`f` receives +each node's syntax with its data. +-/ +public def foldCustomInfoIn (α : Type) [TypeName α] (infoState : InfoState) + (start stop : String.Pos.Raw) (f : Syntax → α → β → β) (init : β) : β := + foldInfoIn infoState start stop (init := init) fun info acc => + match info with + | .ofCustomInfo ⟨stx, data⟩ => + match data.get? α with + | some x => f stx x acc + | none => acc + | _ => acc + +/-- +Folds {name}`f` over the custom info nodes with data of type {name}`α` in {name}`infoState` whose +syntax may contain {name}`pos`. +-/ +public def foldCustomInfoAt (α : Type) [TypeName α] (infoState : InfoState) (pos : String.Pos.Raw) + (f : Syntax → α → β → β) (init : β) : β := + foldCustomInfoIn α infoState pos pos f init diff --git a/src/verso/Verso/Doc.lean b/src/verso/Verso/Doc.lean index dec7db23c..fcfc514fa 100644 --- a/src/verso/Verso/Doc.lean +++ b/src/verso/Verso/Doc.lean @@ -7,6 +7,7 @@ module public import Lean.Data.Json public import Lean.DocString.Types public import SubVerso.Highlighting +public import Std.Data.HashMap import Verso.Doc.Name set_option doc.verso true @@ -678,8 +679,51 @@ private partial def Part.reprPrec [Repr genre.Inline] [Repr genre.Block] [Repr g public instance [Repr g.Inline] [Repr g.Block] [Repr g.PartMetadata] : Repr (Part g) where reprPrec := private Part.reprPrec -public structure DocReconstruction where +/-- +Document reconstruction data: the document-wide data that a document's blocks look up when the +document is constructed. +-/ +public structure DocReconstruction (genre : Genre) where + /-- The table of highlighted code that the document's code refers to by key. -/ highlightDeduplication : SubVerso.Highlighting.Export + /-- The URL of each of the document's link definitions, by link label. -/ + links : Std.HashMap String String := {} + /-- The contents of each of the document's footnote definitions, by footnote label. -/ + footnotes : Std.HashMap String (Array (Inline genre)) := {} + +/-- +The URL of the link with the label {name}`label`, or the empty string if the document has no such +link. +-/ +public def DocReconstruction.linkUrl (docReconst : DocReconstruction genre) (label : String) : + String := + docReconst.links.getD label "" + +/-- +The contents of the footnote with the label {name}`label`, or the empty array if the document has no +such footnote. +-/ +public def DocReconstruction.footnoteContents (docReconst : DocReconstruction genre) + (label : String) : + Array (Inline genre) := + docReconst.footnotes.getD label #[] + +/-- +Adds a document's link and footnote definitions to the document reconstruction data +{name}`docReconst`. + +Each footnote's contents are computed from document reconstruction data that has all the links and +the footnotes that precede it in {name}`footnotes`. +-/ +public def DocReconstruction.withDefs (docReconst : DocReconstruction genre) + (links : Array (String × String)) + (footnotes : Array (String × (DocReconstruction genre → Array (Inline genre)))) : + DocReconstruction genre := + let docReconst := { docReconst with + links := links.foldl (init := docReconst.links) fun table (label, url) => table.insert label url + } + footnotes.foldl (init := docReconst) fun docReconst (label, contents) => + { docReconst with footnotes := docReconst.footnotes.insert label (contents docReconst) } /-- @@ -689,7 +733,11 @@ into a value by invoking the `VersoDoc.toPart` method. The actual structure of a should not be relied on. -/ public structure VersoDoc (genre : Genre) where - construct : DocReconstruction → Part genre + /-- + Builds the document from its document reconstruction data. The document's own links and footnotes + are added to the data first. + -/ + construct : DocReconstruction genre → Part genre /-- Serialization of the DocReconstruction data structure -/ docReconstructionData : String := "{}" @@ -710,8 +758,8 @@ public def VersoDoc.toPart: VersoDoc genre → Part genre if let .ok highlightJson := json.getObjVal? "highlight" then match SubVerso.Highlighting.Export.fromJson? highlightJson with | .error e => panic! s!"Failed to deserialize Export data from parsed JSON: {e}" - | .ok table => construct ⟨table⟩ - else construct ⟨{}⟩ + | .ok table => construct { highlightDeduplication := table } + else construct { highlightDeduplication := {} } /-- Replace the metadata in a VersoDoc. diff --git a/src/verso/Verso/Doc/Concrete.lean b/src/verso/Verso/Doc/Concrete.lean index 6a220e0ac..9fd52d50d 100644 --- a/src/verso/Verso/Doc/Concrete.lean +++ b/src/verso/Verso/Doc/Concrete.lean @@ -12,6 +12,7 @@ import Verso.Doc public import Verso.Doc.Elab public meta import Verso.Doc.Elab.Monad import Verso.Doc.Concrete.InlineString +public import Verso.Doc.Concrete.Environment import Verso.Doc.Lsp namespace Verso.Doc.Concrete @@ -64,15 +65,6 @@ meta partial def findGenreTm : Syntax → TermElabM Unit meta partial def findGenreCmd (genre : Syntax) : Command.CommandElabM Unit := Command.runTermElabM fun _ => findGenreTm genre -meta def saveRefs [Monad m] [MonadInfoTree m] (st : DocElabM.State) (st' : PartElabM.State) : m Unit := do - for r in internalRefs st'.linkDefs st.linkRefs do - for stx in r.syntax do - pushInfoLeaf <| .ofCustomInfo {stx := stx , value := Dynamic.mk r} - for r in internalRefs st'.footnoteDefs st.footnoteRefs do - for stx in r.syntax do - pushInfoLeaf <| .ofCustomInfo {stx := stx , value := Dynamic.mk r} - - open PartElabM in /-- All-at-once elaboration of verso document syntax to syntax denoting a verso `VersoDoc`. Implements @@ -105,7 +97,6 @@ private meta def elabDoc (genre: Term) (title: StrLit) (topLevelBlocks : Array S | .error stx msg => logErrorAt stx msg | oops@(.internal _ _) => throw oops pure () - saveRefs docElabState partElabState let finished := partElabState.partContext.toPartFrame.close endPos @@ -278,20 +269,6 @@ where else s -/-- -As we elaborate a `#doc` command top-level-block by top-level-block, the Lean environment will -be used to thread state between the separate top level blocks. These environment extensions contain -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 #[]) (.node .none nullKind #[]) -deriving Inhabited - -public meta initialize docEnvironmentExt : EnvExtension DocElabEnvironment ← registerEnvExtension (pure {}) - /-- The original parser for the `command` category, which is restored while elaborating a Verso block so that nested Lean code has the correct syntax. @@ -317,10 +294,6 @@ private meta def runPartElabInEnv (act : PartElabM a) : Command.CommandElabM a : finally modifyEnv (categoryParserFnExtension.setState · versoCmdFn) -private meta def saveRefsInEnv : Command.CommandElabM Unit := do - let versoEnv := docEnvironmentExt.getState (← getEnv) - saveRefs versoEnv.docState versoEnv.partState - /-! When we do incremental parsing of `#doc` commands, we split the behaviors that are done all at once in `elabDoc` across three functions: the prelude in `startDoc`, the loop body in `runVersoBlock`, @@ -343,13 +316,14 @@ private meta def startDoc (genreSyntax : Term) (title: StrLit) : Command.Command private meta def runVersoBlock (block : TSyntax `block) : Command.CommandElabM Unit := do runPartElabInEnv <| partCommand block - -- This calls pushInfoLeaf a quadratic number of times for a for a linear number of top-level - -- verso blocks, which should be harmless but may be inefficient. It may be desirable to tag - -- info leaves that have already been pushed to avoid pushing them again. - saveRefsInEnv open PartElabM in -private meta def finishDoc : Command.CommandElabM Unit:= do +/-- +Finishes the document: closes its parts, checks its links and footnotes, and defines the document +constant. {name}`commandStart?` is the start of the current command, which is the document's last +top-level block. It is absent when the document has no blocks. +-/ +private meta def finishDoc (commandStart? : Option String.Pos.Raw := none) : Command.CommandElabM Unit:= do let endPos := (← getFileMap).source.rawEndPos runPartElabInEnv <| do closePartsUntil 0 endPos @@ -360,6 +334,7 @@ private meta def finishDoc : Command.CommandElabM Unit:= do -- The `_root_` prefix ensures that the installed identifier will ignore any ambient namespaces let n := mkIdent (`_root_ ++ (← currentDocName)) let doc ← Command.runTermElabM fun _ => finished.toVersoDoc versoEnv.genreSyntax versoEnv.ctx versoEnv.docState versoEnv.partState + (commandStart? := commandStart?) let ty ← ``(VersoDoc $versoEnv.genreSyntax) Command.elabCommand (← `(public def $n : $ty := $doc)) @@ -419,8 +394,10 @@ public meta def elabVersoBlock : Command.CommandElab @[command_elab addLastBlockCmd] public meta def elabVersoLastBlock : Command.CommandElab | `(addLastBlockCmd| $b:block) => do + let commandStart? := lastVersoEndPosExt.getState (← getEnv) updatePos b - runVersoBlock b - -- Finish up the document - finishDoc + -- Verso finishes the document even when its last block fails. An interrupt is rethrown, and then + -- Verso does not finish the document. + withLogging <| runVersoBlock b + finishDoc commandStart? | _ => throwUnsupportedSyntax diff --git a/src/verso/Verso/Doc/Concrete/Environment.lean b/src/verso/Verso/Doc/Concrete/Environment.lean new file mode 100644 index 000000000..ff600828c --- /dev/null +++ b/src/verso/Verso/Doc/Concrete/Environment.lean @@ -0,0 +1,27 @@ +/- +Copyright (c) 2023-2026 Lean FRO LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Author: David Thrane Christiansen +-/ +module +public import Lean.Environment +public meta import Lean.Elab.Term +public meta import Verso.Doc.Elab.Monad + +namespace Verso.Doc.Concrete + +open Lean Verso Doc Elab + +/-- +The elaboration state of a `#doc` document that persists from one top-level block to the next. +Each top-level block is a separate Lean command, so the environment extension `docEnvironmentExt` +stores this state. +-/ +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 #[]) (.node .none nullKind #[]) +deriving Inhabited + +public meta initialize docEnvironmentExt : EnvExtension DocElabEnvironment ← registerEnvExtension (pure {}) diff --git a/src/verso/Verso/Doc/Elab.lean b/src/verso/Verso/Doc/Elab.lean index c204bfb23..e41b07328 100644 --- a/src/verso/Verso/Doc/Elab.lean +++ b/src/verso/Verso/Doc/Elab.lean @@ -159,17 +159,17 @@ public meta def _root_.Lean.Doc.Syntax.link.expand : InlineExpander match dest with | `(link_target| ( $url )) => pure (↑ url) - | `(link_target| [ $ref ]) => do + | `(link_target| [ $labelStx ]) => do -- Round-trip through quote to get rid of source locations, preventing unwanted IDE info - addLinkRef ref + addLinkRef labelStx | _ => throwErrorAt dest "Couldn't parse link destination" ``(Inline.link #[$[$(← txt.mapM elabInline)],*] $url) | _ => throwUnsupportedSyntax @[inline_expander Lean.Doc.Syntax.footnote] public meta def _root_.Lean.Doc.Syntax.link.footnote : InlineExpander - | `(inline| footnote( $name:str )) => do - ``(Inline.footnote $(quote name.getString) $(← addFootnoteRef name)) + | `(inline| footnote( $labelStx:str )) => do + ``(Inline.footnote $(quote labelStx.getString) $(← addFootnoteRef labelStx)) | _ => throwUnsupportedSyntax @@ -181,9 +181,9 @@ public meta def _root_.Lean.Doc.Syntax.image.expand : InlineExpander match dest with | `(link_target| ( $url )) => pure (↑ url) - | `(link_target| [ $ref ]) => do + | `(link_target| [ $labelStx ]) => do -- Round-trip through quote to get rid of source locations, preventing unwanted IDE info - addLinkRef ref + addLinkRef labelStx | _ => throwErrorAt dest "Couldn't parse link destination" ``(Inline.image $(quote altText) $url) | _ => throwUnsupportedSyntax @@ -244,14 +244,22 @@ where @[part_command Lean.Doc.Syntax.footnote_ref] public meta partial def _root_.Lean.Doc.Syntax.footnote_ref.command : PartCommand - | `(block| [^ $name:str ]: $contents* ) => - addFootnoteDef name =<< contents.mapM (withRefsAllowed .onlyIfDefined <| elabInline ·) + | `(block| [^ $labelStx:str ]: $contents* ) => do + let before := (← getThe DocElabM.State).footnoteRefs + let contents ← contents.mapM (elabInline ·) + -- The footnote uses in the contents are tracked so we can check for cycles when finishing the doc + let mut contentUses := #[] + for (label, uses) in (← getThe DocElabM.State).footnoteRefs do + let known := before[label]?.map (·.useSites.size) |>.getD 0 + for use in uses.useSites.extract known do + contentUses := contentUses.push (label, use) + addFootnoteDef labelStx contents contentUses | _ => throwUnsupportedSyntax @[part_command Lean.Doc.Syntax.link_ref] public meta partial def _root_.Lean.Doc.Syntax.link_ref.command : PartCommand - | `(block| [ $name:str ]: $url:str ) => - addLinkDef name url.getString + | `(block| [ $labelStx:str ]: $url:str ) => + addLinkDef labelStx url.getString | _ => throwUnsupportedSyntax partial def PartElabM.State.close (endPos : String.Pos.Raw) (state : PartElabM.State) : Option PartElabM.State := diff --git a/src/verso/Verso/Doc/Elab/Basic.lean b/src/verso/Verso/Doc/Elab/Basic.lean index 1816f7f7c..81c70c3f6 100644 --- a/src/verso/Verso/Doc/Elab/Basic.lean +++ b/src/verso/Verso/Doc/Elab/Basic.lean @@ -109,10 +109,16 @@ public def PartFrame.close (fr : PartFrame) (endPos : String.Pos.Raw) : Finished .mk fr.rangeSyntax fr.selectionSyntax titleInlines titlePreview fr.metadata fr.blocks fr.priorParts endPos -/-- References that must be local to the current blob of concrete document syntax -/ +/-- A link or footnote definition in a document. -/ public structure DocDef (α : Type) where - defSite : TSyntax `str + /-- The syntax of the defined label. -/ + labelStx : TSyntax `str + /-- The defined value. -/ val : α + /-- The name of the file that contains the definition. -/ + fileName : String + /-- The position of the definition's label in its file. -/ + position : Position deriving Repr public structure DocUses where @@ -162,24 +168,31 @@ Makes the frame {name}`fr` the current frame. The former current frame is saved public def PartContext.push (ctxt : PartContext) (fr : PartFrame) : PartContext := ⟨fr, ctxt.parents.push ctxt.toPartFrame⟩ -/-- Custom info tree data to save footnote and reflink cross-references -/ +/-- Distinguishes links from footnotes. -/ +public inductive DocRefKind where + | link + | footnote +deriving Repr, BEq, Inhabited + +/-- +Custom info tree data for one definition or use of a link or footnote. The info node's syntax is +the label in the definition or use. +-/ public structure DocRefInfo where - defSite : Option Syntax - useSites : Array Syntax + kind : DocRefKind + label : String + /-- + The start of the document that contains the definition or use. It identifies the document within + its file. + -/ + documentPos? : Option String.Pos.Raw + /-- {lean}`true` for a definition, and {lean}`false` for a use. -/ + isDef : Bool deriving TypeName, Repr -public def DocRefInfo.syntax (dri : DocRefInfo) : Array Syntax := - (dri.defSite.map (#[·])|>.getD #[]) ++ dri.useSites - -public def internalRefs (defs : HashMap String (DocDef α)) (refs : HashMap String DocUses) : Array DocRefInfo := Id.run do - let keys : HashSet String := defs.fold (fun soFar k _ => HashSet.insert soFar k) <| refs.fold (fun soFar k _ => soFar.insert k) {} - let mut refInfo := #[] - for k in keys do - refInfo := refInfo.push { - defSite := defs[k]? |>.map (·.defSite), - useSites := refs[k]? |>.map (·.useSites) |>.getD #[] - } - refInfo +/-- Whether two definitions or uses are of the same link or footnote of the same document. -/ +public def DocRefInfo.sameRef (r1 r2 : DocRefInfo) : Bool := + r1.kind == r2.kind && r1.label == r2.label && r1.documentPos? == r2.documentPos? /-- Custom info tree data to save the locations and identities of lists -/ public structure DocListInfo where diff --git a/src/verso/Verso/Doc/Elab/Monad.lean b/src/verso/Verso/Doc/Elab/Monad.lean index 49d2d879f..fd03e76c6 100644 --- a/src/verso/Verso/Doc/Elab/Monad.lean +++ b/src/verso/Verso/Doc/Elab/Monad.lean @@ -37,18 +37,6 @@ initialize registerTraceClass `Elab.Verso initialize registerTraceClass `Elab.Verso.part initialize registerTraceClass `Elab.Verso.block -class HasLink (name : String) (doc : Name) where - url : String - -class HasNote (name : String) (doc : Name) (genre : Genre) where - contents : Array (Inline genre) - -private def linkRefName [Monad m] [MonadQuotation m] (docName : Name) (ref : TSyntax `str) : m Term := do - ``(HasLink.url $(quote ref.getString) $(quote docName)) - -private def footnoteRefName [Monad m] [MonadQuotation m] (genre : Term) (docName : Name) (ref : TSyntax `str) : m Term := - ``(HasNote.contents $(quote ref.getString) $(quote docName) (genre := $genre)) - -- For use in IDE features and previews and such @[inline_to_string Lean.Doc.Syntax.text] @@ -181,6 +169,8 @@ public structure PartElabM.State where partContext : PartContext linkDefs : HashMap String (DocDef String) := {} footnoteDefs : HashMap String (DocDef (Array (TSyntax `term))) := {} + /-- The footnote uses in each footnote's contents, by the footnote's label. -/ + footnoteUses : HashMap String (Array (String × Syntax)) := {} deferredBlocks : Array (Name × Term) := #[] deriving Inhabited @@ -337,11 +327,11 @@ public partial def PartElabM.closePartsUntil (outer : Nat) (endPos : String.Pos. | none => pure () /-- -Adds a block (syntax denoting a function {lit}`Block g`)to the elaboration state. +Adds a block (syntax denoting a {lit}`Block g`) to the elaboration state. -If some {name}`blockInternalDocReconstructionPlaceholder` is given to represent unresolved free -references to a {lean}`DocReconstruction` object within this block, captures those references with a -function argument. +The block becomes a function of document reconstruction data. The function's parameter is +{name}`blockInternalDocReconstructionPlaceholder` if it is given, and otherwise the current +{name}`DocElabContext`'s {name}`DocElabContext.docReconstructionPlaceholder`. -/ public def PartElabM.addBlock (block : TSyntax `term) (blockInternalDocReconstructionPlaceholder : Option Ident := .none) : PartElabM Unit := do -- The syntax denoting the top-level Part structure will refer to this block by name, passing it @@ -354,7 +344,7 @@ public def PartElabM.addBlock (block : TSyntax `term) (blockInternalDocReconstru -- If the internal block includes a doc reconstruction placeholder, it should be different from -- the one in the current `DocElabContext` to maintain good hygiene. let blockDefSyntax ← match blockInternalDocReconstructionPlaceholder with - | .none => `(fun _ => $block) + | .none => `(fun $docReconstructionPlaceholder => $block) | .some name => `(fun $name => $block) modifyThe PartElabM.State fun st => @@ -366,87 +356,197 @@ public def PartElabM.addBlock (block : TSyntax `term) (blockInternalDocReconstru public def PartElabM.addPart (finished : FinishedPart) : PartElabM Unit := modifyThe State fun st => { st with partContext.priorParts := st.partContext.priorParts.push finished } -public def PartElabM.addLinkDef (refName : TSyntax `str) (url : String) : PartElabM Unit := do - let strName := refName.getString - let docName ← currentDocName - match (← getThe State).linkDefs[strName]? with - | none => - let t := mkApp2 (.const ``HasLink []) (toExpr strName) (toExpr docName) - let n ← mkFreshUserName (docName ++ `inst.link ++ strName.toName) - addAndCompile <| .defnDecl { - name := n, - levelParams := [], - type := t, - value := mkApp3 (.const ``HasLink.mk []) (toExpr strName) (toExpr docName) (toExpr url), - hints := .abbrev, - safety := .safe - } - setReducibilityStatus n .implicitReducible - Meta.addInstance n AttributeKind.global (eval_prio default) - modifyThe State fun st => {st with linkDefs := st.linkDefs.insert strName ⟨refName, url⟩} +/-- +The start of the document under construction. It identifies the document within its file. +-/ +public def PartElabM.State.documentPos? (state : PartElabM.State) : Option String.Pos.Raw := + let root := state.partContext.parents[0]?.getD state.partContext.toPartFrame + root.rangeSyntax.getPos? + +/-- +Records a definition or use of a link or footnote in the info tree, for editor features. +-/ +def pushDocRefInfo [Monad m] [MonadInfoTree m] + (state : PartElabM.State) (kind : DocRefKind) (labelStx : TSyntax `str) (isDef : Bool) : m Unit := + let info : DocRefInfo := + { kind, label := labelStx.getString, documentPos? := state.documentPos?, isDef } + pushInfoLeaf <| .ofCustomInfo { stx := labelStx, value := Dynamic.mk info } + +/-- +Describes the location of the definition {name}`d`. The file name is included when it differs from +the current file. +-/ +def describeDefLocation {α : Type} (d : DocDef α) : PartElabM MessageData := do + let lineCol := m!"line {d.position.line}, column {d.position.column}" + if d.fileName == (← getFileName) then + return lineCol + else + return m!"{lineCol} of {d.fileName}" + +/-- A definition of the label {name}`labelStx` with the value {name}`val`, in the current file. -/ +def PartElabM.mkDocDef {α : Type} (labelStx : TSyntax `str) (val : α) : PartElabM (DocDef α) := do + let position := (← getFileMap).toPosition (labelStx.raw.getPos?.getD 0) + return { labelStx, val, fileName := ← getFileName, position } - | some ⟨_, url'⟩ => - throwErrorAt refName "Already defined link [{strName}] as '{url'}'" +/-- +Records the definition of the link whose label is {name}`labelStx`. A second definition of the same +label in one document is an error. +-/ +public def PartElabM.addLinkDef (labelStx : TSyntax `str) (url : String) : PartElabM Unit := do + let label := labelStx.getString + match (← getThe State).linkDefs[label]? with + | none => + let d ← mkDocDef labelStx url + modifyThe State fun st => {st with linkDefs := st.linkDefs.insert label d} + pushDocRefInfo (← getThe State) .link labelStx (isDef := true) + | some prev => + throwErrorAt labelStx + m!"Duplicate definition of link label [{label}]. It is already defined at {← describeDefLocation prev}, with the URL '{prev.val}'. This definition has the URL '{url}'." -public def DocElabM.addLinkRef (refName : TSyntax `str) : DocElabM (TSyntax `term) := do - let strName := refName.getString +/-- +Records a use of the link whose label is {name}`labelStx`, and returns a term for its URL. +-/ +public def DocElabM.addLinkRef (labelStx : TSyntax `str) : DocElabM (TSyntax `term) := do + let label := labelStx.getString match (← readThe DocElabContext).refsAllowed with | .always => pure () | .onlyIfDefined => - if !(← readThe PartElabM.State).linkDefs.contains strName then - throwErrorAt refName m!"Link reference [{strName}] does not have a definition" + if !(← readThe PartElabM.State).linkDefs.contains label then + throwErrorAt labelStx m!"Link reference [{label}] does not have a definition" + let .some docReconst := (← readThe DocElabContext).docReconstructionPlaceholder + | throwErrorAt labelStx m!"The link label [{label}] can't be used here, because this text is elaborated outside of a document" - match (← getThe State).linkRefs[strName]? with - | none => - modifyThe State fun st => {st with linkRefs := st.linkRefs.insert strName ⟨#[refName]⟩} - linkRefName (← currentDocName) refName - | some ⟨uses⟩ => - modifyThe State fun st => {st with linkRefs := st.linkRefs.insert strName ⟨uses.push refName⟩} - linkRefName (← currentDocName) refName - - -public def PartElabM.addFootnoteDef (refName : TSyntax `str) (content : Array (TSyntax `term)) : PartElabM Unit := do - let strName := refName.getString - let docName ← currentDocName - let genre := (← readThe DocElabContext).genre - match (← getThe State).footnoteDefs[strName]? with + modifyThe State fun st => + {st with linkRefs := st.linkRefs.insert label ((st.linkRefs.getD label {}).add labelStx)} + pushDocRefInfo (← readThe PartElabM.State) .link labelStx (isDef := false) + ``(DocReconstruction.linkUrl $docReconst $(quote label)) + +/-- +Elaborates a footnote's contents to check them, and reports their errors. Returns {lean}`true` when +the contents have no errors. The elaborated term is discarded, and the info tree is left unchanged. +-/ +def PartElabM.checkFootnoteContents (content : Array (TSyntax `term)) : PartElabM Bool := do + let ctx ← readThe DocElabContext + let .some docReconst := ctx.docReconstructionPlaceholder + | throwError "No doc reconstruction placeholder available" + let genre : Term := ⟨ctx.genreSyntax⟩ + let stx ← ``(fun ($docReconst : DocReconstruction $genre) => (#[$content,*] : Array (Doc.Inline $genre))) + let act : TermElabM Bool := withEnableInfoTree false do + try + let e ← Term.elabTerm stx none + Term.synthesizeSyntheticMVarsNoPostponing + return !(← instantiateMVars e).hasSyntheticSorry + catch ex => + logException ex + return false + act + +/-- +Records the definition of the footnote whose label is {name}`labelStx`, with the contents +{name}`content`, which are terms that denote inlines. A second definition of the same label in one +document is an error. + +The contents are checked here, so that their errors appear at the definition. Contents with errors +are recorded as empty. + +{name}`contentUses` are the footnote uses in the contents, each paired with its label. +-/ +public def PartElabM.addFootnoteDef (labelStx : TSyntax `str) (content : Array (TSyntax `term)) + (contentUses : Array (String × Syntax) := #[]) : PartElabM Unit := do + let label := labelStx.getString + match (← getThe State).footnoteDefs[label]? with | none => - let t := mkApp3 (.const ``HasNote []) (toExpr strName) (toExpr docName) genre - let n ← mkFreshUserName (docName ++ `inst.note ++ strName.toName) - let inlTy := Expr.app (.const ``Doc.Inline []) genre - let inls ← Term.elabTerm (← `(#[$content,*])) (some (.app (.const ``Array [0]) inlTy)) - let inls ← instantiateMVars inls - addAndCompile <| .defnDecl { - name := n, - levelParams := [], - type := t, - value := mkApp4 (.const ``HasNote.mk []) (toExpr strName) (toExpr docName) genre inls, - hints := .abbrev, - safety := .safe + let content := if ← checkFootnoteContents content then content else #[] + let d ← mkDocDef labelStx content + modifyThe State fun st => { st with + footnoteDefs := st.footnoteDefs.insert label d + footnoteUses := st.footnoteUses.insert label contentUses } - setReducibilityStatus n .implicitReducible - Meta.addInstance n AttributeKind.global (eval_prio default) - modifyThe State fun st => {st with footnoteDefs := st.footnoteDefs.insert strName ⟨refName, content⟩} - | some _ => - throwErrorAt refName m!"Already defined footnote [^{strName}]" - -public def DocElabM.addFootnoteRef (refName : TSyntax `str) : DocElabM (TSyntax `term) := do - let strName := refName.getString - let genre := (← readThe DocElabContext).genreSyntax + pushDocRefInfo (← getThe State) .footnote labelStx (isDef := true) + | some prev => + throwErrorAt labelStx + m!"Duplicate definition of footnote label [^{label}]. It is already defined at {← describeDefLocation prev}." + +/-- +Records a use of the footnote whose label is {name}`labelStx`, and returns a term for its contents. +-/ +public def DocElabM.addFootnoteRef (labelStx : TSyntax `str) : DocElabM (TSyntax `term) := do + let label := labelStx.getString match (← readThe DocElabContext).refsAllowed with | .always => pure () | .onlyIfDefined => - if !(← readThe PartElabM.State).footnoteDefs.contains strName then - throwErrorAt refName m!"Footnote reference [^{strName}] does not have a definition" + if !(← readThe PartElabM.State).footnoteDefs.contains label then + throwErrorAt labelStx m!"Footnote reference [^{label}] does not have a definition" + let .some docReconst := (← readThe DocElabContext).docReconstructionPlaceholder + | throwErrorAt labelStx m!"The footnote label [^{label}] can't be used here, because this text is elaborated outside of a document" - match (← getThe State).footnoteRefs[strName]? with - | none => - modifyThe State fun st => {st with footnoteRefs := st.footnoteRefs.insert strName ⟨#[refName]⟩} - footnoteRefName ⟨genre⟩ (← currentDocName) refName - | some ⟨uses⟩ => - modifyThe State fun st => {st with footnoteRefs := st.footnoteRefs.insert strName ⟨uses.push refName⟩} - footnoteRefName ⟨genre⟩ (← currentDocName) refName + modifyThe State fun st => + {st with footnoteRefs := st.footnoteRefs.insert label ((st.footnoteRefs.getD label {}).add labelStx)} + pushDocRefInfo (← readThe PartElabM.State) .footnote labelStx (isDef := false) + ``(DocReconstruction.footnoteContents $docReconst $(quote label)) + +/-- +Orders the labels of a document's footnotes so that each footnote comes after the footnotes that its +contents use. Also returns each use that makes a footnote's contents use the footnote itself, +directly or through other footnotes. Each of these uses is paired with its label and with the labels +of the other footnotes in the cycle, in the order of the cycle. +-/ +public partial def footnoteOrder (partElabState : PartElabM.State) : + Array String × Array (String × Array String × Syntax) := + let labels := partElabState.footnoteDefs.toArray.mergeSort (fun (_, d1) (_, d2) => + d1.labelStx.raw.getPos?.getD 0 ≤ d2.labelStx.raw.getPos?.getD 0) |>.map (·.1) + let (_, _, order, cycles) := labels.foldl (init := ({}, #[], #[], #[])) fun st label => visit label st + (order, cycles) +where + -- `active` holds the labels of the footnotes being visited, from the outermost to the innermost. + visit (label : String) : + HashSet String × Array String × Array String × Array (String × Array String × Syntax) → + HashSet String × Array String × Array String × Array (String × Array String × Syntax) + | (done, active, order, cycles) => + if done.contains label then (done, active, order, cycles) else + let st := (partElabState.footnoteUses.getD label #[]).foldl (init := (done, active.push label, order, cycles)) + fun (done, active, order, cycles) (used, useStx) => + if !partElabState.footnoteDefs.contains used then (done, active, order, cycles) + else match active.idxOf? used with + | some i => (done, active, order, cycles.push (used, active.extract (i + 1) active.size, useStx)) + | none => visit used (done, active, order, cycles) + let (done, active, order, cycles) := st + (done.insert label, active.pop, order.push label, cycles) +/-- +Compares a document's link and footnote uses with its definitions. Each use without a definition +results in an error, and each definition without a use results in a warning. Cyclic footnotes result +in an error as well. The messages are in source order. +-/ +public def checkLinksAndFootnotes (docElabState : DocElabM.State) (partElabState : PartElabM.State) : + Array (Syntax × MessageSeverity × MessageData) := Id.run do + let mut msgs := #[] + for (label, uses) in docElabState.footnoteRefs do + if !partElabState.footnoteDefs.contains label then + for use in uses.useSites do + msgs := msgs.push (use, .error, m!"No definition for footnote [^{label}]") + for (label, d) in partElabState.footnoteDefs do + if !docElabState.footnoteRefs.contains label then + msgs := msgs.push (d.labelStx.raw, .warning, m!"Unused footnote [^{label}]") + for (label, uses) in docElabState.linkRefs do + if !partElabState.linkDefs.contains label then + for use in uses.useSites do + msgs := msgs.push (use, .error, m!"No definition for link [{label}]") + for (label, d) in partElabState.linkDefs do + if !docElabState.linkRefs.contains label then + msgs := msgs.push (d.labelStx.raw, .warning, m!"Unused link [{label}]") + for (label, path, use) in (footnoteOrder partElabState).2 do + msgs := msgs.push (use, .error, m!"Footnote [^{label}] is used inside its own contents{through path}") + return msgs.mergeSort fun (stx1, _) (stx2, _) => startPos stx1 ≤ startPos stx2 +where + startPos (stx : Syntax) : Nat := stx.getPos?.map (·.byteIdx) |>.getD 0 + -- ", through [^b]", ", through [^b] and [^c]", or ", through [^b], [^c] and [^d]" + through (path : Array String) : String := + let labels := path.toList.map (s!"[^{·}]") + match labels.reverse with + | [] => "" + | [l] => s!", through {l}" + | last :: rest => s!", through {", ".intercalate rest.reverse} and {last}" public def PartElabM.push (fr : PartFrame) : PartElabM Unit := modifyThe State fun st => {st with partContext := st.partContext.push fr} @@ -484,38 +584,44 @@ public opaque inlineExpandersFor (x : Name) : DocElabM (Array InlineExpander) /-- Creates a term denoting a {lean}`VersoDoc` value from a {lean}`FinishedPart`. This is the final step in turning a parsed verso doc into syntax. + +It also reports the document's undefined and unused links and footnotes, and compiles the document's +blocks. + +{name}`commandStart?` is the start of the command that finishes the document. It is used when the +command's syntax has no source range. -/ public def FinishedPart.toVersoDoc (genreSyntax : Term) (finished : FinishedPart) (ctx : DocElabContext) (docElabState : DocElabM.State) - (partElabState : PartElabM.State) : + (partElabState : PartElabM.State) + (commandStart? : Option String.Pos.Raw := none) : TermElabM Term := do - -- Check internal refs - for (ref, uses) in docElabState.footnoteRefs do - if !partElabState.footnoteDefs.contains ref then - for use in uses.useSites do - throwErrorAt use m!"No definition for footnote [^{ref}]" - for (ref, site) in partElabState.footnoteDefs do - if !docElabState.footnoteRefs.contains ref then - logWarningAt site.defSite m!"Unused footnote [^{ref}]" - - for (ref, uses) in docElabState.linkRefs do - if !partElabState.linkDefs.contains ref then - for use in uses.useSites do - throwErrorAt use m!"No definition for link [{ref}]" - for (ref, site) in partElabState.linkDefs do - if !docElabState.linkRefs.contains ref then - logWarningAt site.defSite m!"Unused link [{ref}]" + -- Lean suppresses the elaboration errors of a command with a parse error. Messages about syntax + -- outside the current command are logged with this suppression turned off. This way, a parse + -- error in the last block of a `#doc` document leaves the messages about earlier blocks visible. + -- When the command's syntax has no source range, `commandStart?` gives its start. + let cmdRange? := (← getRef).getRange? + for (stx, severity, msg) in checkLinksAndFootnotes docElabState partElabState do + let outsideCommand := match cmdRange?, commandStart?, stx.getPos? with + | some r, _, some pos => !(r.start ≤ pos && pos ≤ r.stop) + | none, some start, some pos => pos < start + | _, _, _ => false + if outsideCommand then + withTheReader Core.Context ({ · with suppressElabErrors := false }) <| + logAt stx msg severity + else + logAt stx msg severity -- Add and compile blocks for (name, block) in partElabState.deferredBlocks do withRef block do withCurrHeartbeats do -- reset the heartbeat count for each block addAndCompile - let mut type ← Term.elabType (← ``(DocReconstruction → Doc.Block $genreSyntax)) + let mut type ← Term.elabType (← ``(DocReconstruction $genreSyntax → Doc.Block $genreSyntax)) let mut blockExpr ← Term.elabTerm block (some type) -- Wrap auto-bound implicits and global variables (this is possibly overly defensive) @@ -551,7 +657,32 @@ public def FinishedPart.toVersoDoc | .none => Json.mkObj [] | .some table => Json.mkObj [("highlight", table.toExport.toJson)] - ``(VersoDoc.mk (fun $docReconstructionPlaceholder => $finishedSyntax) $(quote reconstJson.compress)) + let body ← refTables genreSyntax docReconstructionPlaceholder partElabState finishedSyntax + ``(VersoDoc.mk (fun $docReconstructionPlaceholder => $body) $(quote reconstJson.compress)) +where + /-- + Wraps {name}`body` so that the document reconstruction data {name}`docReconst` also holds the + document's link table and footnote table. + Each footnote's contents can use the links. Footnotes are added in the order of + {name}`footnoteOrder`, so each footnote comes after its footnote dependencies. + -/ + refTables (genreSyntax : Term) (docReconst : Ident) (partElabState : PartElabM.State) (body : Term) : + TermElabM Term := do + if partElabState.linkDefs.isEmpty && partElabState.footnoteDefs.isEmpty then + return body + let links ← (inSourceOrder partElabState.linkDefs).mapM fun (label, d) => + ``(($(quote label), $(quote d.val))) + let footnotes ← (footnoteOrder partElabState).1.filterMapM fun label => do + let some d := partElabState.footnoteDefs[label]? | return none + some <$> ``(($(quote label), + fun ($docReconst : DocReconstruction $genreSyntax) => + (#[$(d.val),*] : Array (Doc.Inline $genreSyntax)))) + let tables ← ``(DocReconstruction.withDefs $docReconst #[$links,*] #[$footnotes,*]) + `(let $docReconst := $tables + $body) + inSourceOrder {α : Type} (defs : HashMap String (DocDef α)) : Array (String × DocDef α) := + defs.toArray.mergeSort fun (_, d1) (_, d2) => + d1.labelStx.raw.getPos?.getD 0 ≤ d2.labelStx.raw.getPos?.getD 0 public abbrev BlockExpander := Syntax → DocElabM (TSyntax `term) diff --git a/src/verso/Verso/Doc/Lsp.lean b/src/verso/Verso/Doc/Lsp.lean index 42ed13daa..793cbdc6a 100644 --- a/src/verso/Verso/Doc/Lsp.lean +++ b/src/verso/Verso/Doc/Lsp.lean @@ -18,6 +18,8 @@ import Lean.DocString.Syntax public meta import Verso.Hover public meta import Verso.Doc.PointOfInterest public meta import Verso.Doc.Name +public meta import Verso.Doc.Concrete.Environment +public meta import VersoUtil.InfoTree namespace Verso.Lsp @@ -131,6 +133,77 @@ meta partial instance : FromJson Lean.Lsp.DocumentSymbolResult where pure ⟨syms⟩ +/-- +The link and footnote definitions and uses in the info trees found in `snaps`, each with the syntax +of its label. +-/ +meta def docRefs (snaps : List Lean.Server.Snapshots.Snapshot) : Array (Syntax × DocRefInfo) := + snaps.foldl (init := #[]) fun acc snap => + snap.infoTree.foldInfo (init := acc) fun _ctxt info acc => + match info with + | .ofCustomInfo ⟨stx, data⟩ => + if let some i := data.get? DocRefInfo then acc.push (stx, i) else acc + | _ => acc + +/-- +All the custom info data of type `α` in `snap` whose syntax contains `pos`, paired with its syntax. +-/ +meta def customInfoAt (α : Type) [TypeName α] (snap : Lean.Server.Snapshots.Snapshot) + (pos : String.Pos.Raw) : Array (Syntax × α) := + Verso.foldCustomInfoAt α snap.cmdState.infoState pos (init := #[]) fun stx x acc => + if stx.containsPos pos then acc.push (stx, x) else acc + +/-- The link and footnote definitions and uses in `snap` whose labels contain `pos`. -/ +meta def docRefsAt (snap : Lean.Server.Snapshots.Snapshot) (pos : String.Pos.Raw) : + Array (Syntax × DocRefInfo) := + customInfoAt DocRefInfo snap pos + +/-- +Every link and footnote definition and use that the `#doc` document whose state is in the extension +in `env` has recorded so far. Each is paired with the syntax of its label at that location. +-/ +meta def envDocRefs (env : Environment) : Array (Syntax × DocRefInfo) := Id.run do + let st := Verso.Doc.Concrete.docEnvironmentExt.getState env + let documentPos? := st.partState.documentPos? + let mut out := #[] + for (label, d) in st.partState.linkDefs do + out := out.push (d.labelStx.raw, { kind := .link, label, documentPos?, isDef := true }) + for (label, d) in st.partState.footnoteDefs do + out := out.push (d.labelStx.raw, { kind := .footnote, label, documentPos?, isDef := true }) + for (label, uses) in st.docState.linkRefs do + for use in uses.useSites do + out := out.push (use, { kind := .link, label, documentPos?, isDef := false }) + for (label, uses) in st.docState.footnoteRefs do + for use in uses.useSites do + out := out.push (use, { kind := .footnote, label, documentPos?, isDef := false }) + return out + +open Lean Server RequestM in +/-- +The definitions and uses of the links and footnotes in `here`, in source order. The entries of +`here` are from the snapshot `snap`. Each source range appears once in the result. +-/ +meta def relatedDocRefs (snap : Lean.Server.Snapshots.Snapshot) (here : Array (Syntax × DocRefInfo)) : + RequestM (Array (Syntax × DocRefInfo)) := do + if here.isEmpty then return #[] + let (snaps, _, _) ← (← readDoc).cmdSnaps.getFinishedPrefix + let env := snaps.getLast?.getD snap |>.env + let envDocumentPos? := (Verso.Doc.Concrete.docEnvironmentExt.getState env).partState.documentPos? + let refs := + if envDocumentPos?.isSome && here.any (·.2.documentPos? == envDocumentPos?) then envDocRefs env + else docRefs [snap] + -- The definitions and uses under the cursor are always included. A block that fails leaves its + -- definitions and uses out of the environment. + let related := here ++ refs.filter fun (_, r) => here.any (·.2.sameRef r) + let mut seen : Std.HashSet (Option String.Pos.Raw × Option String.Pos.Raw) := {} + let mut out := #[] + for (stx, r) in related do + let span := (stx.getPos?, stx.getTailPos?) + unless seen.contains span do + seen := seen.insert span + out := out.push (stx, r) + return out.mergeSort fun (s1, _) (s2, _) => s1.getPos?.getD 0 ≤ s2.getPos?.getD 0 + open Lean Server Lsp RequestM in meta def handleRefs (params : ReferenceParams) (prev : RequestTask (Array Location)) : RequestM (RequestTask (Array Location)) := do let doc ← readDoc @@ -138,21 +211,9 @@ meta def handleRefs (params : ReferenceParams) (prev : RequestTask (Array Locati let pos := text.lspPosToUtf8Pos params.position bindWaitFindSnap doc (·.endPos + ' ' >= pos) (notFoundX := pure prev) fun snap => do withFallbackAs (!·.isEmpty) prev <| do - let nodes := snap.infoTree.deepestNodes fun _ctxt info _arr => - match info with - | .ofCustomInfo ⟨stx, data⟩ => - if stx.containsPos pos then - data.get? DocRefInfo - else none - | _ => none - if nodes.isEmpty then return #[] - else - let mut locs : Array Location := #[] - for node in nodes do - for stx in node.syntax do - if let some range := stx.lspRange text then - locs := locs.push {uri := params.textDocument.uri, range := range} - pure <| locs + let related ← relatedDocRefs snap (docRefsAt snap pos) + return related.filterMap fun (stx, _) => + stx.lspRange text |>.map ({uri := params.textDocument.uri, range := ·}) open Lean Server Lsp RequestM in meta partial def handleHl (params : DocumentHighlightParams) (prev : RequestTask DocumentHighlightResult) : RequestM (RequestTask DocumentHighlightResult) := do @@ -161,33 +222,22 @@ meta partial def handleHl (params : DocumentHighlightParams) (prev : RequestTask let pos := text.lspPosToUtf8Pos params.position bindWaitFindSnap doc (·.endPos + ' ' >= pos) (notFoundX := pure prev) fun snap => withFallbackAs (!·.isEmpty) prev <| do - let nodes : List (_ ⊕ _) := snap.infoTree.deepestNodes fun _ctxt info _arr => - match info with - | .ofCustomInfo ⟨stx, data⟩ => - if stx.containsPos pos then - (Sum.inl <$> data.get? DocListInfo) <|> (Sum.inr <$> data.get? DocRefInfo) - else none - | _ => none - if nodes.isEmpty then + let lists := customInfoAt DocListInfo snap pos |>.map (·.2) + let related ← relatedDocRefs snap (docRefsAt snap pos) + if lists.isEmpty && related.isEmpty then if let some hls := syntactic text pos snap.stx then return hls.filterMap (fun stx : Syntax => stx.lspRange text) |>.map ({range := · : DocumentHighlight}) else return #[] else let mut hls := #[] - for node in nodes do - match node with - | .inl ⟨bulletStxs, _⟩ => - for s in bulletStxs do - if let some range := s.lspRange text then - hls := hls.push {range : DocumentHighlight} - | .inr ⟨defSite, useSites⟩ => - if let some s := defSite then - if let some range := s.lspRange text then - hls := hls.push {range : DocumentHighlight} - for s in useSites do - if let some range := s.lspRange text then - hls := hls.push {range : DocumentHighlight} + for ⟨bulletStxs, _⟩ in lists do + for s in bulletStxs do + if let some range := s.lspRange text then + hls := hls.push {range : DocumentHighlight} + for (s, _) in related do + if let some range := s.lspRange text then + hls := hls.push {range : DocumentHighlight} pure hls where -- Unfortunately, VS Code doesn't do the right thing, so many of these highlights don't work there: @@ -604,32 +654,17 @@ where open Lean Server Lsp RequestM in meta def handleDef (params : TextDocumentPositionParams) (prev : RequestTask (Array LeanLocationLink)) : RequestM (RequestTask (Array LeanLocationLink)) := do - let ctx ← read let doc ← readDoc let text := doc.meta.text let pos := text.lspPosToUtf8Pos params.position - let locTask ← RequestM.asTask do - let (snaps, _, _) ← doc.cmdSnaps.getFinishedPrefixWithTimeout 300 (cancelTks := ctx.cancelTk.cancellationTasks) - let nodes := snaps.flatMap fun snap => - snap.infoTree.collectNodesBottomUp fun _ctxt info _arr xs => - match info with - | .ofCustomInfo ⟨stx, data⟩ => - if stx.containsPos pos then - if let some i := data.get? DocRefInfo then i :: xs else xs - else xs - | _ => xs - - let mut locs : Array LeanLocationLink := #[] - for node in nodes do - match node with - | ⟨some defSite, _⟩ => - let mut origin : Option Range := none - for stx in node.syntax do - if let some ⟨head, tail⟩ := stx.getRange? then - if pos ≥ head && pos ≤ tail then - origin := stx.lspRange text - break - let some target := defSite.lspRange text + bindWaitFindSnap doc (·.endPos + ' ' >= pos) (notFoundX := pure prev) fun snap => + withFallbackAs (!·.isEmpty) prev <| do + let here := docRefsAt snap pos + let origin := here[0]?.bind (·.1.lspRange text) + let mut locs : Array LeanLocationLink := #[] + for (labelStx, r) in ← relatedDocRefs snap here do + unless r.isDef do continue + let some target := labelStx.lspRange text | continue locs := locs.push { originSelectionRange? := origin, @@ -644,10 +679,7 @@ meta def handleDef (params : TextDocumentPositionParams) (prev : RequestTask (Ar ident? := none, isDefault := true } - | _ => continue - pure locs - mergeResponses prev locTask fun xs ys => - xs.getD #[] ++ ys.getD #[] + pure locs open Lean Server Lsp RequestM in meta partial def handleTokens (prev : RequestTask SemanticTokens) @@ -715,13 +747,13 @@ public meta def renumberLists : CodeActionProvider := fun params snap => do let text := doc.meta.text let startPos := text.lspPosToUtf8Pos params.range.start let endPos := text.lspPosToUtf8Pos params.range.end - let lists := snap.infoTree.foldInfo (init := #[]) fun ctx info result => Id.run do - let .ofCustomInfo ⟨stx, data⟩ := info | result - let some listInfo := data.get? DocListInfo | result - let (some head, some tail) := (stx.getPos? true, stx.getTailPos? true) | result - unless head ≤ endPos && startPos ≤ tail do return result - result.push (ctx, listInfo) - pure <| lists.map fun (_, ⟨bulletStxs, _⟩) => { + let lists := + Verso.foldCustomInfoIn DocListInfo snap.cmdState.infoState startPos endPos (init := #[]) + fun stx listInfo result => Id.run do + let (some head, some tail) := (stx.getPos? true, stx.getTailPos? true) | result + unless head ≤ endPos && startPos ≤ tail do return result + result.push listInfo + pure <| lists.map fun ⟨bulletStxs, _⟩ => { eager := { title := "Number from 1", kind? := some "quickfix", @@ -913,13 +945,7 @@ meta def handleHover (params : HoverParams) (prev : RequestTask (Option Hover)) let pos := text.lspPosToUtf8Pos params.position bindWaitFindSnap doc (·.endPos + ' ' >= pos) (notFoundX := pure prev) fun snap => do withFallbackAs (·.isSome) prev <| do - let nodes : List (Syntax × CustomHover) := snap.infoTree.deepestNodes fun _ctxt info _arr => - match info with - | .ofCustomInfo ⟨stx, data⟩ => - if stx.containsPos pos then - (stx, ·) <$> data.get? CustomHover - else none - | _ => none + let nodes := customInfoAt CustomHover snap pos |>.toList match nodes with | [] => pure none | h :: hs =>