feat: config mathjax like doc-gen

DocGen4/Output.lean

@@ -86,6 +86,7 @@ def htmlOutput (result : AnalyzerResult) (root : String) : IO Unit := do
   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
   for (module, content) in result.moduleInfo.toArray do
     let moduleHtml := ReaderT.run (moduleToHtml content) config
     let path := moduleNameToFile basePath module

DocGen4/Output/Base.lean

@@ -49,6 +49,7 @@ section Static
   def styleCss : String := include_str "./static/style.css"
   def navJs : String := include_str "./static/nav.js"
   def searchJs : String := include_str "./static/search.js"
+  def mathjaxConfigJs : String := include_str "./static/mathjax-config.js"
 end Static
 
 def declNameToLink (name : Name) : HtmlM String := do

DocGen4/Output/Template.lean

@@ -51,6 +51,7 @@ def baseHtmlArray (title : String) (site : Array Html) : HtmlM Html := do
       <script src={s!"{←getRoot}nav.js"}></script>
       <script src={s!"{←getRoot}search.js"}></script>
       -- mathjax
+      <script src={s!"{←getRoot}mathjax-config.js"}></script>
       <script src="https://polyfill.io/v3/polyfill.min.js?features=es6"></script>
       <script src="https://cdn.jsdelivr.net/npm/mathjax@3/es5/tex-mml-chtml.js"></script>
       </body>

static/mathjax-config.js

@@ -0,0 +1,17 @@
+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',
+    },
+};