refactor: move siteRoot to separate file

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

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>
+      <script src={s!"{←getRoot}site-root.js"}></script>
-        siteRoot = "{←getRoot}";
-      </script>
 
       -- TODO Add more js stuff
       <script src={s!"{←getRoot}nav.js"}></script>

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: {
+  tex: {
-        inlineMath: [['$', '$']],
+    inlineMath: [['$', '$']],
-        displayMath: [['$$', '$$']]
+    displayMath: [['$$', '$$']]
-    },
+  },
-    options: {
+  options: {
-        skipHtmlTags: [
+    skipHtmlTags: [
-            'script', 'noscript', 'style', 'textarea', 'pre',
+      'script', 'noscript', 'style', 'textarea', 'pre',
-            'code', 'annotation', 'annotation-xml',
+      'code', 'annotation', 'annotation-xml',
-            'decl', 'decl_meta', 'attributes', 'decl_args', 'decl_header', 'decl_name',
+      'decl', 'decl_meta', 'attributes', 'decl_args', 'decl_header', 'decl_name',
-            'decl_type', 'equation', 'equations', 'structure_field', 'structure_fields',
+      'decl_type', 'equation', 'equations', 'structure_field', 'structure_fields',
-            'constructor', 'constructors', 'instances'
+      'constructor', 'constructors', 'instances'
-        ],
+    ],
-        ignoreHtmlClass: 'tex2jax_ignore',
+    ignoreHtmlClass: 'tex2jax_ignore',
-        processHtmlClass: 'tex2jax_process',
+    processHtmlClass: 'tex2jax_process',
-    },
+  },
 };

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 () => {