|
| 1 | +/- |
| 2 | +Copyright (c) 2026 Lean FRO LLC. All rights reserved. |
| 3 | +Released under Apache 2.0 license as described in the file LICENSE. |
| 4 | +Author: Emilio J. Gallego Arias |
| 5 | +-/ |
| 6 | +module |
| 7 | +public import Verso |
| 8 | +public import VersoManual |
| 9 | +public meta import Verso |
| 10 | +public meta import VersoManual |
| 11 | +import Errata |
| 12 | + |
| 13 | +namespace Verso.Integration.SectionAnchors |
| 14 | + |
| 15 | +open Lean Verso Genre Manual |
| 16 | + |
| 17 | +#docs (Manual) doc "Section Anchors" := |
| 18 | +::::::: |
| 19 | +%%% |
| 20 | +tag := "manual-root" |
| 21 | +%%% |
| 22 | + |
| 23 | +See {ref "tagged-chapter"}[the chapter] and {ref "nested-section"}[its section]. |
| 24 | + |
| 25 | +# Tagged Chapter |
| 26 | +%%% |
| 27 | +tag := "tagged-chapter" |
| 28 | +%%% |
| 29 | + |
| 30 | +Return to {ref "manual-root"}[the title page]. |
| 31 | + |
| 32 | +## Nested Section |
| 33 | +%%% |
| 34 | +tag := "nested-section" |
| 35 | +%%% |
| 36 | + |
| 37 | +This section stays on its chapter's page. |
| 38 | + |
| 39 | +# Automatic Chapter |
| 40 | + |
| 41 | +This chapter gets an automatically generated tag. |
| 42 | +::::::: |
| 43 | + |
| 44 | +/-- Every exported section target must occur exactly once, on a heading in its declared page. -/ |
| 45 | +private def checkAnchors (mode : Mode) (htmlDepth : Nat := 1) : IO Unit := IO.FS.withTempDir fun destination => do |
| 46 | + let cfg : RenderConfig := { destination, htmlDepth, features := {} } |
| 47 | + let (traverse, emit, directory) := match mode with |
| 48 | + | .single => (traverseHtmlSingle, emitHtmlSingle, "html-single") |
| 49 | + | .multi => (traverseHtmlMulti, emitHtmlMulti, "html-multi") |
| 50 | + let site := destination / directory |
| 51 | + let exitCode ← withLogger fun logger => do |
| 52 | + let (part, state) ← (traverse cfg doc.toPart).run extension_impls% |>.run logger |
| 53 | + emitXrefsJson site state |
| 54 | + (emit cfg part state).run extension_impls% |>.run logger |
| 55 | + unless exitCode == 0 do |
| 56 | + throw <| IO.userError "Section anchor document generation logged errors" |
| 57 | + let xrefs ← IO.ofExcept <| Json.parse (← IO.FS.readFile (site / "xref.json")) |
| 58 | + let sections ← IO.ofExcept <| xrefs.getObjVal? "Verso.Genre.Manual.section" |
| 59 | + let contents ← IO.ofExcept <| sections.getObjVal? "contents" |
| 60 | + let entries ← IO.ofExcept contents.getObj? |
| 61 | + unless entries.size == 4 do |
| 62 | + throw <| IO.userError s!"Expected four section targets, got {entries.size}" |
| 63 | + for tag in ["manual-root", "tagged-chapter", "nested-section"] do |
| 64 | + discard <| IO.ofExcept <| contents.getObjVal? tag |
| 65 | + for (tag, targets) in entries.toArray do |
| 66 | + let targets ← IO.ofExcept targets.getArr? |
| 67 | + unless targets.size == 1 do |
| 68 | + throw <| IO.userError s!"Expected one destination for {tag}" |
| 69 | + let target := targets[0]! |
| 70 | + let address ← IO.ofExcept <| target.getObjValAs? String "address" |
| 71 | + let id ← IO.ofExcept <| target.getObjValAs? String "id" |
| 72 | + let page := (address.splitOn "/").filter (!·.isEmpty) |>.foldl (· / ·) site |
| 73 | + let html ← IO.FS.readFile (page / "index.html") |
| 74 | + let count := (html.splitOn s!" id=\"{id}\"").length - 1 |
| 75 | + unless count == 1 do |
| 76 | + throw <| IO.userError s!"{tag}: expected exactly one id=\"{id}\" in {address}, got {count}" |
| 77 | + unless (List.range 6).any (fun n => (html.splitOn s!"<h{n + 1} id=\"{id}\">").length == 2) do |
| 78 | + throw <| IO.userError s!"{tag}: expected id=\"{id}\" on a heading in {address}" |
| 79 | + |
| 80 | +/-- Single-page manual headings contain every exported section target exactly once. -/ |
| 81 | +@[test] |
| 82 | +def singlePageSectionAnchors : Errata.Test := do |
| 83 | + checkAnchors .single |
| 84 | + |
| 85 | +/-- Multi-page manual headings retain their anchors at each splitting depth. -/ |
| 86 | +@[test] |
| 87 | +def multiPageSectionAnchors : Errata.Test := do |
| 88 | + for depth in [0, 1, 2] do |
| 89 | + checkAnchors .multi depth |
0 commit comments