Sorry, what we actually need: pandoc KaTeX

lukstafi · Oct 26, 2023 · 5536b8a · 5536b8a
1 parent 4af4d46
commit 5536b8a
Show file tree

Hide file tree

Showing 3 changed files with 989 additions and 995 deletions.
diff --git a/site/dune b/site/dune
@@ -31,7 +31,7 @@
  (target new_book.html)
  (deps README.md)
  (action
-  (system "pandoc -s %{deps} -o %{target} --metadata title='Curious OCaml'")))
+  (system "pandoc -s %{deps} -o %{target} --katex --metadata title='Curious OCaml'")))
 
 (rule
  (alias old_lectures_as_book)
@@ -40,4 +40,4 @@
  (deps old_lectures_as_book.md)
  (action
   (system
-   "pandoc -s %{deps} -o %{target} --metadata title='Functional Programming Course'")))
+   "pandoc -s %{deps} -o %{target} --katex --metadata title='Functional Programming Course'")))
diff --git a/site/new_book.html b/site/new_book.html
@@ -152,8 +152,25 @@
     div.column{display: inline-block; vertical-align: top; width: 50%;}
     div.hanging-indent{margin-left: 1.5em; text-indent: -1.5em;}
     ul.task-list{list-style: none;}
-    .display.math{display: block; text-align: center; margin: 0.5rem auto;}
   </style>
+  <script defer=""
+  src="/usr/share/javascript/katex/katex.min.js"></script>
+  <script>document.addEventListener("DOMContentLoaded", function () {
+ var mathElements = document.getElementsByClassName("math");
+ var macros = [];
+ for (var i = 0; i < mathElements.length; i++) {
+  var texText = mathElements[i].firstChild;
+  if (mathElements[i].tagName == "SPAN") {
+   katex.render(texText.data, mathElements[i], {
+    displayMode: mathElements[i].classList.contains('display'),
+    throwOnError: false,
+    macros: macros,
+    fleqn: false
+   });
+}}});
+  </script>
+  <link rel="stylesheet"
+  href="/usr/share/javascript/katex/katex.min.css" />
 </head>
 <body>
 <header id="title-block-header">
@@ -174,20 +191,20 @@ <h1 id="from-logic-rules-to-programming-constructs">From logic rules to
 </colgroup>
 <thead>
 <tr class="header">
-<th><span class="math inline">⊤</span></th>
-<th><span class="math inline">⊥</span></th>
-<th><span class="math inline">∧</span></th>
-<th><span class="math inline">∨</span></th>
-<th><span class="math inline">→</span></th>
+<th><span class="math inline">\top</span></th>
+<th><span class="math inline">\bot</span></th>
+<th><span class="math inline">\wedge</span></th>
+<th><span class="math inline">\vee</span></th>
+<th><span class="math inline">\rightarrow</span></th>
 </tr>
 </thead>
 <tbody>
 <tr class="odd">
 <td></td>
 <td></td>
-<td><span class="math inline"><em>a</em> ∧ <em>b</em></span></td>
-<td><span class="math inline"><em>a</em> ∨ <em>b</em></span></td>
-<td><span class="math inline"><em>a</em> → <em>b</em></span></td>
+<td><span class="math inline">a \wedge b</span></td>
+<td><span class="math inline">a \vee b</span></td>
+<td><span class="math inline">a \rightarrow b</span></td>
 </tr>
 <tr class="even">
 <td>truth</td>
@@ -199,39 +216,39 @@ <h1 id="from-logic-rules-to-programming-constructs">From logic rules to
 <tr class="odd">
 <td>“trivial”</td>
 <td>“impossible”</td>
-<td><span class="math inline"><em>a</em></span> and <span
-class="math inline"><em>b</em></span></td>
-<td><span class="math inline"><em>a</em></span> or <span
-class="math inline"><em>b</em></span></td>
-<td><span class="math inline"><em>a</em></span> gives <span
-class="math inline"><em>b</em></span></td>
+<td><span class="math inline">a</span> and <span
+class="math inline">b</span></td>
+<td><span class="math inline">a</span> or <span
+class="math inline">b</span></td>
+<td><span class="math inline">a</span> gives <span
+class="math inline">b</span></td>
 </tr>
 <tr class="even">
 <td></td>
 <td>shouldn’t get</td>
 <td>got both</td>
 <td>got at least one</td>
-<td>given <span class="math inline"><em>a</em></span>, we get <span
-class="math inline"><em>b</em></span></td>
+<td>given <span class="math inline">a</span>, we get <span
+class="math inline">b</span></td>
 </tr>
 </tbody>
 </table>
 <p>How can we define them? Think in terms of <em>derivation
 trees</em>:</p>
-<p><span class="math display">$$
+<p><span class="math display">
 \frac{
 \frac{\frac{\,}{\text{a premise}} \; \frac{\,}{\text{another
 premise}}}{\frac{\,}{\text{some fact}}} \;
 \frac{\frac{\,}{\text{a premise}} \; \frac{\,}{\text{another
 premise}}}{\frac{\,}{\text{another fact}}}}
 {\text{final conclusion}}
-$$</span></p>
+</span></p>
 <p>To define the connectives, we provide rules for using them: for
-example, a rule <span class="math inline">$\frac{a \; b}{c}$</span>
+example, a rule <span class="math inline">\frac{a \; b}{c}</span>
 matches parts of the tree that have two premises, represented by
-variables <span class="math inline"><em>a</em></span> and <span
-class="math inline"><em>b</em></span>, and have any conclusion,
-represented by variable <span class="math inline"><em>c</em></span>.</p>
+variables <span class="math inline">a</span> and <span
+class="math inline">b</span>, and have any conclusion, represented by
+variable <span class="math inline">c</span>.</p>
 <h2 id="rules-for-logical-connectives">Rules for Logical
 Connectives</h2>
 <p>Introduction rules say how to produce a connective. Elimination rules