leanprover · david-christiansen · Jan 30, 2025 · Jan 10, 2025 · Jan 10, 2025 · Jan 10, 2025
diff --git a/doc/UsersGuide/Basic.lean b/doc/UsersGuide/Basic.lean
@@ -80,6 +80,17 @@ They include heuristic elaboration of code items in their Markdown that attempts
 
 {optionDocs pp.deepTerms.threshold}
 
+# Technical Terminology
+
+The `deftech` role can be used to annotate the definition of a {tech}[technical term].
+Elsewhere in the document, `tech` can be used to annotate a use site of a technical term.
+A {deftech}_technical term_ is a term with a specific meaning that's used precisely, like this one.
+References to technical terms are valid both before and after their definition sites.
+
+{docstring deftech}
+
+{docstring tech}
+
 # Index
 %%%
 number := false

diff --git a/examples/website-examples/lake-manifest.json b/examples/website-examples/lake-manifest.json
@@ -4,7 +4,7 @@
  [{"url": "https://github.com/leanprover/subverso.git",
    "type": "git",
    "subDir": null,
-   "rev": "844b9a53cf7acd71e0e81a3a56608bb28215646d",
+   "rev": "b4dd804a58961657d6c2f24d5eb350abb4992204",
    "name": "subverso",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",

diff --git a/lake-manifest.json b/lake-manifest.json
@@ -15,7 +15,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "844b9a53cf7acd71e0e81a3a56608bb28215646d",
+   "rev": "b4dd804a58961657d6c2f24d5eb350abb4992204",
    "name": "subverso",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",

diff --git a/src/verso-manual/VersoManual.lean b/src/verso-manual/VersoManual.lean
@@ -120,6 +120,8 @@ structure Config where
   extraFiles : List (System.FilePath × String) := []
   extraCss : List String := []
   extraJs : List String := []
+  /-- Extra elements to add to every page's `head` tag -/
+  extraHead : Array Output.Html := #[]
   draft : Bool := false
   /-- The URL from which to draw the logo to show, if any -/
   logo : Option String := none
@@ -283,6 +285,7 @@ def page (toc : List Html.Toc) (path : Path) (textTitle : String) (htmlTitle con
     (issueLink := config.issueLink)
     (extraStylesheets := config.extraCss ++ state.extraCssFiles.toList.map ("/-verso-css/" ++ ·.1))
     (extraJsFiles := config.extraJs.toArray ++ state.extraJsFiles.map ("/-verso-js/" ++ ·.1))
+    (extraHead := config.extraHead)
 
 def Config.relativize (config : Config) (path : Path) (html : Html) : Html :=
   if config.baseURL.isSome then
@@ -471,7 +474,7 @@ def manualMain (text : Part Manual)
   ReaderT.run go extensionImpls
 
 where
-  opts (cfg : Config)
+  opts (cfg : Config) : List String → ReaderT ExtensionImpls IO Config
     | ("--output"::dir::more) => opts {cfg with destination := dir} more
     | ("--depth"::n::more) => opts {cfg with htmlDepth := n.toNat!} more
     | ("--with-tex"::more) => opts {cfg with emitTeX := true} more

diff --git a/src/verso-manual/VersoManual/Basic.lean b/src/verso-manual/VersoManual/Basic.lean
@@ -736,6 +736,7 @@ def TraverseState.resolveTag (st : TraverseState) (tag : Slug) : Option (Path ×
 
 def docstringDomain := `Verso.Genre.Manual.doc
 def tacticDomain := `Verso.Genre.Manual.doc.tactic
+def technicalTermDomain := `Verso.Genre.Manual.doc.tech
 def syntaxKindDomain := `Verso.Genre.Manual.doc.syntaxKind
 def optionDomain := `Verso.Genre.Manual.doc.option
 def convDomain := `Verso.Genre.Manual.doc.tactic.conv
@@ -772,6 +773,18 @@ def TraverseState.linkTargets (state : TraverseState) : Code.LinkTargets where
      (state.resolveDomainObject syntaxKindDomain k.toString).toOption) <&>
     fun (path, htmlId) => path.link (some htmlId.toString)
 
+def sectionNumberString (num : Array Numbering) : String := Id.run do
+  let mut out := ""
+  for n in num do
+    out := out ++
+      match n with
+      | .nat n => s!"{n}."
+      | .letter a => s!"{a}."
+  out
+
+def sectionString (ctxt : TraverseContext) : Option String :=
+  ctxt.sectionNumber.mapM id |>.map sectionNumberString
+
 
 def sectionDomain := `Verso.Genre.Manual.section
 
@@ -824,9 +837,17 @@ instance : Traverse Manual TraverseM where
               externalTags := st.externalTags.insert id (path, slug)
             }
           meta := {meta with tag := external}
-        let jsonMetadata := Json.arr ((← read).inPart part |>.headers.map (Json.str ·.titleString))
+        let jsonMetadata :=
+          Json.arr ((← read).inPart part |>.headers.map (fun h => json%{"title": $h.titleString, "number": $(h.metadata.bind (·.assignedNumber) |>.map toString)}))
+        let title := (← read).inPart part |>.headers |>.back? |>.map (·.titleString)
+        -- During the traverse pass, the root section (which is unnumbered) is in the header stack.
+        -- Including it causes all sections to be unnumbered, so it needs to be dropped here.
+        -- TODO: harmonize this situation with HTML generation and give it a clean API
+        let num :=
+          ((← read).inPart part |>.headers[1:]).toArray.map (fun (h : PartHeader) => h.metadata.bind (·.assignedNumber))
+            |>.mapM _root_.id |>.map sectionNumberString
         modify (·.saveDomainObject sectionDomain n id
-                 |>.saveDomainObjectData sectionDomain n jsonMetadata)
+                 |>.saveDomainObjectData sectionDomain n (json%{"context": $jsonMetadata, "title": $title, "sectionNum": $num}))
 
     -- Assign section numbers to subsections
     let mut i := 1
@@ -919,17 +940,6 @@ instance : TeX.GenreTeX Manual (ReaderT ExtensionImpls IO) where
       | panic! s!"Inline {i.name} doesn't support TeX"
     impl go id i.data content
 
-def sectionNumberString (num : Array Numbering) : String := Id.run do
-  let mut out := ""
-  for n in num do
-    out := out ++
-      match n with
-      | .nat n => s!"{n}."
-      | .letter a => s!"{a}."
-  out
-
-def sectionString (ctxt : TraverseContext) : Option String :=
-  ctxt.sectionNumber.mapM id |>.map sectionNumberString
 
 def sectionHtml (ctxt : TraverseContext) : Html :=
   match sectionString ctxt with

diff --git a/src/verso-manual/VersoManual/Docstring.lean b/src/verso-manual/VersoManual/Docstring.lean
@@ -1567,7 +1567,10 @@ def tactic.descr : BlockDescr where
     let _ ← Verso.Genre.Manual.externalTag id path <| show.getD tactic.userName
     Index.addEntry id {term := Doc.Inline.code <| show.getD tactic.userName}
 
-    modify fun st => st.saveDomainObject tacticDomain tactic.internalName.toString id
+    modify fun st =>
+      st
+        |>.saveDomainObject tacticDomain tactic.internalName.toString id
+        |>.saveDomainObjectData tacticDomain tactic.internalName.toString (json%{"userName": $tactic.userName})
 
     pure none
   toHtml := some <| fun _goI goB id info contents =>
@@ -1690,7 +1693,8 @@ open Lean Elab Term Parser Tactic Doc in
 @[block_extension conv]
 def conv.descr : BlockDescr where
   init st := st
-    |>.setDomainTitle convDomain "Conversion Tactics" |>.setDomainDescription convDomain "Tatics for performing targeted rewriting of subterms"
+    |>.setDomainTitle convDomain "Conversion Tactics"
+    |>.setDomainDescription convDomain "Tactics for performing targeted rewriting of subterms"
 
   traverse id info _ := do
     let .ok (name, «show», _docs?) := FromJson.fromJson? (α := Name × String × Option String) info
@@ -1700,6 +1704,7 @@ def conv.descr : BlockDescr where
     Index.addEntry id {term := Doc.Inline.code <| «show»}
 
     modify fun st => st.saveDomainObject convDomain name.toString id
+    modify fun st => st.saveDomainObjectData convDomain name.toString (json%{"userName": $«show»})
 
     pure none
   toHtml := some <| fun _goI goB id info contents =>

diff --git a/src/verso-manual/VersoManual/Glossary.lean b/src/verso-manual/VersoManual/Glossary.lean
@@ -69,7 +69,6 @@ def deftech : RoleExpander
   | args, content => do
     let {key, normalize} ← TechArgs.parse.run args
 
-
     -- Heuristically guess at the string and key (usually works)
     let str := inlineToString (← getEnv) <| mkNullNode content
     let k := key.getD str
@@ -82,8 +81,9 @@ def deftech : RoleExpander
 
     let stx ←
       `(let content : Array (Doc.Inline Verso.Genre.Manual) := #[$content,*]
-        let k := ($(quote key) : Option String).getD (techString (Doc.Inline.concat content))
-        Doc.Inline.other {Inline.deftech with data := if $(quote normalize) then normString k else k} content)
+        let asString : String := techString (Doc.Inline.concat content)
+        let k : String := ($(quote key) : Option String).getD asString
+        Doc.Inline.other {Inline.deftech with data := ToJson.toJson (if $(quote normalize) then normString k else k, asString)} content)
     return #[stx]
 
 /-- Adds an internal identifier as a target for a given glossary entry -/
@@ -98,6 +98,10 @@ def Glossary.addEntry [Monad m] [MonadState TraverseState m] [MonadLiftT IO m] [
 
 @[inline_extension deftech]
 def deftech.descr : InlineDescr where
+  init st := st
+    |>.setDomainTitle technicalTermDomain "Terminology"
+    |>.setDomainDescription technicalTermDomain "Definitions of technical terms"
+
   traverse id data _contents := do
     -- TODO use internal tags in the first round to respect users' assignments (cf part tag assignment)
     let path ← (·.path) <$> read
@@ -106,9 +110,15 @@ def deftech.descr : InlineDescr where
     | .error err =>
       logError err
       return none
-    | .ok (key : String) =>
+    | .ok ((key, term) : (String × String) ) =>
       Glossary.addEntry id key
+      modify fun st =>
+        st
+          |>.saveDomainObject technicalTermDomain key id
+          |>.saveDomainObjectData technicalTermDomain key (json%{"term": $term})
+
       pure none
+
   toTeX :=
     some <| fun go _id _ content => do
       pure <| .seq <| ← content.mapM fun b => do

diff --git a/src/verso-manual/VersoManual/Html.lean b/src/verso-manual/VersoManual/Html.lean
@@ -479,6 +479,7 @@ def page
     (textTitle : String) (htmlTitle : Html) (contents : Html)
     (extraCss : HashSet String)
     (extraJs : HashSet String)
+    (extraHead : Array Html := #[])
     (showNavButtons : Bool := true)
     (base : Option String := none)
     (logo : Option String := none)
@@ -507,6 +508,7 @@ def page
         {{extraStylesheets.map (fun url => {{<link rel="stylesheet" href={{url}}/> }})}}
         {{extraCss.toArray.map ({{<style>{{Html.text false ·}}</style>}})}}
         {{extraJs.toArray.map ({{<script>{{Html.text false ·}}</script>}})}}
+        {{extraHead}}
       </head>
       <body>
         <label for="toggle-toc" id="toggle-toc-click">

diff --git a/src/verso-manual/VersoManual/Html/Style.lean b/src/verso-manual/VersoManual/Html/Style.lean
@@ -111,7 +111,7 @@ pre, code {
 
 .with-toc #toc {
     position: fixed;
-    z-index: 10;
+    z-index: 9;
 }
 
 /** Non-mobile **/