diff --git a/src/verso-manual/VersoManual.lean b/src/verso-manual/VersoManual.lean
index 721c8aa..4693ba1 100644
--- 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
index 27c9408..d70315b 100644
--- 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 => {{ }})}}
{{extraCss.toArray.map ({{}})}}
{{extraJs.toArray.map ({{}})}}
+ {{extraHead}}