From 80cb92eb94686319f2aa60b3d06969bcd3d9cd44 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Henrik=20B=C3=B6ving?= Date: Thu, 21 Jul 2022 22:06:26 +0200 Subject: [PATCH] feat: Use iframe for navbar to move it into the finalize stage --- DocGen4/Output.lean | 4 +++- DocGen4/Output/Base.lean | 25 +++++++++++++++++++++++++ DocGen4/Output/Navbar.lean | 35 ++++++++++++++++++++--------------- DocGen4/Output/Template.lean | 28 ++++------------------------ static/style.css | 5 +++++ 5 files changed, 57 insertions(+), 40 deletions(-) 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; }