feat: allow manual genre to add custom elements to HTML <head>

leanprover · Jan 10, 2025 · fc18d3d · fc18d3d
1 parent 7bd1a44
commit fc18d3d
Show file tree

Hide file tree

Showing 2 changed files with 7 additions and 2 deletions.
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
@@ -269,7 +271,7 @@ partial def toc (depth : Nat) (opts : Html.Options Manual IO)
       children := children.toList
     }
 
-def page (toc : List Html.Toc) (path : Path) (textTitle : String) (htmlTitle contents : Html) (state : TraverseState) (config : Config) (showNavButtons : Bool := true) (extraJs : List String := []) : Html :=
+def page (toc : List Html.Toc) (path : Path) (textTitle : String) (htmlTitle contents : Html) (state : TraverseState) (config : Config) (showNavButtons : Bool := true) (extraJs : List String := []) (extraHead : Array Html := #[]) : Html :=
   let toc := {
     title := htmlTitle, path := #[], id := "" , sectionNum := some #[], children := toc
   }
@@ -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 := 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/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">