add prooftree.js

README.md

@@ -6,6 +6,15 @@ Render proof tree in bussproofs into html
 
 右ラベル前提とする．
 
+## Memo
+
+How to build:
+
+```bash
+yarn build
+cp proof-tree/dist/index.js docs/assets/prooftree.js
+```
+
 ## 処理の流れ
 
 1. KaTeX を適用して，数式部分をレンダリングする．

docs/assets/prooftree.js

@@ -1,10 +1,10 @@
-const V = "div.prooftree,div.prtr-proof-tree{width:fit-content;margin:20px auto}div.prtr-sequent{width:auto;text-align:center}div.prtr-premises{width:auto;display:flex;flex-direction:row;gap:20px;align-items:flex-end}div.prtr-horizontal-rule{width:100%;border-bottom:1.3px solid;position:relative}div.prtr-horizontal-rule>.prtr-right-label{position:absolute;height:auto;top:-50%;right:0;-webkit-transform:translateY(-50%);transform:translateY(-50%)}", $ = () => {
+const V = "div.prooftree,div.prtr-proof-tree{width:fit-content;margin:20px auto}div.prtr-sequent{width:auto;text-align:center}div.prtr-premises{width:auto;display:flex;flex-direction:row;gap:20px;align-items:flex-end}div.prtr-horizontal-rule{width:100%;border-bottom:1.3px solid;position:relative}div.prtr-horizontal-rule>.prtr-right-label{position:absolute;height:auto;top:-50%;right:0;-webkit-transform:translateY(-50%);transform:translateY(-50%)}", O = () => {
   const t = document.createElement("style");
   t.innerHTML = V, document.head.appendChild(t);
   const n = Array.from(
     document.body.getElementsByTagName("P")
   ).filter(
-    (o) => o.innerText.includes("\\begin{prooftree}")
+    (o) => o.innerHTML.includes("\\begin{prooftree}")
   );
   console.log("nodes", n), console.log(n.map((o) => w(o))), n.forEach((o) => L(o));
 }, L = (t) => {
@@ -289,5 +289,5 @@ const S = (t) => t.reduce((e, n) => e + n, 0), E = (t) => {
   });
 };
 export {
-  $ as renderProofTrees
+  O as renderProofTrees
 };

docs/test.md

