diff --git a/README.md b/README.md index 7f08004..ab0d994 100644 --- a/README.md +++ b/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 を適用して，数式部分をレンダリングする． diff --git a/docs/assets/prooftree.css b/docs/assets/prooftree.css deleted file mode 100644 index e91f37e..0000000 --- a/docs/assets/prooftree.css +++ /dev/null @@ -1 +0,0 @@ -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:2px solid blue;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%)} diff --git a/docs/assets/prooftree.js b/docs/assets/prooftree.js index 06bab91..1143e43 100644 --- a/docs/assets/prooftree.js +++ b/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 }; diff --git a/docs/test.md b/docs/test.md new file mode 100644 index 0000000..d54c4a3 --- /dev/null +++ b/docs/test.md @@ -0,0 +1,127 @@ +--- +marp: true +footer: Powered by Aqua / Marp +paginate: true +headingDivider: 1 +theme: aqua +math: katex +--- + + + +# 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 + +foooo +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 + + + foooo +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} + + diff --git a/proof-tree/src/lib/prooftree/index.ts b/proof-tree/src/lib/prooftree/index.ts index 6021e68..f3092c9 100644 --- a/proof-tree/src/lib/prooftree/index.ts +++ b/proof-tree/src/lib/prooftree/index.ts @@ -16,7 +16,7 @@ export const renderProofTrees = () => { >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)));