From 0cff3d7cda28818334b8769260de77970ccfcb32 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Henrik=20B=C3=B6ving?= Date: Thu, 21 Jul 2022 23:01:15 +0200 Subject: [PATCH] fix: Javascript errors in the navbar --- DocGen4/Output/Base.lean | 33 +++++++++------------------------ DocGen4/Output/Navbar.lean | 7 ++++++- DocGen4/Output/Template.lean | 17 ++++++++++++++--- 3 files changed, 29 insertions(+), 28 deletions(-) diff --git a/DocGen4/Output/Base.lean b/DocGen4/Output/Base.lean index 0e6ea5a..976b711 100644 --- a/DocGen4/Output/Base.lean +++ b/DocGen4/Output/Base.lean @@ -215,29 +215,14 @@ partial def infoFormatToHtml (i : CodeWithInfos) : HtmlM (Array Html) := do pure #[[←infoFormatToHtml t]] | _ => pure #[[←infoFormatToHtml t]] -def baseHtmlHead (title : String) : BaseHtmlM Html := do - pure - - {title} - - - - - - - - - - - - - - - - - - - - +def baseHtmlHeadDeclarations : BaseHtmlM (Array Html) := do + pure #[ + , + , + , + , + , + + ] end DocGen4.Output diff --git a/DocGen4/Output/Navbar.lean b/DocGen4/Output/Navbar.lean index 9f71f45..eea77f0 100644 --- a/DocGen4/Output/Navbar.lean +++ b/DocGen4/Output/Navbar.lean @@ -58,7 +58,12 @@ The main entry point to rendering the navbar on the left hand side. def navbar : BaseHtmlM Html := do pure - {←baseHtmlHead "Navbar"} + + [←baseHtmlHeadDeclarations] + + + +