@@ -0,0 +1,127 @@
+---
+marp: true
+footer: Powered by Aqua / Marp
+paginate: true
+headingDivider: 1
+theme: aqua
+math: katex
+---
+
+<script type="text/javascript" class="next-head">
+console.log("hello world!")
+</script>
+
+# Proof Tree Renderer
+
+foo
+hige
+fai
+\begin{prooftree}
+\AXC{$1 + 2 + 3 + 4 + 5$}
+\RightLabel{Label 1}
+\UIC{$1 + 2 + 3$}
+\AXC{$1 + 2$}
+\RightLabel{Long Label 2}
+\UIC{$1 + 2 + 3$}
+\RightLabel{Label 3}
+\BIC{$1 + 2$}
+\AXC{$1 + 2$}
+\RightLabel{Label 4}
+\UIC{$1 + 2 + 3 + 4 + 5$}
+\RightLabel{Label 5}
+\BIC{$1 + 2 + 3 + 4 + 5 + 6 + 7 + 8 + 9 + 10 + 
+11 + 12 + 13 + 14 + 15 + 16 + 17 + 18 + 19 + 20 +
+21 + 22 + 23
+$}
+\end{prooftree}
+hoef barbar
+foo
+<span>
+foooo</span>
+hige
+fai
+\begin{prooftree}
+\AXC{$1 + 2 + 3 + 4 + 5$}
+\RightLabel{Label 1}
+\UIC{$1 + 2 + 3$}
+\AXC{$1 + 2$}
+\RightLabel{Long Label 2}
+\UIC{$1 + 2 + 3$}
+\RightLabel{Label 3}
+\BIC{$1 + 2$}
+\AXC{$1 + 2$}
+\RightLabel{Long Long Long Long Long Long Long
+Long Long Long Long Long Label 4}
+\UIC{$1 + 2 + 3 + 4 + 5$}
+\RightLabel{Label 5}
+\BIC{$1 + 2 + 3$}
+\RightLabel{Label 6}
+\UIC{$1 + 2 + 3 + 4 + 5 + 6 + 7 + 8 + 9 + 10 + 
+11 + 12 + 13 + 14 + 15 + 16 + 17 + 18 + 19 + 20 + 
+21 + 22 + 23
+$}
+\end{prooftree}
+hoef barbar
+
+<span>
+  foooo</span>
+hige
+fai
+\begin{prooftree}
+\AXC{$1 + 2 + 3 + 4 + 5$}
+\RightLabel{Label 1}
+\UIC{$1 + 2 + 3$}
+\AXC{$1 + 2$}
+\RightLabel{Long Label 2}
+\UIC{$1 + 2 + 3$}
+\RightLabel{Label 3}
+\BIC{$1 + 2$}
+\AXC{$1 + 2$}
+\RightLabel{Long Long Long Long Long Long Long
+Long Long Long Long Long Label 4}
+\UIC{$1 + 2 + 3 + 4 + 5$}
+\RightLabel{Label 5}
+\BIC{$1 + 2 + 3$}
+\RightLabel{Label 6}
+\UIC{$1 + 2 + 3 + 4 + 5 + 6 + 7 + 8 + 9 + 10
++ 11 + 12 + 13 + 14 + 15 + 16 + 17 + 18 + 19 + 20
++ 21 + 22 + 23
+$}
+\end{prooftree}
+hoef barbar
+
+\begin{prooftree}
+\AXC{}
+\RightLabel{Ty-Var}
+\UIC{$\Gamma'\{z[X]: nat(X)\}, P \vdash z[X] : nat(X)$}
+\RightLabel{Ty-Alpha}
+\UIC{$\Gamma', P \vdash z[W_1] : nat(W_1)$}
+\AXC{}
+\RightLabel{Ty-Prod}
+\UIC{$\Gamma', P \vdash \Nil(X,Z), Y \bowtie Z : dbllist(X,Y,Z)$}
+\RightLabel{Ty-Alpha}
+\UIC{$\Gamma', P \vdash \Nil(Z,W_2), Y \bowtie W_2 : dbllist(Z,Y,W_2)$}
+\RightLabel{Ty-Prod}
+\BIC{$\Gamma', P \vdash
+ \nu W_1 W_2.(\Cons(W_1,X,W_2,Z),z[W_1],\Nil(Z,W_2),Y \bowtie W_2): dbllist(X,Y,Z)$}
+\RightLabel{Ty-Cong}
+\UIC{$\Gamma', P \vdash
+ \nu W_3.(\Cons(W_3,X,Y,Z),z[W_3],\Nil(Z,Y)): dbllist(X,Y,Z)$}
+\RightLabel{Ty-Alpha}
+\UIC{$\Gamma', P \vdash
+ \nu W_3.(\Cons(W_3,W_2,Y,W_1),z[W_3],\Nil(W_1,Y)): dbllist(W_2,Y,W_1)$}
+\RightLabel{Ty-Var$^\ast$}
+\UIC{$\begin{array}{lll}
+ \Gamma'\{y[W_1, W_2, X, Z]: dbllist(W_2,Y,W_1) \multimap dbllist(X,Y,Z)\}, P \vdash \\
+ \quad \nu W_1 W_2 (y[W_1,W_2,X,Z],\nu W_3.(\Cons(W_3,W_2,Y,W_1),z[W_3],\Nil(W_1,Y))) \\
+ \quad : dbllist(X,Y,Z)
+ \end{array}$}
+\RightLabel{Ty-Cong}
+\UIC{$\Gamma', P \vdash
+ T: dbllist(X,Y,Z)$}
+\end{prooftree}
+
+<script type="text/javascript" class="next-head">
+  import { renderProofTrees } from "https://sano-jin.github.io/busproofs-html/assets/prooftree.js";
+  renderProofTrees();
+</script>

proof-tree/src/lib/prooftree/index.ts

@@ -16,7 +16,7 @@ export const renderProofTrees = () => {
     <HTMLCollectionOf<HTMLElement>>document.body.getElementsByTagName("P")
   );
   const nodes = nodeArray.filter((node) =>
-    node.innerText.includes("\\begin{prooftree}")
+    node.innerHTML.includes("\\begin{prooftree}")
   );
   console.log("nodes", nodes);
   console.log(nodes.map((node) => getPrtrFragment(node)));