diff --git a/DocGen4/Output.lean b/DocGen4/Output.lean
index 7636deb..9c40844 100644
--- a/DocGen4/Output.lean
+++ b/DocGen4/Output.lean
@@ -35,6 +35,7 @@ def htmlOutputSetup (config : SiteBaseContext) : IO Unit := do
-- All the doc-gen static stuff
let indexHtml := ReaderT.run index config |>.toString
let notFoundHtml := ReaderT.run notFound config |>.toString
+ let navbarHtml := ReaderT.run navbar config |>.toString
let docGenStatic := #[
("style.css", styleCss),
("declaration-data.js", declarationDataCenterJs),
@@ -43,7 +44,8 @@ def htmlOutputSetup (config : SiteBaseContext) : IO Unit := do
("search.js", searchJs),
("mathjax-config.js", mathjaxConfigJs),
("index.html", indexHtml),
- ("404.html", notFoundHtml)
+ ("404.html", notFoundHtml),
+ ("navbar.html", navbarHtml)
]
for (fileName, content) in docGenStatic do
FS.writeFile (basePath / fileName) content
diff --git a/DocGen4/Output/Base.lean b/DocGen4/Output/Base.lean
index daf980d..0e6ea5a 100644
--- a/DocGen4/Output/Base.lean
+++ b/DocGen4/Output/Base.lean
@@ -215,4 +215,29 @@ partial def infoFormatToHtml (i : CodeWithInfos) : HtmlM (Array Html) := do
pure #[[←infoFormatToHtml t]]
| _ => pure #[[←infoFormatToHtml t]]
+def baseHtmlHead (title : String) : BaseHtmlM Html := do
+ pure
+
+ {title}
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
end DocGen4.Output
diff --git a/DocGen4/Output/Navbar.lean b/DocGen4/Output/Navbar.lean
index bf70e34..9f71f45 100644
--- a/DocGen4/Output/Navbar.lean
+++ b/DocGen4/Output/Navbar.lean
@@ -57,21 +57,26 @@ The main entry point to rendering the navbar on the left hand side.
-/
def navbar : BaseHtmlM Html := do
pure
-
+
+ {←baseHtmlHead "Navbar"}
+
+
+
+
end Output
end DocGen4
diff --git a/DocGen4/Output/Template.lean b/DocGen4/Output/Template.lean
index 49aa9f5..632e4e9 100644
--- a/DocGen4/Output/Template.lean
+++ b/DocGen4/Output/Template.lean
@@ -17,29 +17,7 @@ The HTML template used for all pages.
def baseHtmlGenerator (title : String) (site : Array Html) : BaseHtmlM Html := do
pure
-
-
- {title}
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
+ {←baseHtmlHead title}
@@ -57,7 +35,9 @@ def baseHtmlGenerator (title : String) (site : Array Html) : BaseHtmlM Html := d
[site]
- {←navbar}
+
diff --git a/static/style.css b/static/style.css
index fbf8614..4b35ab2 100644
--- a/static/style.css
+++ b/static/style.css
@@ -257,6 +257,11 @@ nav {
text-indent: -2ex; padding-left: 2ex;
}
+.navframe {
+ height: 100%;
+ width: 100%;
+}
+
.internal_nav .imports {
margin-bottom: 1rem;
}