From 14e42f65ceb24ed69bdf2f178f008e92290dd129 Mon Sep 17 00:00:00 2001
From: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com>
Date: Thu, 7 Nov 2024 17:01:41 +0000
Subject: [PATCH] docs: Modify doc template
---
.github/workflows/docs.yml | 4 ++
scripts/Template.lean | 89 ++++++++++++++++++++++++++++++++++++++
2 files changed, 93 insertions(+)
create mode 100644 scripts/Template.lean
diff --git a/.github/workflows/docs.yml b/.github/workflows/docs.yml
index 9590ca8..2aee321 100644
--- a/.github/workflows/docs.yml
+++ b/.github/workflows/docs.yml
@@ -2,6 +2,7 @@ on:
push:
branches:
- master
+ - DocPreface
name: Build and deploy documentation
@@ -50,6 +51,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:
diff --git a/scripts/Template.lean b/scripts/Template.lean
new file mode 100644
index 0000000..fb83020
--- /dev/null
+++ 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
+ #[]
+ else
+ #[]
+ pure
+
+
+ [← baseHtmlHeadDeclarations]
+
+ {title}
+
+
+
+
+
+ [moduleConstant]
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+ [breakWithin title]
+
+
+
+ [site]
+
+
+
+
+
+/--
+A comfortability wrapper around `baseHtmlGenerator`.
+-/
+def baseHtml (title : String) (site : Html) : BaseHtmlM Html := baseHtmlGenerator title #[site]
+
+end Output
+end DocGen4