Make basic math work

utensil · Oct 27, 2024 · ba64d4d · ba64d4d
1 parent 9dae348
commit ba64d4d
Show file tree

Hide file tree

Showing 4 changed files with 64 additions and 1 deletion.
diff --git a/lean4-verso-xp/Main.lean b/lean4-verso-xp/Main.lean
@@ -7,9 +7,10 @@ def main :=
   manualMain (%doc VersoXp) (config := config)
 where
   config := {
-    -- extraFiles := [("static", "static")],
+    extraFiles := [("static", "static")],
     -- extraCss := ["/static/colors.css", "/static/theme.css", "/static/print.css", "/static/fonts/source-serif/source-serif-text.css", "/static/fonts/source-code-pro/source-code-pro.css", "/static/katex/katex.min.css"],
     -- extraJs := ["/static/katex/katex.min.js", "/static/math.js", "/static/print.js"],
+    extraJs := ["/static/math.js"],
     emitTeX := false,
     -- emitHtmlSingle := true, -- for proofreading
     -- logo := some "/static/lean_logo.svg",

diff --git a/lean4-verso-xp/VersoXp.lean b/lean4-verso-xp/VersoXp.lean
@@ -1,6 +1,7 @@
 import VersoManual
 
 import VersoXp.Basic
+import VersoXp.Math
 
 open Verso.Genre Manual
 
@@ -15,3 +16,5 @@ This is a Verso exploration.
 
 {include VersoXp.Basic}
 
+{include VersoXp.Math}
+
diff --git a/lean4-verso-xp/VersoXp/Math.lean b/lean4-verso-xp/VersoXp/Math.lean
@@ -0,0 +1,24 @@
+import VersoManual
+
+open Lean.MessageSeverity
+
+open Verso.Genre Manual
+
+set_option pp.rawOnError true
+
+#doc (Manual) "Math" =>
+%%%
+htmlSplit := .never
+tag := "math"
+%%%
+
+Inline math:
+
+$`E=mc^2`
+
+Display math:
+
+$$`E=mc^2`
+
+❌ But no support for multiline math yet.
+
diff --git a/lean4-verso-xp/static/math.js b/lean4-verso-xp/static/math.js
@@ -0,0 +1,35 @@
+const load_script = (src, onload) => {
+    console.debug(`loading ${src}`)
+    const script = document.createElement('script')
+    // script.type = 'module'
+    script.src = src
+    script.setAttribute('onload', onload)
+    document.head.appendChild(script)
+}
+
+const load_css = (href) => {
+    console.debug(`loading ${href}`)
+    const link = document.createElement('link')
+    link.rel = 'stylesheet'
+    link.href = href
+    document.head.appendChild(link)
+}
+
+const render = () => {
+    for (const m of document.querySelectorAll(".math.inline")) {
+        katex.render(m.textContent, m, {throwOnError: false, displayMode: false});
+    }
+    for (const m of document.querySelectorAll(".math.display")) {
+        katex.render(m.textContent, m, {throwOnError: false, displayMode: true});
+    }
+}
+
+load_css('https://cdn.jsdelivr.net/npm/katex@0.16.11/dist/katex.min.css')
+load_script('https://cdn.jsdelivr.net/npm/katex@0.16.11/dist/katex.min.js', 'render();')
+// load_script('https://cdn.jsdelivr.net/npm/katex@0.16.11/dist/contrib/auto-render.min.js', 'renderMathInElement(document.body);')
+// https://github.com/leanprover/reference-manual/blob/main/static/math.js
+
+// document.addEventListener("DOMContentLoaded", () => {
+
+// });
+