From 8769a3e2bf99d75f6f0f17c74964d0f84bd219f2 Mon Sep 17 00:00:00 2001 From: sano Date: Sun, 14 Jul 2024 15:06:22 +0900 Subject: [PATCH] updated --- README.md | 15 ++- docs/assets/prooftree.js | 151 ++++++++++++-------------- docs/index.md | 15 ++- proof-tree/src/lib/prooftree/index.ts | 41 ++++--- 4 files changed, 111 insertions(+), 111 deletions(-) diff --git a/README.md b/README.md index 56d6b98..abddf17 100644 --- a/README.md +++ b/README.md @@ -104,10 +104,17 @@ to `renderProofTreesOnLoad` and `renderProofTrees`. ```ts interface configP { - marginPremises?: number; // the margin between premises in px (default is 20). - paddingAxiomConclusion?: number; // the left and right padding of an axiom and conclusion in px (default is 20). - marginLabelLeft?: number; // the left margin of a label in px (default is 10). - styleOnLoad?: null | number; // when to apply styles; after load (on null) or manually set timeout in milliseconds (on number) (default is null). + // the margin between premises (default is 20). + marginPremises?: number; + + // the left and right padding of an axiom and conclusion (default is 20). + paddingAxiomConclusion?: number; + + // the left margin of a label (default is 10). + marginLabelLeft?: number; + + // when to apply styles; after load (on null) or manually set timeout (on number) (default is null). + styleOnLoad?: null | number; } ``` diff --git a/docs/assets/prooftree.js b/docs/assets/prooftree.js index 73f6f86..8c49923 100644 --- a/docs/assets/prooftree.js +++ b/docs/assets/prooftree.js @@ -1,33 +1,22 @@ console.log("ProofTree v0.0.1"); -const p = "bussproofs-html__", x = { - marginPremises: 20, - paddingAxiomConclusion: 20, - marginLabelLeft: 10, - styleOnLoad: null -}, T = (t, e) => t === void 0 ? e : t, v = (t) => ({ - marginPremises: T(t.marginPremises, x.marginPremises), - paddingAxiomConclusion: T( - t.paddingAxiomConclusion, - x.paddingAxiomConclusion - ), - marginLabelLeft: T( - t.marginLabelLeft, - x.marginLabelLeft - ), - styleOnLoad: T(t.styleOnLoad, x.styleOnLoad) -}), B = (t) => `div.${p}proof-tree{width:max-content;margin:20px auto}div.${p}sequent{width:auto;text-align:center}div.${p}premises{width:auto;display:flex;flex-direction:row;gap:${t.marginPremises}px;align-items:flex-end}div.${p}horizontal-rule{width:100%;border-bottom:1.3px solid;position:relative}div.${p}horizontal-rule>.${p}right-label{position:absolute;height:auto;top:-50%;right:0;-webkit-transform:translateY(-50%);transform:translateY(-50%)}`, _ = (t = x) => { +const p = "bussproofs-html__", T = (t, e) => t === void 0 ? e : t, P = (t) => ({ + marginPremises: T(t.marginPremises, 20), + paddingAxiomConclusion: T(t.paddingAxiomConclusion, 20), + marginLabelLeft: T(t.marginLabelLeft, 10), + styleOnLoad: T(t.styleOnLoad, null) +}), V = P({}), B = (t) => `div.${p}proof-tree{width:max-content;margin:20px auto}div.${p}sequent{width:auto;text-align:center}div.${p}premises{width:auto;display:flex;flex-direction:row;gap:${t.marginPremises}px;align-items:flex-end}div.${p}horizontal-rule{width:100%;border-bottom:1.3px solid;position:relative}div.${p}horizontal-rule>.${p}right-label{position:absolute;height:auto;top:-50%;right:0;-webkit-transform:translateY(-50%);transform:translateY(-50%)}`, _ = (t = V) => { console.log(`renderProofTreesOnLoad(${JSON.stringify(t)})`), document.addEventListener("DOMContentLoaded", () => { I(t); }); -}, I = (t = x) => { +}, I = (t = V) => { console.log(`renderProofTrees(${JSON.stringify(t)})`); - const e = v(t), n = document.createElement("style"); + const e = P(t), n = document.createElement("style"); n.innerHTML = B(e), document.head.appendChild(n), Array.from( document.body.getElementsByTagName("P") ).filter( (o) => o.innerHTML.includes("\\begin{prooftree}") - ).forEach((o) => V(o, e)); -}, V = (t, e) => { + ).forEach((o) => E(o, e)); +}, E = (t, e) => { try { const n = z(t); if (!n) throw new Error("cannot find fragment"); @@ -40,17 +29,17 @@ const p = "bussproofs-html__", x = { return (i = u.parentNode) == null ? void 0 : i.removeChild(u); }); const o = R(s); - t.insertBefore(n == null ? void 0 : n.beforeTextNode, n == null ? void 0 : n.nodeList[0]), t.insertBefore(o, n == null ? void 0 : n.nodeList[0]), t.insertBefore(n == null ? void 0 : n.afterTextNode, n == null ? void 0 : n.nodeList[0]), t.removeChild(n == null ? void 0 : n.nodeList[0]), e.styleOnLoad === null ? window.addEventListener("load", () => P(e, o), !1) : setTimeout(() => P(e, o), e.styleOnLoad), t.innerHTML.includes("\\begin{prooftree}") && V(t, e); + t.insertBefore(n == null ? void 0 : n.beforeTextNode, n == null ? void 0 : n.nodeList[0]), t.insertBefore(o, n == null ? void 0 : n.nodeList[0]), t.insertBefore(n == null ? void 0 : n.afterTextNode, n == null ? void 0 : n.nodeList[0]), t.removeChild(n == null ? void 0 : n.nodeList[0]), e.styleOnLoad === null ? window.addEventListener("load", () => N(e, o), !1) : setTimeout(() => N(e, o), e.styleOnLoad), t.innerHTML.includes("\\begin{prooftree}") && E(t, e); } catch (n) { console.error(n); } -}, N = (t, e) => { +}, C = (t, e) => { let n = -1, r = -1; - for (let a = 0; a < e.length; a++) - if (e[a].nodeType === Node.TEXT_NODE) { - const l = e[a].nodeValue.indexOf(t); + for (let c = 0; c < e.length; c++) + if (e[c].nodeType === Node.TEXT_NODE) { + const l = e[c].nodeValue.indexOf(t); if (l !== -1) { - r = a, n = l; + r = c, n = l; break; } } @@ -58,39 +47,39 @@ const p = "bussproofs-html__", x = { const s = e[r].nodeValue, o = s.slice(0, n), u = s.slice(n + t.length), i = document.createTextNode(o), f = document.createTextNode(u); return [r, i, f]; }, z = (t) => { - const e = Array.from(t.childNodes), n = N("\\begin{prooftree}", e); + const e = Array.from(t.childNodes), n = C("\\begin{prooftree}", e); if (n === null) return null; const [r, s, o] = n, u = e.slice(r), i = [...u]; i.splice(0, 1, o); - const f = N("\\end{prooftree}", i); + const f = C("\\end{prooftree}", i); if (f === null) return null; - const [a, l, m] = f, d = u.slice(0, a + 1), h = i; + const [c, l, m] = f, d = u.slice(0, c + 1), h = i; h.splice( - a, - i.length - a, + c, + i.length - c, l ); - const L = h.filter( - (g) => g.nodeType !== Node.COMMENT_NODE + const x = h.filter( + (y) => y.nodeType !== Node.COMMENT_NODE ); return { nodeList: d, - prtrNodeList: L, + prtrNodeList: x, beforeTextNode: s, afterTextNode: m }; }, S = (t) => { t[0].nodeValue = t[0].nodeValue.trimStart(); -}, E = (t) => { +}, A = (t) => { const e = t[0].nodeValue.indexOf(` `); if (e !== -1) return t[0].nodeValue = t[0].nodeValue.substring(e + 1), !0; for (t.shift(); t.length > 0; ) if (t[0].nodeType !== Node.TEXT_NODE) t.shift(); - else return E(t); + else return A(t); return !1; -}, c = (t, e) => { +}, a = (t, e) => { const n = t[0].nodeValue, r = n.indexOf("}"); if (r !== -1) { const s = document.createTextNode(n.slice(0, r)); @@ -98,7 +87,7 @@ const p = "bussproofs-html__", x = { } else { for (e.push(t.shift()); t.length > 0; ) if (t[0].nodeType !== Node.TEXT_NODE) e.push(t.shift()); - else return c(t, e); + else return a(t, e); return null; } }, H = (t) => { @@ -108,55 +97,55 @@ const p = "bussproofs-html__", x = { if (e[0].nodeType !== Node.TEXT_NODE) return null; const s = e[0].nodeValue; if (s.startsWith("%")) { - if (e[0].nodeValue = s.substring(1), !E(e)) return null; + if (e[0].nodeValue = s.substring(1), !A(e)) return null; } else if (s.startsWith("\\AXC{")) { e[0].nodeValue = s.substring(5); - const o = c(e, []); + const o = a(e, []); if (o === null) return null; n.push({ type: "AXC", body: o }); } else if (s.startsWith("\\UIC{")) { e[0].nodeValue = s.substring(5); - const o = c(e, []); + const o = a(e, []); if (o === null) return null; n.push({ type: "UIC", body: o }); } else if (s.startsWith("\\BIC{")) { e[0].nodeValue = s.substring(5); - const o = c(e, []); + const o = a(e, []); if (o === null) return null; n.push({ type: "BIC", body: o }); } else if (s.startsWith("\\TIC{")) { e[0].nodeValue = s.substring(5); - const o = c(e, []); + const o = a(e, []); if (o === null) return null; n.push({ type: "TIC", body: o }); } else if (s.startsWith("\\QuaternaryInfC{")) { e[0].nodeValue = s.substring(16); - const o = c(e, []); + const o = a(e, []); if (o === null) return null; n.push({ type: "QuaternaryInfC", body: o }); } else if (s.startsWith("\\RightLabel{")) { e[0].nodeValue = s.substring(12); - const o = c(e, []); + const o = a(e, []); if (o === null) return null; n.push({ type: "RightLabel", body: o }); } else if (s.startsWith("\\normalsize{")) { - if (e[0].nodeValue = s.substring(12), c(e, []) === null) return null; + if (e[0].nodeValue = s.substring(12), a(e, []) === null) return null; } else if (s.startsWith("\\normalsize")) e[0].nodeValue = s.substring(11); else if (s.startsWith("\\small{")) { - if (e[0].nodeValue = s.substring(7), c(e, []) === null) return null; + if (e[0].nodeValue = s.substring(7), a(e, []) === null) return null; } else if (s.startsWith("\\small")) e[0].nodeValue = s.substring(6); else if (s.startsWith("\\footnotesize{")) { - if (e[0].nodeValue = s.substring(14), c(e, []) === null) return null; + if (e[0].nodeValue = s.substring(14), a(e, []) === null) return null; } else if (s.startsWith("\\footnotesize")) e[0].nodeValue = s.substring(13); else if (s.startsWith("\\scriptsize{")) { - if (e[0].nodeValue = s.substring(12), c(e, []) === null) return null; + if (e[0].nodeValue = s.substring(12), a(e, []) === null) return null; } else if (s.startsWith("\\scriptsize")) e[0].nodeValue = s.substring(11); else if (s.startsWith("\\tiny{")) { - if (e[0].nodeValue = s.substring(6), c(e, []) === null) return null; + if (e[0].nodeValue = s.substring(6), a(e, []) === null) return null; } else if (s.startsWith("\\tiny")) e[0].nodeValue = s.substring(5); else if (e[0].nodeValue.length === 0) @@ -165,14 +154,14 @@ const p = "bussproofs-html__", x = { return console.error("error: unrecognised charactor", e[0].nodeValue), null; } return n; -}, w = (t, e, n) => { +}, L = (t, e, n) => { const r = t[0]; if (!r) return null; let s = []; r.type === "RightLabel" && (t.shift(), s = r.body); const o = []; for (let u = 0; u < n; u++) { - const i = A(t); + const i = W(t); if (!i) return null; o.push(i); } @@ -182,40 +171,40 @@ const p = "bussproofs-html__", x = { rightLabel: s, conclusion: e }; -}, A = (t) => { +}, W = (t) => { const e = t.shift(); if (!e) return null; switch (e.type) { case "AXC": return { type: "Axiom", axiom: e.body }; case "UIC": - return w(t, e.body, 1); + return L(t, e.body, 1); case "BIC": - return w(t, e.body, 2); + return L(t, e.body, 2); case "TIC": - return w(t, e.body, 3); + return L(t, e.body, 3); case "QuaternaryInfC": - return w(t, e.body, 4); + return L(t, e.body, 4); } return null; }, M = (t) => { - const e = A(t.reverse()); + const e = W(t.reverse()); return t.length > 0 ? null : e; -}, y = (t, e) => { +}, g = (t, e) => { const n = document.createElement("div"); return n.classList.add(p + t), (t === "axiom" || t === "right-label" || t === "conclusion") && (n.style.width = "max-content"), e.forEach((r) => n.appendChild(r)), n; -}, W = (t) => { +}, O = (t) => { switch (t.type) { case "Axiom": - return y("axiom", t.axiom); + return g("axiom", t.axiom); case "Sequent": - return y("sequent", [ - y("premises", t.premises.map(W)), - y("horizontal-rule", [y("right-label", t.rightLabel)]), - y("conclusion", t.conclusion) + return g("sequent", [ + g("premises", t.premises.map(O)), + g("horizontal-rule", [g("right-label", t.rightLabel)]), + g("conclusion", t.conclusion) ]); } -}, R = (t) => y("proof-tree", [W(t)]), q = (t) => t.reduce((e, n) => e + n, 0), O = (t) => { +}, R = (t) => g("proof-tree", [O(t)]), q = (t) => t.reduce((e, n) => e + n, 0), $ = (t) => { switch (t.type) { case "PSAxiom": { t.node.style.width = `${t.prtrStyleAux.w}px`; @@ -223,11 +212,11 @@ const p = "bussproofs-html__", x = { } case "PSSequent": { const e = t.prtrStyleAux; - t.node.style.width = `${e.w}px`, t.nodePremises.style.marginLeft = `${e.mlp}px`, t.nodeHR.style.width = `${e.whr}px`, t.nodeHR.style.marginLeft = `${e.mlhr}px`, t.nodeHR.style.marginRight = `${e.mrhr}px`, t.nodeLabel.style.right = `-${e.widthL}px`, t.nodeConclusion.style.width = `${e.widthC}px`, t.nodeConclusion.style.marginLeft = `${e.mlc}px`, t.premises.forEach(O); + t.node.style.width = `${e.w}px`, t.nodePremises.style.marginLeft = `${e.mlp}px`, t.nodeHR.style.width = `${e.whr}px`, t.nodeHR.style.marginLeft = `${e.mlhr}px`, t.nodeHR.style.marginRight = `${e.mrhr}px`, t.nodeLabel.style.right = `-${e.widthL}px`, t.nodeConclusion.style.width = `${e.widthC}px`, t.nodeConclusion.style.marginLeft = `${e.mlc}px`, t.premises.forEach($); return; } } -}, $ = (t) => (e) => { +}, v = (t) => (e) => { if (e.classList.contains(p + "axiom")) { const n = e.offsetWidth + 1 + t.paddingAxiomConclusion * 2; return { @@ -246,25 +235,25 @@ const p = "bussproofs-html__", x = { node: e }; } else if (e.classList.contains(p + "sequent")) { - const n = e.children[0], r = e.children[1], s = r.children[0], o = e.children[2], u = Array.prototype.slice.apply(n.children), i = o.children[0] ? o.children[0].offsetWidth + 1 + t.paddingAxiomConclusion * 2 : o.offsetWidth + 1 + t.paddingAxiomConclusion * 2, f = s.offsetWidth + t.marginLabelLeft, a = u.map($(t)), l = a.map((d) => d.prtrStyleAux); + const n = e.children[0], r = e.children[1], s = r.children[0], o = e.children[2], u = Array.prototype.slice.apply(n.children), i = o.children[0] ? o.children[0].offsetWidth + 1 + t.paddingAxiomConclusion * 2 : o.offsetWidth + 1 + t.paddingAxiomConclusion * 2, f = s.offsetWidth + t.marginLabelLeft, c = u.map(v(t)), l = c.map((d) => d.prtrStyleAux); u.length === 0 && console.error("error: empty premises", u); const m = q(l.map((d) => d.w)) + t.marginPremises * (l.length - 1) - l[0].mlc - l[l.length - 1].mrc; if (m > i) { - const d = m, h = l[0].mlc, L = h + (m - i) / 2, b = Math.max(l[l.length - 1].mrc, f), g = b + (m - i) / 2; + const d = m, h = l[0].mlc, x = h + (m - i) / 2, b = Math.max(l[l.length - 1].mrc, f), y = b + (m - i) / 2; return { type: "PSSequent", prtrStyleAux: { w: d + h + b, whr: d, - mlc: L, - mrc: g, + mlc: x, + mrc: y, mlhr: h, mrhr: b, widthC: i, widthL: f, mlp: 0 }, - premises: a, + premises: c, node: e, nodePremises: n, nodeHR: r, @@ -272,14 +261,14 @@ const p = "bussproofs-html__", x = { nodeConclusion: o }; } else { - const d = i, h = Math.max(l[0].mlc - (i - m) / 2, 0), L = Math.max((i - m) / 2 - l[0].mlc, 0), b = h, g = Math.max( + const d = i, h = Math.max(l[0].mlc - (i - m) / 2, 0), x = Math.max((i - m) / 2 - l[0].mlc, 0), b = h, y = Math.max( l[l.length - 1].mrc - (i - m) / 2, f - ), C = g; + ), w = y; return { type: "PSSequent", - prtrStyleAux: { w: d + h + g, whr: d, mlc: b, mrc: C, mlhr: h, mrhr: g, widthC: i, widthL: f, mlp: L }, - premises: a, + prtrStyleAux: { w: d + h + y, whr: d, mlc: b, mrc: w, mlhr: h, mrhr: y, widthC: i, widthL: f, mlp: x }, + premises: c, node: e, nodePremises: n, nodeHR: r, @@ -289,9 +278,9 @@ const p = "bussproofs-html__", x = { } } else throw new Error("error"); -}, P = (t, e) => { - const n = $(t)(e.children[0]); - O(n); +}, N = (t, e) => { + const n = v(t)(e.children[0]); + $(n); }; export { I as renderProofTrees, diff --git a/docs/index.md b/docs/index.md index c5ca097..2f68413 100644 --- a/docs/index.md +++ b/docs/index.md @@ -104,10 +104,17 @@ to `renderProofTreesOnLoad` and `renderProofTrees`. ```ts interface configP { - marginPremises?: number; // the margin between premises in px (default is 20). - paddingAxiomConclusion?: number; // the left and right padding of an axiom and conclusion in px (default is 20). - marginLabelLeft?: number; // the left margin of a label in px (default is 10). - styleOnLoad?: null | number; // when to apply styles; after load (on null) or manually set timeout in milliseconds (on number) (default is null). + // the margin between premises (default is 20). + marginPremises?: number; + + // the left and right padding of an axiom and conclusion (default is 20). + paddingAxiomConclusion?: number; + + // the left margin of a label (default is 10). + marginLabelLeft?: number; + + // when to apply styles; after load (on null) or manually set timeout (on number) (default is null). + styleOnLoad?: null | number; } ``` diff --git a/proof-tree/src/lib/prooftree/index.ts b/proof-tree/src/lib/prooftree/index.ts index 818f340..2c9e5fc 100644 --- a/proof-tree/src/lib/prooftree/index.ts +++ b/proof-tree/src/lib/prooftree/index.ts @@ -5,10 +5,17 @@ console.log("ProofTree v0.0.1"); const BH = "bussproofs-html__"; interface configP { - marginPremises?: number; // the margin between premises (default is 20). - paddingAxiomConclusion?: number; // the left and right padding of an axiom and conclusion (default is 20). - marginLabelLeft?: number; // the left margin of a label (default is 10). - styleOnLoad?: null | number; // when to apply styles; after load (on null) or manually set timeout (on number) (default is null). + // the margin between premises (default is 20). + marginPremises?: number; + + // the left and right padding of an axiom and conclusion (default is 20). + paddingAxiomConclusion?: number; + + // the left margin of a label (default is 10). + marginLabelLeft?: number; + + // when to apply styles; after load (on null) or manually set timeout (on number) (default is null). + styleOnLoad?: null | number; } interface config { @@ -18,28 +25,18 @@ interface config { styleOnLoad: null | number; } -const defaultConfig: config = { - marginPremises: 20, - paddingAxiomConclusion: 20, - marginLabelLeft: 10, - styleOnLoad: null, -}; - const maybe = (x: undefined | T, def: T): T => (x === undefined ? def : x); -const initConfig = (configP: configP) => ({ - marginPremises: maybe(configP.marginPremises, defaultConfig.marginPremises), - paddingAxiomConclusion: maybe( - configP.paddingAxiomConclusion, - defaultConfig.paddingAxiomConclusion - ), - marginLabelLeft: maybe( - configP.marginLabelLeft, - defaultConfig.marginLabelLeft - ), - styleOnLoad: maybe(configP.styleOnLoad, defaultConfig.styleOnLoad), +// Initialize configuration options with default parameters. +const initConfig = (cfg: configP) => ({ + marginPremises: maybe(cfg.marginPremises, 20), + paddingAxiomConclusion: maybe(cfg.paddingAxiomConclusion, 20), + marginLabelLeft: maybe(cfg.marginLabelLeft, 10), + styleOnLoad: maybe(cfg.styleOnLoad, null), }); +const defaultConfig = initConfig({}); + const style = (cfg: config) => `div.${BH}proof-tree{width:max-content;margin:20px auto}div.${BH}sequent{width:auto;text-align:center}div.${BH}premises{width:auto;display:flex;flex-direction:row;gap:${cfg.marginPremises}px;align-items:flex-end}div.${BH}horizontal-rule{width:100%;border-bottom:1.3px solid;position:relative}div.${BH}horizontal-rule>.${BH}right-label{position:absolute;height:auto;top:-50%;right:0;-webkit-transform:translateY(-50%);transform:translateY(-50%)}`;