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

feat: Use iframe for navbar to move it into the finalize stage

main
Henrik Böving 2022-07-21 22:06:26 +02:00
parent 80cf5bc96f
commit 80cb92eb94
5 changed files with 57 additions and 40 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
DocGen4/Output.lean
View File

@ -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

25
DocGen4/Output/Base.lean
View File

@ -215,4 +215,29 @@ 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"}/>
<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

35
DocGen4/Output/Navbar.lean
View File

@ -57,21 +57,26 @@ The main entry point to rendering the navbar on the left hand side.
-/
def navbar : BaseHtmlM Html := do
pure
<nav class="nav">
<h3>General documentation</h3>
<div class="nav_link"><a href={s!"{←getRoot}"}>index</a></div>
/-
TODO: Add these in later
<div class="nav_link"><a href={s!"{←getRoot}tactics.html"}>tactics</a></div>
<div class="nav_link"><a href={s!"{←getRoot}commands.html"}>commands</a></div>
<div class="nav_link"><a href={s!"{←getRoot}hole_commands.html"}>hole commands</a></div>
<div class="nav_link"><a href={s!"{←getRoot}attributes.html"}>attributes</a></div>
<div class="nav_link"><a href={s!"{←getRoot}notes.html"}>notes</a></div>
<div class="nav_link"><a href={s!"{←getRoot}references.html"}>references</a></div>
-/
<h3>Library</h3>
{← moduleList}
</nav>
<html lang="en">
{←baseHtmlHead "Navbar"}
<body>
<nav class="nav">
<h3>General documentation</h3>
<div class="nav_link"><a href={s!"{←getRoot}"}>index</a></div>
/-
TODO: Add these in later
<div class="nav_link"><a href={s!"{←getRoot}tactics.html"}>tactics</a></div>
<div class="nav_link"><a href={s!"{←getRoot}commands.html"}>commands</a></div>
<div class="nav_link"><a href={s!"{←getRoot}hole_commands.html"}>hole commands</a></div>
<div class="nav_link"><a href={s!"{←getRoot}attributes.html"}>attributes</a></div>
<div class="nav_link"><a href={s!"{←getRoot}notes.html"}>notes</a></div>
<div class="nav_link"><a href={s!"{←getRoot}references.html"}>references</a></div>
-/
<h3>Library</h3>
{← moduleList}
</nav>
</body>
</html>
end Output
end DocGen4

28
DocGen4/Output/Template.lean
View File

@ -17,29 +17,7 @@ The HTML template used for all pages.
def baseHtmlGenerator (title : String) (site : Array Html) : BaseHtmlM Html := do
pure
<html lang="en">
<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"}/>
<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>
</head>
{←baseHtmlHead title}
<body>
<input id="nav_toggle" type="checkbox"/>
@ -57,7 +35,9 @@ def baseHtmlGenerator (title : String) (site : Array Html) : BaseHtmlM Html := d
[site]
{←navbar}
<nav class="nav">
<iframe src={s!"{←getRoot}/navbar.html"} class="navframe" frameBorder="0"></iframe>
</nav>
</body>

5
static/style.css
View File

@ -257,6 +257,11 @@ nav {
text-indent: -2ex; padding-left: 2ex;
}
.navframe {
height: 100%;
width: 100%;
}
.internal_nav .imports {
margin-bottom: 1rem;
}