diff --git a/DocGen4/Output.lean b/DocGen4/Output.lean
index 8d2b30e..2509c25 100644
--- a/DocGen4/Output.lean
+++ b/DocGen4/Output.lean
@@ -80,13 +80,14 @@ def htmlOutput (result : AnalyzerResult) (root : String) : IO Unit := do
declList := declList.push obj
let json := Json.arr declList
- FS.writeFile (basePath / "searchable_data.json") json.compress
+ FS.writeFile (basePath / "searchable-data.json") json.compress
FS.writeFile (basePath / "index.html") indexHtml.toString
FS.writeFile (basePath / "style.css") styleCss
FS.writeFile (basePath / "404.html") notFoundHtml.toString
FS.writeFile (basePath / "nav.js") navJs
FS.writeFile (basePath / "search.js") searchJs
FS.writeFile (basePath / "mathjax-config.js") mathjaxConfigJs
+ FS.writeFile (basePath / "site-root.js") s!"siteRoot = \"{config.root}\"";
for (module, content) in result.moduleInfo.toArray do
let moduleHtml := ReaderT.run (moduleToHtml content) config
let path := moduleNameToFile basePath module
diff --git a/DocGen4/Output/Template.lean b/DocGen4/Output/Template.lean
index 232df38..9181b47 100644
--- a/DocGen4/Output/Template.lean
+++ b/DocGen4/Output/Template.lean
@@ -18,7 +18,7 @@ def baseHtmlArray (title : String) (site : Array Html) : HtmlM Html := do
-
+
{title}
@@ -44,9 +44,7 @@ def baseHtmlArray (title : String) (site : Array Html) : HtmlM Html := do
{←navbar}
-- Lean in JS in HTML in Lean...very meta
-
+
-- TODO Add more js stuff
diff --git a/static/mathjax-config.js b/static/mathjax-config.js
index 51adbd6..9e470bc 100644
--- a/static/mathjax-config.js
+++ b/static/mathjax-config.js
@@ -1,17 +1,26 @@
+/*
+ * This file is for configing MathJax behavior.
+ * Seehttps://docs.mathjax.org/en/latest/web/configuration.html
+ */
+
+/**
+ * This configuration is copied from old doc-gen3
+ * https://github.com/leanprover-community/doc-gen
+ */
MathJax = {
- tex: {
- inlineMath: [['$', '$']],
- displayMath: [['$$', '$$']]
- },
- options: {
- skipHtmlTags: [
- 'script', 'noscript', 'style', 'textarea', 'pre',
- 'code', 'annotation', 'annotation-xml',
- 'decl', 'decl_meta', 'attributes', 'decl_args', 'decl_header', 'decl_name',
- 'decl_type', 'equation', 'equations', 'structure_field', 'structure_fields',
- 'constructor', 'constructors', 'instances'
- ],
- ignoreHtmlClass: 'tex2jax_ignore',
- processHtmlClass: 'tex2jax_process',
- },
+ tex: {
+ inlineMath: [['$', '$']],
+ displayMath: [['$$', '$$']]
+ },
+ options: {
+ skipHtmlTags: [
+ 'script', 'noscript', 'style', 'textarea', 'pre',
+ 'code', 'annotation', 'annotation-xml',
+ 'decl', 'decl_meta', 'attributes', 'decl_args', 'decl_header', 'decl_name',
+ 'decl_type', 'equation', 'equations', 'structure_field', 'structure_fields',
+ 'constructor', 'constructors', 'instances'
+ ],
+ ignoreHtmlClass: 'tex2jax_ignore',
+ processHtmlClass: 'tex2jax_process',
+ },
};
\ No newline at end of file
diff --git a/static/nav.js b/static/nav.js
index b741863..75b82fd 100644
--- a/static/nav.js
+++ b/static/nav.js
@@ -106,7 +106,7 @@ if (tse != null) {
// Simple declaration search
// -------------------------
-const declURL = new URL(`${siteRoot}searchable_data.json`, window.location);
+const declURL = new URL(`${siteRoot}searchable-data.json`, window.location);
const getDecls = (() => {
let decls;
return () => {