diff --git a/src/tests/VersoTests/DocStructure.lean b/src/tests/VersoTests/DocStructure.lean new file mode 100644 index 000000000..835365d88 --- /dev/null +++ b/src/tests/VersoTests/DocStructure.lean @@ -0,0 +1,384 @@ +/- +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 VersoTests.DocStructure.Genre +import VersoTests.DocStructure.Included +import VersoTests.DocStructure.Nesting +import VersoTests.DocStructure.Metadata +import VersoTests.DocStructure.Includes +import VersoTests.DocStructure.Term.Nesting +import VersoTests.DocStructure.Term.Metadata +import VersoTests.DocStructure.Term.Includes + +set_option doc.verso true + +/-! +Tests of the parts that document elaboration produces. + +The sample documents in {lit}`VersoTests.DocStructure` are elaborated three ways: block by block by +the {lit}`#doc` command, and all at once by {lit}`#docs` and by the {lit}`#doc` term. All three +must produce the same parts. The tests compare them with golden files. +-/ + +open Verso.Doc +open Errata + +namespace Verso.Tests.DocStructure.Docs + +/- The document of `VersoTests.DocStructure.Nesting`, elaborated all at once by `#docs`. -/ +#docs (StructuralTesting) nesting "Nesting" := +::::::: + +Text before any header. + +A second paragraph before any header. + +# One + +Text in one. + +## One A + +Text in one A. + +### One A i + +Text in one A i. + +#### One A i x + +Text in one A i x. + +## One B + +Text in one B. + +### One B i + +# Two + +## Two A + +### Two A i + +Text in two A i. + +# Three + +Text in three. + +* a list +* in three + +## Three A + +## Three B + +## Three C + +Text in three C. +::::::: + +/- The document of `VersoTests.DocStructure.Metadata`, elaborated all at once by `#docs`. -/ +#docs (StructuralTesting) metadata "Metadata" := +::::::: +%%% +tag := "root" +number := 1 +%%% + +Text in the root, with a [link][example] and a footnote.[^note] + +[example]: https://example.com + +# First +%%% +tag := "first" +%%% + +Text in first. + +[^note]: The footnote text. + +## First Nested +%%% +number := 2 +%%% + +# Second + +Text in second, which has no metadata. + +[other]: https://example.org + +## Second Nested +%%% +tag := "second nested" +number := 3 +%%% + +Text in second nested, with [another link][other]. +::::::: + +/- The document of `VersoTests.DocStructure.Includes`, elaborated all at once by `#docs`. -/ +#docs (StructuralTesting) includes "Includes" := +::::::: + +Text before the first include. + +{include VersoTests.DocStructure.Included} + +# Section + +Text in section. + +## Nested + +Text in nested. + +{include 2 VersoTests.DocStructure.Included} + +{include 1 VersoTests.DocStructure.Included} + +# After + +Text after the includes. + +## After Nested + +{include VersoTests.DocStructure.Included} + +{include 3 VersoTests.DocStructure.Included} +::::::: + +end Verso.Tests.DocStructure.Docs + +namespace Verso.Tests.DocStructure + +/-- The directory that holds the golden files and the test output. -/ +def baseDir : System.FilePath := "src/tests/integration/doc-structure" + +/-- +Renders each document's parts to {lit}`output//.txt`, then compares the output with the +golden files in {lit}`expected`. +-/ +def checkStructure (dir : String) (docs : List (String × Part StructuralTesting)) : Test := do + let output := baseDir / "output" / dir + if ← output.pathExists then IO.FS.removeDirAll output + IO.FS.createDirAll output + for (name, part) in docs do + IO.FS.writeFile (output / s!"{name}.txt") (renderPart part) + goldenDir (baseDir / "expected") output + +/-- The documents elaborated block by block by the {lit}`#doc` command match the golden files. -/ +@[test] +def docCommand : Test := + checkStructure "doc-command" [ + ("nesting", %doc VersoTests.DocStructure.Nesting), + ("metadata", %doc VersoTests.DocStructure.Metadata), + ("includes", %doc VersoTests.DocStructure.Includes) + ] + +/-- The documents elaborated all at once by {lit}`#docs` match the golden files. -/ +@[test] +def docsCommand : Test := + checkStructure "docs-command" [ + ("nesting", Docs.nesting.toPart), + ("metadata", Docs.metadata.toPart), + ("includes", Docs.includes.toPart) + ] + +/-- The documents elaborated all at once by the {lit}`#doc` term match the golden files. -/ +@[test] +def docTerm : Test := + checkStructure "doc-term" [ + ("nesting", Term.nesting.toPart), + ("metadata", Term.metadata.toPart), + ("includes", Term.includes.toPart) + ] + +end Verso.Tests.DocStructure + +namespace Verso.Tests.DocStructure.Errors + +/- Errors for badly structured parts. -/ + +/-- +error: Wrong header nesting - got ### but expected at most ## +-/ +#test_msgs in +#docs (StructuralTesting) wrongNesting "Wrong Nesting" := +::::::: +# One + +### Too Deep + +Text. +::::::: + +/-- +error: Wrong header nesting - got ### but expected at most ## +-/ +#test_msgs in +#docs (StructuralTesting) wrongNestingAfterClose "Wrong Nesting After Closing Several Parts" := +::::::: +# A + +## B + +### C + +# D + +### E +::::::: + +/-- +error: Wrong header nesting - got ## but expected at most # +-/ +#test_msgs in +#docs (StructuralTesting) wrongNestingAtRoot "Wrong Nesting at the Root" := +::::::: +## Too Deep +::::::: + +/-- +error: Metadata blocks must precede both content and subsections +-/ +#test_msgs in +#docs (StructuralTesting) metadataAfterContent "Metadata After Content" := +::::::: +Text. + +%%% +tag := "late" +%%% +::::::: + +/-- +error: Metadata blocks must precede both content and subsections +-/ +#test_msgs in +#docs (StructuralTesting) metadataAfterContentInSection "Metadata After Content in a Section" := +::::::: +# Section + +Text. + +%%% +tag := "late" +%%% +::::::: + +/-- +error: Metadata blocks must precede both content and subsections +-/ +#test_msgs in +#docs (StructuralTesting) metadataAfterSubPart "Metadata After a Sub-Part" := +::::::: +# Section + +{include VersoTests.DocStructure.Included} + +%%% +tag := "late" +%%% +::::::: + +/-- +error: Metadata already provided for this section +-/ +#test_msgs in +#docs (StructuralTesting) duplicateMetadata "Duplicate Metadata" := +::::::: +%%% +tag := "first" +%%% + +%%% +tag := "second" +%%% +::::::: + +/-- +error: Metadata already provided for this section +-/ +#test_msgs in +#docs (StructuralTesting) duplicateMetadataInSection "Duplicate Metadata in a Section" := +::::::: +# Section +%%% +tag := "first" +%%% + +%%% +tag := "second" +%%% +::::::: + +/-- +error: Block content found in a context where a header was expected. + + +Note: A document part (section/chapter/etc) consists of a header, followed by zero or more blocks, followed by zero or more sub-parts. This block occurs after a sub-part (namely `VersoTests.DocStructure.Included`), but outside of the sub-parts. +-/ +#test_msgs in +#docs (StructuralTesting) contentAfterInclude "Content After an Include" := +::::::: +Text. + +{include VersoTests.DocStructure.Included} + +More text. +::::::: + +/-- +error: Block content found in a context where a header was expected. + + +Note: A document part (section/chapter/etc) consists of a header, followed by zero or more blocks, followed by zero or more sub-parts. This block occurs after a sub-part (namely `VersoTests.DocStructure.Included`), but outside of the sub-parts. +-/ +#test_msgs in +#docs (StructuralTesting) contentAfterIncludeInSection "Content After an Include in a Section" := +::::::: +# Section + +{include 2 VersoTests.DocStructure.Included} + +* A list +::::::: + +open Lean Lean.Elab Lean.Doc.Syntax Verso.Doc.Elab PartElabM in +/-- +Adds a finished part with the title {lit}`Built Part` as a sub-part of the root part. It is an +example of a part command that builds a whole part. +-/ +@[part_command Lean.Doc.Syntax.command] +meta def builtPart : PartCommand + | stx@`(block|command{builtPart $args*}) => do + unless args.isEmpty do throwErrorAt stx "Expected no arguments" + let endPos := stx.getTailPos?.getD 0 + closePartsUntil 1 (stx.getPos?.getD 0) + addPart <| .mk stx stx #[] "Built Part" none #[] #[] endPos + | _ => throwUnsupportedSyntax + +/-- +error: Block content found in a context where a header was expected. + + +Note: A document part (section/chapter/etc) consists of a header, followed by zero or more blocks, followed by zero or more sub-parts. This block occurs after a sub-part (namely “Built Part”), but outside of the sub-parts. +-/ +#test_msgs in +#docs (StructuralTesting) contentAfterBuiltPart "Content After a Built Part" := +::::::: +# Section + +{builtPart} + +Text. +::::::: + +end Verso.Tests.DocStructure.Errors diff --git a/src/tests/VersoTests/DocStructure/Genre.lean b/src/tests/VersoTests/DocStructure/Genre.lean new file mode 100644 index 000000000..25a1ec436 --- /dev/null +++ b/src/tests/VersoTests/DocStructure/Genre.lean @@ -0,0 +1,75 @@ +/- +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 Verso + +set_option doc.verso true + +/-! +A minimal genre for the document structure tests, and a text rendering of a document's parts. +-/ + +namespace Verso.Tests.DocStructure + +open Verso.Doc + +/-- The part metadata of the test genre. -/ +public structure StructuralTesting.Metadata where + tag : String := "" + number : Nat := 0 +deriving Repr + +/-- A genre whose only feature is its part metadata. -/ +@[expose] +public def StructuralTesting : Genre where + PartMetadata := StructuralTesting.Metadata + Block := Empty + Inline := Empty + TraverseContext := Unit + TraverseState := Unit + +public instance : Repr (Genre.PartMetadata StructuralTesting) := + inferInstanceAs (Repr StructuralTesting.Metadata) + +/-- A plain-text summary of some inline content. -/ +partial def inlineSummary : Inline StructuralTesting → String + | .text s | .code s | .math _ s => s + | .linebreak _ => " " + | .emph xs | .bold xs | .concat xs => String.join (xs.map inlineSummary).toList + | .link xs url => s!"[{String.join (xs.map inlineSummary).toList}]({url})" + | .footnote name _ => s!"[^{name}]" + | .image alt url => s!"![{alt}]({url})" + | .other e _ => nomatch e + +/-- A one-line summary of a block. -/ +def blockSummary : Block StructuralTesting → String + | .para xs => s!"para: {(String.join (xs.map inlineSummary).toList).trimAscii}" + | .code s => s!"code: {s.trimAscii}" + | .ul items => s!"ul: {items.size} items" + | .ol _ items => s!"ol: {items.size} items" + | .dl items => s!"dl: {items.size} items" + | .blockquote items => s!"blockquote: {items.size} blocks" + | .concat items => s!"concat: {items.size} blocks" + | .other e _ => nomatch e + +/-- +Renders a part as indented text: its title, metadata, blocks and sub-parts. Included documents +appear as the parts they contain. +-/ +public partial def renderPart (part : Part StructuralTesting) (depth : Nat := 0) : String := + let indent := "".pushn ' ' (2 * depth) + let header := s!"{indent}part {part.titleString.quote}\n" + let metadata := + match part.metadata with + | some m => s!"{indent} metadata: {reprStr m}\n" + | none => "" + let blocks := + s!"{indent} blocks: {part.content.size}\n" ++ + String.join (part.content.map (s!"{indent} - {blockSummary ·}\n")).toList + let subParts := String.join (part.subParts.map (renderPart · (depth + 1))).toList + header ++ metadata ++ blocks ++ subParts + +end Verso.Tests.DocStructure diff --git a/src/tests/VersoTests/DocStructure/Included.lean b/src/tests/VersoTests/DocStructure/Included.lean new file mode 100644 index 000000000..9b0304880 --- /dev/null +++ b/src/tests/VersoTests/DocStructure/Included.lean @@ -0,0 +1,23 @@ +/- +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 VersoTests.DocStructure.Genre + +open Verso.Tests.DocStructure + +/-! +A document that the other document structure samples include. +-/ + +#doc (StructuralTesting) "Included Document" => +%%% +tag := "included" +%%% + +Text of the included document. + +# Included Section + +Text of the included section. diff --git a/src/tests/VersoTests/DocStructure/Includes.lean b/src/tests/VersoTests/DocStructure/Includes.lean new file mode 100644 index 000000000..705b172cc --- /dev/null +++ b/src/tests/VersoTests/DocStructure/Includes.lean @@ -0,0 +1,41 @@ +/- +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 VersoTests.DocStructure.Genre +import VersoTests.DocStructure.Included + +open Verso.Tests.DocStructure + +/-! +Included documents, with and without an explicit header level. +-/ + +#doc (StructuralTesting) "Includes" => + +Text before the first include. + +{include VersoTests.DocStructure.Included} + +# Section + +Text in section. + +## Nested + +Text in nested. + +{include 2 VersoTests.DocStructure.Included} + +{include 1 VersoTests.DocStructure.Included} + +# After + +Text after the includes. + +## After Nested + +{include VersoTests.DocStructure.Included} + +{include 3 VersoTests.DocStructure.Included} diff --git a/src/tests/VersoTests/DocStructure/Metadata.lean b/src/tests/VersoTests/DocStructure/Metadata.lean new file mode 100644 index 000000000..668c9b7bd --- /dev/null +++ b/src/tests/VersoTests/DocStructure/Metadata.lean @@ -0,0 +1,50 @@ +/- +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 VersoTests.DocStructure.Genre + +open Verso.Tests.DocStructure + +/-! +Metadata on the root part and on sub-parts, with link and footnote definitions between headers. +-/ + +#doc (StructuralTesting) "Metadata" => +%%% +tag := "root" +number := 1 +%%% + +Text in the root, with a [link][example] and a footnote.[^note] + +[example]: https://example.com + +# First +%%% +tag := "first" +%%% + +Text in first. + +[^note]: The footnote text. + +## First Nested +%%% +number := 2 +%%% + +# Second + +Text in second, which has no metadata. + +[other]: https://example.org + +## Second Nested +%%% +tag := "second nested" +number := 3 +%%% + +Text in second nested, with [another link][other]. diff --git a/src/tests/VersoTests/DocStructure/Nesting.lean b/src/tests/VersoTests/DocStructure/Nesting.lean new file mode 100644 index 000000000..7cc1109ce --- /dev/null +++ b/src/tests/VersoTests/DocStructure/Nesting.lean @@ -0,0 +1,63 @@ +/- +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 VersoTests.DocStructure.Genre + +open Verso.Tests.DocStructure + +/-! +Nested headers, headers that return to shallower levels, and sibling parts. +-/ + +#doc (StructuralTesting) "Nesting" => + +Text before any header. + +A second paragraph before any header. + +# One + +Text in one. + +## One A + +Text in one A. + +### One A i + +Text in one A i. + +#### One A i x + +Text in one A i x. + +## One B + +Text in one B. + +### One B i + +# Two + +## Two A + +### Two A i + +Text in two A i. + +# Three + +Text in three. + +* a list +* in three + +## Three A + +## Three B + +## Three C + +Text in three C. diff --git a/src/tests/VersoTests/DocStructure/Term/Includes.lean b/src/tests/VersoTests/DocStructure/Term/Includes.lean new file mode 100644 index 000000000..ac03c12d2 --- /dev/null +++ b/src/tests/VersoTests/DocStructure/Term/Includes.lean @@ -0,0 +1,41 @@ +/- +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 VersoTests.DocStructure.Genre +import VersoTests.DocStructure.Included + +open Verso.Doc Verso.Tests.DocStructure + +/-! +The document of `VersoTests.DocStructure.Includes`, elaborated all at once by the `#doc` term. +-/ + +def Verso.Tests.DocStructure.Term.includes : VersoDoc StructuralTesting := #doc (StructuralTesting) "Includes" => + +Text before the first include. + +{include VersoTests.DocStructure.Included} + +# Section + +Text in section. + +## Nested + +Text in nested. + +{include 2 VersoTests.DocStructure.Included} + +{include 1 VersoTests.DocStructure.Included} + +# After + +Text after the includes. + +## After Nested + +{include VersoTests.DocStructure.Included} + +{include 3 VersoTests.DocStructure.Included} diff --git a/src/tests/VersoTests/DocStructure/Term/Metadata.lean b/src/tests/VersoTests/DocStructure/Term/Metadata.lean new file mode 100644 index 000000000..9a28a0d07 --- /dev/null +++ b/src/tests/VersoTests/DocStructure/Term/Metadata.lean @@ -0,0 +1,50 @@ +/- +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 VersoTests.DocStructure.Genre + +open Verso.Doc Verso.Tests.DocStructure + +/-! +The document of `VersoTests.DocStructure.Metadata`, elaborated all at once by the `#doc` term. +-/ + +def Verso.Tests.DocStructure.Term.metadata : VersoDoc StructuralTesting := #doc (StructuralTesting) "Metadata" => +%%% +tag := "root" +number := 1 +%%% + +Text in the root, with a [link][example] and a footnote.[^note] + +[example]: https://example.com + +# First +%%% +tag := "first" +%%% + +Text in first. + +[^note]: The footnote text. + +## First Nested +%%% +number := 2 +%%% + +# Second + +Text in second, which has no metadata. + +[other]: https://example.org + +## Second Nested +%%% +tag := "second nested" +number := 3 +%%% + +Text in second nested, with [another link][other]. diff --git a/src/tests/VersoTests/DocStructure/Term/Nesting.lean b/src/tests/VersoTests/DocStructure/Term/Nesting.lean new file mode 100644 index 000000000..a4b226ac8 --- /dev/null +++ b/src/tests/VersoTests/DocStructure/Term/Nesting.lean @@ -0,0 +1,63 @@ +/- +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 VersoTests.DocStructure.Genre + +open Verso.Doc Verso.Tests.DocStructure + +/-! +The document of `VersoTests.DocStructure.Nesting`, elaborated all at once by the `#doc` term. +-/ + +def Verso.Tests.DocStructure.Term.nesting : VersoDoc StructuralTesting := #doc (StructuralTesting) "Nesting" => + +Text before any header. + +A second paragraph before any header. + +# One + +Text in one. + +## One A + +Text in one A. + +### One A i + +Text in one A i. + +#### One A i x + +Text in one A i x. + +## One B + +Text in one B. + +### One B i + +# Two + +## Two A + +### Two A i + +Text in two A i. + +# Three + +Text in three. + +* a list +* in three + +## Three A + +## Three B + +## Three C + +Text in three C. diff --git a/src/tests/VersoTests/VersoManual/Markdown.lean b/src/tests/VersoTests/VersoManual/Markdown.lean index e93137656..413607533 100644 --- a/src/tests/VersoTests/VersoManual/Markdown.lean +++ b/src/tests/VersoTests/VersoManual/Markdown.lean @@ -76,6 +76,23 @@ def markdownPartRangesValid (input : String) : Elab.TermElabM Bool := do let (_, _, part) ← addParts.run ⟨Syntax.node .none identKind #[], mkConst ``Manual, .always, .none⟩ default default return part.partContext.priorParts.all partRangesValid +open PartElabM in +/-- +Adds a Markdown header while `currentHeaderLevels` lists one Markdown section. The root part is the +only part under construction, so closing that section fails. +-/ +def closeMarkdownSectionAtRoot : Elab.TermElabM Unit := do + let some parsed := MD4Lean.parse "# Header" + | throwError m!"Couldn't parse markdown" + let addParts : PartElabM Unit := do + for block in parsed.blocks do + discard <| addPartFromMarkdown block (currentHeaderLevels := [1]) + discard <| addParts.run ⟨Syntax.node .none identKind #[], mkConst ``Manual, .always, .none⟩ default default + +/-- error: Failed to close verso part corresponding to markdown section: no parts left -/ +#test_msgs in +#eval closeMarkdownSectionAtRoot + /-- info: true -/ #test_msgs in #eval markdownPartRangesValid r#" diff --git a/src/tests/integration/doc-structure/expected/includes.txt b/src/tests/integration/doc-structure/expected/includes.txt new file mode 100644 index 000000000..cce8f48c4 --- /dev/null +++ b/src/tests/integration/doc-structure/expected/includes.txt @@ -0,0 +1,49 @@ +part "Includes" + blocks: 1 + - para: Text before the first include. + part "Included Document" + metadata: { tag := "included", number := 0 } + blocks: 1 + - para: Text of the included document. + part "Included Section" + blocks: 1 + - para: Text of the included section. + part "Section" + blocks: 1 + - para: Text in section. + part "Nested" + blocks: 1 + - para: Text in nested. + part "Included Document" + metadata: { tag := "included", number := 0 } + blocks: 1 + - para: Text of the included document. + part "Included Section" + blocks: 1 + - para: Text of the included section. + part "Included Document" + metadata: { tag := "included", number := 0 } + blocks: 1 + - para: Text of the included document. + part "Included Section" + blocks: 1 + - para: Text of the included section. + part "After" + blocks: 1 + - para: Text after the includes. + part "After Nested" + blocks: 0 + part "Included Document" + metadata: { tag := "included", number := 0 } + blocks: 1 + - para: Text of the included document. + part "Included Section" + blocks: 1 + - para: Text of the included section. + part "Included Document" + metadata: { tag := "included", number := 0 } + blocks: 1 + - para: Text of the included document. + part "Included Section" + blocks: 1 + - para: Text of the included section. diff --git a/src/tests/integration/doc-structure/expected/metadata.txt b/src/tests/integration/doc-structure/expected/metadata.txt new file mode 100644 index 000000000..3e1d7999f --- /dev/null +++ b/src/tests/integration/doc-structure/expected/metadata.txt @@ -0,0 +1,18 @@ +part "Metadata" + metadata: { tag := "root", number := 1 } + blocks: 1 + - para: Text in the root, with a [link](https://example.com) and a footnote.[^note] + part "First" + metadata: { tag := "first", number := 0 } + blocks: 1 + - para: Text in first. + part "First Nested" + metadata: { tag := "", number := 2 } + blocks: 0 + part "Second" + blocks: 1 + - para: Text in second, which has no metadata. + part "Second Nested" + metadata: { tag := "second nested", number := 3 } + blocks: 1 + - para: Text in second nested, with [another link](https://example.org). diff --git a/src/tests/integration/doc-structure/expected/nesting.txt b/src/tests/integration/doc-structure/expected/nesting.txt new file mode 100644 index 000000000..5dae1540b --- /dev/null +++ b/src/tests/integration/doc-structure/expected/nesting.txt @@ -0,0 +1,39 @@ +part "Nesting" + blocks: 2 + - para: Text before any header. + - para: A second paragraph before any header. + part "One" + blocks: 1 + - para: Text in one. + part "One A" + blocks: 1 + - para: Text in one A. + part "One A i" + blocks: 1 + - para: Text in one A i. + part "One A i x" + blocks: 1 + - para: Text in one A i x. + part "One B" + blocks: 1 + - para: Text in one B. + part "One B i" + blocks: 0 + part "Two" + blocks: 0 + part "Two A" + blocks: 0 + part "Two A i" + blocks: 1 + - para: Text in two A i. + part "Three" + blocks: 2 + - para: Text in three. + - ul: 2 items + part "Three A" + blocks: 0 + part "Three B" + blocks: 0 + part "Three C" + blocks: 1 + - para: Text in three C. diff --git a/src/tests/interactive/test-cases/symbols_verso_nesting.lean b/src/tests/interactive/test-cases/symbols_verso_nesting.lean new file mode 100644 index 000000000..15081734a --- /dev/null +++ b/src/tests/interactive/test-cases/symbols_verso_nesting.lean @@ -0,0 +1,59 @@ +import VersoTests.DocStructure.Genre +import VersoTests.DocStructure.Included + +open Verso.Tests.DocStructure + +-- Document symbols and folding ranges for deep nesting, headers that return to shallower levels, +-- included documents and metadata. Synchronize first so that the whole document is elaborated. +-- The `--^` requests come before the document. After it, they would be paragraph text in its last +-- part, and they would change what the test measures. +--^ sync +--^ textDocument/documentSymbol +--^ textDocument/foldingRange + +#doc (StructuralTesting) "Nesting Symbols" => +%%% +tag := "root" +%%% + +Text before any header. + +# One +%%% +tag := "one" +%%% + +Text in one. + +## One A + +### One A i + +#### One A i x + +Text in one A i x. + +{include 3 VersoTests.DocStructure.Included} + +## One B + +{include 2 VersoTests.DocStructure.Included} + +# Two +%%% +number := 2 +%%% + +{include VersoTests.DocStructure.Included} + +# Three + +## Three A + +### Three A i + +Text in three A i. + +# Four + +Text at the end of the document. diff --git a/src/tests/interactive/test-cases/symbols_verso_nesting.lean.expected.out b/src/tests/interactive/test-cases/symbols_verso_nesting.lean.expected.out new file mode 100644 index 000000000..af64ff5fa --- /dev/null +++ b/src/tests/interactive/test-cases/symbols_verso_nesting.lean.expected.out @@ -0,0 +1,149 @@ +{"textDocument": + {"uri": "file:///src/tests/interactive/test-cases/symbols_verso_nesting.lean"}, + "position": {"line": 8, "character": 2}} +[{"selectionRange": + {"start": {"line": 13, "character": 25}, + "end": {"line": 13, "character": 42}}, + "range": + {"start": {"line": 13, "character": 0}, "end": {"line": 59, "character": 0}}, + "name": "Nesting Symbols", + "kind": 15, + "children": + [{"selectionRange": + {"start": {"line": 20, "character": 0}, + "end": {"line": 20, "character": 5}}, + "range": + {"start": {"line": 20, "character": 0}, + "end": {"line": 41, "character": 0}}, + "name": "One", + "kind": 15, + "children": + [{"selectionRange": + {"start": {"line": 27, "character": 0}, + "end": {"line": 27, "character": 8}}, + "range": + {"start": {"line": 27, "character": 0}, + "end": {"line": 37, "character": 0}}, + "name": "One A", + "kind": 15, + "children": + [{"selectionRange": + {"start": {"line": 29, "character": 0}, + "end": {"line": 29, "character": 11}}, + "range": + {"start": {"line": 29, "character": 0}, + "end": {"line": 35, "character": 0}}, + "name": "One A i", + "kind": 15, + "children": + [{"selectionRange": + {"start": {"line": 31, "character": 0}, + "end": {"line": 31, "character": 14}}, + "range": + {"start": {"line": 31, "character": 0}, + "end": {"line": 35, "character": 0}}, + "name": "One A i x", + "kind": 15}]}, + {"selectionRange": + {"start": {"line": 35, "character": 11}, + "end": {"line": 35, "character": 43}}, + "range": + {"start": {"line": 35, "character": 11}, + "end": {"line": 35, "character": 43}}, + "name": "VersoTests.DocStructure.Included", + "kind": 7, + "detail": + "Included from VersoTests.DocStructure.Included.«the canonical document object name»"}]}, + {"selectionRange": + {"start": {"line": 37, "character": 0}, + "end": {"line": 37, "character": 8}}, + "range": + {"start": {"line": 37, "character": 0}, + "end": {"line": 39, "character": 0}}, + "name": "One B", + "kind": 15}, + {"selectionRange": + {"start": {"line": 39, "character": 11}, + "end": {"line": 39, "character": 43}}, + "range": + {"start": {"line": 39, "character": 11}, + "end": {"line": 39, "character": 43}}, + "name": "VersoTests.DocStructure.Included", + "kind": 7, + "detail": + "Included from VersoTests.DocStructure.Included.«the canonical document object name»"}]}, + {"selectionRange": + {"start": {"line": 41, "character": 0}, + "end": {"line": 41, "character": 5}}, + "range": + {"start": {"line": 41, "character": 0}, + "end": {"line": 48, "character": 0}}, + "name": "Two", + "kind": 15, + "children": + [{"selectionRange": + {"start": {"line": 46, "character": 9}, + "end": {"line": 46, "character": 41}}, + "range": + {"start": {"line": 46, "character": 9}, + "end": {"line": 46, "character": 41}}, + "name": "VersoTests.DocStructure.Included", + "kind": 7, + "detail": + "Included from VersoTests.DocStructure.Included.«the canonical document object name»"}]}, + {"selectionRange": + {"start": {"line": 48, "character": 0}, + "end": {"line": 48, "character": 7}}, + "range": + {"start": {"line": 48, "character": 0}, + "end": {"line": 56, "character": 0}}, + "name": "Three", + "kind": 15, + "children": + [{"selectionRange": + {"start": {"line": 50, "character": 0}, + "end": {"line": 50, "character": 10}}, + "range": + {"start": {"line": 50, "character": 0}, + "end": {"line": 56, "character": 0}}, + "name": "Three A", + "kind": 15, + "children": + [{"selectionRange": + {"start": {"line": 52, "character": 0}, + "end": {"line": 52, "character": 13}}, + "range": + {"start": {"line": 52, "character": 0}, + "end": {"line": 56, "character": 0}}, + "name": "Three A i", + "kind": 15}]}]}, + {"selectionRange": + {"start": {"line": 56, "character": 0}, + "end": {"line": 56, "character": 6}}, + "range": + {"start": {"line": 56, "character": 0}, + "end": {"line": 59, "character": 0}}, + "name": "Four", + "kind": 15}]}] +{"textDocument": + {"uri": "file:///src/tests/interactive/test-cases/symbols_verso_nesting.lean"}, + "position": {"line": 8, "character": 2}} +[{"startLine": 13, "endLine": 58}, + {"startLine": 20, "endLine": 40}, + {"startLine": 27, "endLine": 36}, + {"startLine": 29, "endLine": 34}, + {"startLine": 31, "endLine": 34}, + {"startLine": 37, "endLine": 38}, + {"startLine": 41, "endLine": 47}, + {"startLine": 48, "endLine": 55}, + {"startLine": 50, "endLine": 55}, + {"startLine": 52, "endLine": 55}, + {"startLine": 56, "endLine": 58}, + {"startLine": 14, "endLine": 16}, + {"startLine": 21, "endLine": 23}, + {"startLine": 42, "endLine": 44}, + {"startLine": 0, "kind": "imports", "endLine": 3}, + {"startLine": 14, "kind": "region", "endLine": 16}, + {"startLine": 21, "kind": "region", "endLine": 23}, + {"startLine": 42, "kind": "region", "endLine": 44}, + {"startLine": 58, "kind": "region", "endLine": 59}]