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 -- mathjax + 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