r
/
bookshelf-doc
mirror of https://github.com/jrpotter/bookshelf-doc
1
Fork 0
Code Issues Packages Projects Releases Wiki Activity

fix: Javascript errors in the navbar

main
Henrik Böving 2022-07-21 23:01:15 +02:00
parent eea23d332a
commit 0cff3d7cda
3 changed files with 29 additions and 28 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

31
DocGen4/Output/Base.lean
View File

@ -215,29 +215,14 @@ partial def infoFormatToHtml (i : CodeWithInfos) : HtmlM (Array Html) := do
pure #[<span class="fn">[←infoFormatToHtml t]</span>]
| _ => pure #[<span class="fn">[←infoFormatToHtml t]</span>]
def baseHtmlHead (title : String) : BaseHtmlM Html := do
pure
<head>
<title>{title}</title>
<meta charset="UTF-8"/>
<meta name="viewport" content="width=device-width, initial-scale=1"/>
<link rel="stylesheet" href={s!"{←getRoot}style.css"}/>
<link rel="stylesheet" href={s!"{←getRoot}pygments.css"}/>
<link rel="shortcut icon" href={s!"{←getRoot}favicon.ico"}/>
def baseHtmlHeadDeclarations : BaseHtmlM (Array Html) := do
pure #[
<meta charset="UTF-8"/>,
<meta name="viewport" content="width=device-width, initial-scale=1"/>,
<link rel="stylesheet" href={s!"{←getRoot}style.css"}/>,
<link rel="stylesheet" href={s!"{←getRoot}pygments.css"}/>,
<link rel="shortcut icon" href={s!"{←getRoot}favicon.ico"}/>,
<link rel="prefetch" href={s!"{←getRoot}declaration-data.bmp"}/>
<script defer="true" src={s!"{←getRoot}mathjax-config.js"}></script>
<script defer="true" src="https://polyfill.io/v3/polyfill.min.js?features=es6"></script>
<script defer="true" src="https://cdn.jsdelivr.net/npm/mathjax@3/es5/tex-mml-chtml.js"></script>
<script>{s!"const SITE_ROOT={String.quote (←getRoot)};"}</script>
<script type="module" src={s!"{←getRoot}nav.js"}></script>
<script type="module" src={s!"{←getRoot}search.js"}></script>
<script type="module" src={s!"{←getRoot}how-about.js"}></script>
<base target="_parent" />
</head>
]
end DocGen4.Output

7
DocGen4/Output/Navbar.lean
View File

@ -58,7 +58,12 @@ The main entry point to rendering the navbar on the left hand side.
def navbar : BaseHtmlM Html := do
pure
<html lang="en">
{←baseHtmlHead "Navbar"}
<head>
[←baseHtmlHeadDeclarations]
<base target="_parent" />
</head>
<body>
<nav class="nav">
<h3>General documentation</h3>

17
DocGen4/Output/Template.lean
View File

@ -17,7 +17,20 @@ The HTML template used for all pages.
def baseHtmlGenerator (title : String) (site : Array Html) : BaseHtmlM Html := do
pure
<html lang="en">
{←baseHtmlHead title}
<head>
[←baseHtmlHeadDeclarations]
<title>{title}</title>
<script defer="true" src={s!"{←getRoot}mathjax-config.js"}></script>
<script defer="true" src="https://polyfill.io/v3/polyfill.min.js?features=es6"></script>
<script defer="true" src="https://cdn.jsdelivr.net/npm/mathjax@3/es5/tex-mml-chtml.js"></script>
<script>{s!"const SITE_ROOT={String.quote (←getRoot)};"}</script>
<script type="module" src={s!"{←getRoot}nav.js"}></script>
<script type="module" src={s!"{←getRoot}search.js"}></script>
<script type="module" src={s!"{←getRoot}how-about.js"}></script>
</head>
<body>
<input id="nav_toggle" type="checkbox"/>
@ -38,9 +51,7 @@ def baseHtmlGenerator (title : String) (site : Array Html) : BaseHtmlM Html := d
<nav class="nav">
<iframe src={s!"{←getRoot}/navbar.html"} class="navframe" frameBorder="0"></iframe>
</nav>
</body>
</html>
/--