Merge pull request #230 from HEPLean/DocPreface

Docs: Update header of doc pages
2024-11-07 18:21:08 +00:00 · 2024-11-07 18:21:08 +00:00 · e2f06dd57f
commit e2f06dd57f
parent 1a8bc9bf61 f66cfa9a78
2 changed files with 92 additions and 0 deletions
--- a/.github/workflows/docs.yml
+++ b/.github/workflows/docs.yml
@ -50,6 +50,9 @@ jobs:
      - name: Generate svg from dot
        run : dot -Tsvg -o ./docs/graph.svg ./docs/InformalDot.dot

+      - name: Replace template file with custom
+        run : cp ./scripts/Template.lean .lake/packages/doc-gen4/DocGen4/Output/Template.lean
+
      - name: Get doc cache
        uses: actions/cache@v3
        with:
--- a/scripts/Template.lean
+++ b/scripts/Template.lean
@ -0,0 +1,89 @@
+/-
+
+Modified from:
+
+https://github.com/leanprover/doc-gen4/blob/main/DocGen4/Output/Template.lean
+
+Copyright (c) 2021 Henrik Böving. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Henrik Böving
+
+Modifications include: Style changes.
+
+Test these changes with:
+- cp ./scripts/Template.lean .lake/packages/doc-gen4/DocGen4/Output/Template.lean
+- lake -Kenv=dev build Batteries:docs; rm -rf ./docs/docs; mv .lake/build/doc docs/docs
+- cd ./docs
+- bundle exec jekyll serve
+
+-/
+import DocGen4.Output.ToHtmlFormat
+import DocGen4.Output.Navbar
+
+namespace DocGen4
+namespace Output
+
+open scoped DocGen4.Jsx
+
+/--
+The HTML template used for all pages.
+-/
+def baseHtmlGenerator (title : String) (site : Array Html) : BaseHtmlM Html := do
+  let moduleConstant :=
+    if let some module := ← getCurrentName then
+      #[<script>{.raw s!"const MODULE_NAME={String.quote module.toString};"}</script>]
+    else
+      #[]
+  pure
+    <html lang="en">
+      <head>
+        [← baseHtmlHeadDeclarations]
+
+        <title>{title}</title>
+        <script defer="true" src={s!"{← getRoot}mathjax-config.js"}></script>
+        <script defer="true" src="https://cdnjs.cloudflare.com/polyfill/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>{.raw s!"const SITE_ROOT={String.quote (← getRoot)};"}</script>
+        [moduleConstant]
+        <script type="module" src={s!"{← getRoot}jump-src.js"}></script>
+        <script type="module" src={s!"{← getRoot}search.js"}></script>
+        <script type="module" src={s!"{← getRoot}expand-nav.js"}></script>
+        <script type="module" src={s!"{← getRoot}how-about.js"}></script>
+        <script type="module" src={s!"{← getRoot}instances.js"}></script>
+        <script type="module" src={s!"{← getRoot}importedBy.js"}></script>
+      </head>
+
+      <body>
+
+        <input id="nav_toggle" type="checkbox"/>
+
+        <header style="background-color: #2C3E50; color: #fff;">
+          <h1><label for="nav_toggle"></label><span>
+          <a href="https://heplean.github.io/HepLean/" style="color: #fff; text-decoration: none; font-family: serif">
+          HepLean Documentation</a>
+          </span></h1>
+          <h2  style="color: #fff; font-family: serif">[breakWithin title]</h2>
+          <form action="https://google.com/search" method="get" id="search_form">
+            <input type="hidden" name="sitesearch" value="https://leanprover-community.github.io/mathlib4_docs"/>
+            <input type="text" name="q" autocomplete="off"/>{.raw "&#32;"}
+            <button id="search_button" onclick={s!"javascript: form.action='{← getRoot}search.html';"}>Search</button>
+            <button>Google site search</button>
+          </form>
+        </header>
+
+        [site]
+
+        <nav class="nav">
+          <iframe src={s!"{← getRoot}navbar.html"} class="navframe" frameBorder="0"></iframe>
+        </nav>
+      </body>
+    </html>
+
+/--
+A comfortability wrapper around `baseHtmlGenerator`.
+-/
+def baseHtml (title : String) (site : Html) : BaseHtmlM Html := baseHtmlGenerator title #[site]
+
+end Output
+end DocGen4