From a89cf7d7a4c26a83ff5f0da9758f97c3c237819e Mon Sep 17 00:00:00 2001
From: Xubai Wang <self@xubai.wang>
Date: Sun, 20 Feb 2022 23:24:08 +0800
Subject: [PATCH] refactor: move siteRoot to separate file

---
 DocGen4/Output.lean          |  3 ++-
 DocGen4/Output/Template.lean |  6 ++----
 static/mathjax-config.js     | 39 ++++++++++++++++++++++--------------
 static/nav.js                |  2 +-
 4 files changed, 29 insertions(+), 21 deletions(-)

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
         <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}searchable_data.json"}/>
+        <link rel="prefetch" href={s!"{←getRoot}searchable-data.json"}/>
         <title>{title}</title>
         <meta charset="UTF-8"/>
         <meta name="viewport" content="width=device-width, initial-scale=1"/>
@@ -44,9 +44,7 @@ def baseHtmlArray (title : String) (site : Array Html) : HtmlM Html := do
       {←navbar}
 
       -- Lean in JS in HTML in Lean...very meta
-      <script>
-        siteRoot = "{←getRoot}";
-      </script>
+      <script src={s!"{←getRoot}site-root.js"}></script>
 
       -- TODO Add more js stuff
       <script src={s!"{←getRoot}nav.js"}></script>
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 () => {