From 5dc3ab855f16383d809fb925301e27d8fc5d45d5 Mon Sep 17 00:00:00 2001
From: Xubai Wang <self@xubai.wang>
Date: Fri, 18 Feb 2022 03:27:00 +0800
Subject: [PATCH] feat: config mathjax like doc-gen

---
 DocGen4/Output.lean          |  1 +
 DocGen4/Output/Base.lean     |  1 +
 DocGen4/Output/Template.lean |  1 +
 static/mathjax-config.js     | 17 +++++++++++++++++
 4 files changed, 20 insertions(+)
 create mode 100644 static/mathjax-config.js

diff --git a/DocGen4/Output.lean b/DocGen4/Output.lean
index 1cc370d..734bb34 100644
--- a/DocGen4/Output.lean
+++ b/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
diff --git a/DocGen4/Output/Base.lean b/DocGen4/Output/Base.lean
index 485739b..4579f69 100644
--- a/DocGen4/Output/Base.lean
+++ b/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
diff --git a/DocGen4/Output/Template.lean b/DocGen4/Output/Template.lean
index cd6509e..8ed58ee 100644
--- a/DocGen4/Output/Template.lean
+++ b/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>
diff --git a/static/mathjax-config.js b/static/mathjax-config.js
new file mode 100644
index 0000000..51adbd6
--- /dev/null
+++ b/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',
+    },
+};
\ No newline at end of file