Formatting improvements for metamath.org proof pages
// ==UserScript==
// @name MM Site Format
// @namespace https://github.com/marnix/mm-site-format-userscript
// @version 0.28.0
// @description Formatting improvements for metamath.org proof pages
// @author Marnix Klooster
// @license Unlicense; https://unlicense.org/
// @match *://us.metamath.org/*
// @match *://metamath.org/*
// @grant none
// ==/UserScript==
"use strict";
(() => {
// src/config.ts
var import_meta = {};
var HIGHLIGHT_COLOR = "#ffe066";
var HIGHLIGHT_MATCH_COLOR = "#fff3bf";
var DIFF_COLOR = "#ffd0d0";
var CALC_WIDTH_FACTOR = 1.1;
var DEV_BYPASS_CACHE = false;
var DEV_PERF_LOG = false;
var DEV_CHECK_SHARED_COVERAGE = (
// Always enabled in test runs (vitest sets import.meta.env.MODE to "test").
// eslint-disable-next-line @typescript-eslint/no-unnecessary-condition
import_meta.env?.MODE === "test"
);
// src/database-assumptions.ts
var TOP_TYPE = "$TOP";
var GIF_TOP_RULE = {
assumptions: [["wff", "chi"]],
conclusion: [TOP_TYPE, "|-", "chi"]
};
var UNI_TOP_RULE = {
assumptions: [["wff", "chi"]],
conclusion: [TOP_TYPE, "\u22A2", "chi"]
};
var PRIMITIVE_SYNTAX_PAGES = [
"cv",
"wcel",
"wceq",
"weq",
"wel",
"wnf"
];
var KIND_ALIASES = { set: "setvar" };
var SYMVAR_CSS_CLASS = "symvar";
var SYMVAR_KIND = "class";
// src/cache.ts
function createCache(store, version) {
if (DEV_BYPASS_CACHE) {
return { get: (_key, compute) => compute() };
}
const memo = /* @__PURE__ */ new Map();
const fullKey = (key) => `mmsf:${version}:${key}`;
return {
get(key, compute) {
const k = fullKey(key);
const memoised = memo.get(k);
if (memoised) return memoised;
let stored = null;
try {
stored = store?.getItem(k) ?? null;
} catch {
stored = null;
}
if (stored !== null) {
try {
const resolved = Promise.resolve(JSON.parse(stored));
memo.set(k, resolved);
return resolved;
} catch {
}
}
const result = compute().then((value) => {
try {
store?.setItem(k, JSON.stringify(value));
} catch {
}
return value;
});
memo.set(k, result);
return result;
}
};
}
// src/calculation.ts
function findSharedNodes(root) {
const seen = /* @__PURE__ */ new Set();
const shared = /* @__PURE__ */ new Set();
function walk(node) {
if (seen.has(node)) {
shared.add(node);
return;
}
seen.add(node);
for (const child of node.subproofs) walk(child);
}
walk(root);
return shared;
}
function proofTreeToCalculation(tree, spineFor = () => 0, smallFor = () => false, tokensFor = () => null, anchor = null, shared = /* @__PURE__ */ new Set(), spineShared = /* @__PURE__ */ new Set(), isChild = false) {
if (tree.subproofs.length === 0 || shared.has(tree))
return {
kind: "given",
hypothesisRefHtml: tree.refHtml,
get expressionHtml() {
return tree.expressionHtml;
}
};
if (isChild && tree.subproofs.every((s) => s.subproofs.length === 0))
return {
kind: "given",
hypothesisRefHtml: tree.refHtml,
get expressionHtml() {
return tree.expressionHtml;
},
leafRefHtmls: tree.subproofs.map((s) => s.refHtml),
leafExpressionHtmls: tree.subproofs.map((s) => s.expressionHtml)
};
const spineIndex = spineFor(tree, anchor);
const nextAnchor = tokensFor(tree);
const step = {
kind: "step",
inferenceRuleRefHtml: tree.refHtml,
get expressionHtml() {
return tree.expressionHtml;
},
subcalculations: tree.subproofs.map((s, i) => {
const effectiveShared = i === spineIndex ? shared : /* @__PURE__ */ new Set([...shared, ...spineShared]);
return proofTreeToCalculation(
s,
spineFor,
smallFor,
tokensFor,
i === spineIndex ? nextAnchor : null,
effectiveShared,
spineShared,
i !== spineIndex
// only off-spine children can fold to givens
);
}),
spine: spineIndex
};
const foldedRefs = [];
let foldNode = spineIndex !== null ? tree.subproofs[spineIndex] : null;
while (foldNode && smallFor(foldNode)) {
foldedRefs.push(foldNode.refHtml);
if (foldNode.subproofs.length !== 1) break;
foldNode = foldNode.subproofs[0];
}
if (foldedRefs.length > 0) {
step.foldedRuleRefs = foldedRefs;
if (spineIndex !== null && foldNode) {
const effectiveShared = /* @__PURE__ */ new Set([...shared]);
step.subcalculations[spineIndex] = proofTreeToCalculation(
foldNode,
spineFor,
smallFor,
tokensFor,
nextAnchor,
effectiveShared,
spineShared,
false
// spine continuation: must not fold to given
);
}
}
return step;
}
function collectCalcRefs(calc) {
const refs = /* @__PURE__ */ new Set();
const walk = (c) => {
if (c.kind === "given") {
refs.add(c.hypothesisRefHtml);
for (const leaf of c.leafRefHtmls ?? []) refs.add(leaf);
} else {
refs.add(c.inferenceRuleRefHtml);
for (const folded of c.foldedRuleRefs ?? []) refs.add(folded);
for (const sub of c.subcalculations) walk(sub);
}
};
walk(calc);
return refs;
}
function missingCalcRefs(tree, stepOf, mainCalc, shared) {
const mainRefs = collectCalcRefs(mainCalc);
const missing = [];
const visited = /* @__PURE__ */ new Set();
const walk = (node) => {
if (visited.has(node)) return;
visited.add(node);
if (shared.has(node)) {
return;
}
if (!mainRefs.has(node.refHtml)) {
const n = stepOf.get(node);
if (n !== void 0) missing.push(n);
}
for (const sub of node.subproofs) walk(sub);
};
walk(tree);
return missing;
}
function checkSpineValidity(calc) {
const walk = (c, depth) => {
if (depth > 1e4) return "spine depth exceeds 10000 (likely cycle)";
if (c.kind === "given") return null;
if (c.spine === null) return null;
if (c.spine < 0 || c.spine >= c.subcalculations.length)
return `spine index ${c.spine} out of bounds (${c.subcalculations.length} subcalculations)`;
for (let i = 0; i < c.subcalculations.length; i++) {
if (i === c.spine) continue;
const sub = c.subcalculations[i];
if (sub.kind === "step") {
const err = walk(sub, 0);
if (err) return `in subcalc ${i}: ${err}`;
}
}
return walk(c.subcalculations[c.spine], depth + 1);
};
return walk(calc, 0);
}
function collectCalcExpressions(calc) {
const exprs = /* @__PURE__ */ new Set();
const walk = (c) => {
exprs.add(c.expressionHtml);
if (c.kind === "step") {
for (const sub of c.subcalculations) walk(sub);
}
};
walk(calc);
return exprs;
}
function missingCalcExpressions(tree, stepOf, mainCalc, shared) {
const exprs = collectCalcExpressions(mainCalc);
const foldedRefs = /* @__PURE__ */ new Set();
const collectFolded = (c) => {
if (c.kind === "step") {
for (const ref of c.foldedRuleRefs ?? []) foldedRefs.add(ref);
for (const sub of c.subcalculations) collectFolded(sub);
}
};
collectFolded(mainCalc);
const missing = [];
const visited = /* @__PURE__ */ new Set();
const walk = (node, parentIsDepth1) => {
if (visited.has(node)) return;
visited.add(node);
if (shared.has(node)) return;
if (parentIsDepth1 && node.subproofs.length === 0) return;
if (foldedRefs.has(node.refHtml)) return;
if (!exprs.has(node.expressionHtml)) {
const n = stepOf.get(node);
if (n !== void 0) missing.push(n);
}
const isDepth1 = node.subproofs.length > 0 && node.subproofs.every((s) => s.subproofs.length === 0);
for (const sub of node.subproofs) walk(sub, isDepth1);
};
walk(tree, false);
return missing;
}
function checkSharedSubtreeCoverage(shared, stepOf, spineFor, smallFor) {
const missing = [];
for (const node of shared) {
if (node.subproofs.length === 0) continue;
const others = new Set(shared);
others.delete(node);
const miniCalc = proofTreeToCalculation(
node,
spineFor,
smallFor,
() => null,
null,
others,
/* @__PURE__ */ new Set(),
false
);
const refs = collectCalcRefs(miniCalc);
const exprs = collectCalcExpressions(miniCalc);
const foldedRefs = /* @__PURE__ */ new Set();
const collectFolded = (c) => {
if (c.kind === "step") {
for (const ref of c.foldedRuleRefs ?? []) foldedRefs.add(ref);
for (const sub of c.subcalculations) collectFolded(sub);
}
};
collectFolded(miniCalc);
const visited = /* @__PURE__ */ new Set();
const walk = (n, parentIsDepth1) => {
if (visited.has(n)) return;
visited.add(n);
if (others.has(n)) return;
if (foldedRefs.has(n.refHtml)) {
for (const sub of n.subproofs) walk(sub, false);
return;
}
if (!refs.has(n.refHtml)) {
const s = stepOf.get(n);
if (s !== void 0) missing.push(s);
} else if (!exprs.has(n.expressionHtml) && !(parentIsDepth1 && n.subproofs.length === 0)) {
const s = stepOf.get(n);
if (s !== void 0) missing.push(s);
}
const isDepth1 = n.subproofs.length > 0 && n.subproofs.every((sub) => sub.subproofs.length === 0);
for (const sub of n.subproofs) walk(sub, isDepth1);
};
walk(node, false);
}
return missing;
}
function checkRuleRefIntegrity(tree, stepOf, mainCalc, shared) {
const allTreeRefs = /* @__PURE__ */ new Set();
const visited = /* @__PURE__ */ new Set();
const collectTreeRefs = (node) => {
if (visited.has(node)) return;
visited.add(node);
allTreeRefs.add(node.refHtml);
for (const sub of node.subproofs) collectTreeRefs(sub);
};
collectTreeRefs(tree);
const isSynthetic = (el) => !!el.querySelector('a[href^="#mm-site-format-proof-"]');
const bad = [];
const walkCalc = (c) => {
if (c.kind === "given") {
if (!allTreeRefs.has(c.hypothesisRefHtml) && !isSynthetic(c.hypothesisRefHtml)) {
for (const [node, n] of stepOf) {
if (node.expressionHtml === c.expressionHtml) {
bad.push(n);
break;
}
}
}
} else {
if (!allTreeRefs.has(c.inferenceRuleRefHtml) && !isSynthetic(c.inferenceRuleRefHtml)) {
for (const [node, n] of stepOf) {
if (node.expressionHtml === c.expressionHtml) {
bad.push(n);
break;
}
}
}
for (const sub of c.subcalculations) walkCalc(sub);
}
};
walkCalc(mainCalc);
return bad;
}
function checkNoDuplicateAppearance(mainCalc, stepOf) {
const duplicates = [];
const walkCalc = (c) => {
if (c.kind !== "step") return;
const givenRefs = /* @__PURE__ */ new Set();
const stepRefs = /* @__PURE__ */ new Set();
for (let i = 0; i < c.subcalculations.length; i++) {
if (i === c.spine) continue;
const sub = c.subcalculations[i];
if (sub.kind === "given") givenRefs.add(sub.hypothesisRefHtml);
else stepRefs.add(sub.inferenceRuleRefHtml);
}
for (const ref of givenRefs) {
if (stepRefs.has(ref)) {
for (const [node, n] of stepOf) {
if (node.refHtml === ref) {
duplicates.push(n);
break;
}
}
}
}
for (const sub of c.subcalculations) walkCalc(sub);
};
walkCalc(mainCalc);
return duplicates;
}
function checkStepCountConservation(tree, stepOf, mainCalc, shared) {
const allNodes = /* @__PURE__ */ new Set();
const collectAll = (node) => {
if (allNodes.has(node)) return;
allNodes.add(node);
for (const sub of node.subproofs) collectAll(sub);
};
collectAll(tree);
const mainRefs = collectCalcRefs(mainCalc);
const mainExprs = collectCalcExpressions(mainCalc);
const accounted = /* @__PURE__ */ new Set();
for (const node of allNodes) {
if (shared.has(node)) {
const markShared = (n) => {
if (accounted.has(n)) return;
accounted.add(n);
for (const sub of n.subproofs) markShared(sub);
};
markShared(node);
} else if (mainRefs.has(node.refHtml) || mainExprs.has(node.expressionHtml)) {
accounted.add(node);
}
}
const orphans = [];
for (const node of allNodes) {
if (!accounted.has(node)) {
const n = stepOf.get(node);
if (n !== void 0) orphans.push(n);
}
}
return orphans;
}
// src/expression.ts
function findMathSpans(root) {
return [...root.querySelectorAll("span.math")];
}
var INLINE_FORMATTING_TAGS = /* @__PURE__ */ new Set([
"B",
"SMALL",
"I",
"EM",
"STRONG",
"TT",
"SUP",
"SUB",
"FONT"
]);
function findGifRuns(root) {
const runs = [];
function scan(parent) {
let run = [];
let images = 0;
let tokens = 0;
const flush = () => {
if (images >= 1 && tokens >= 2) runs.push(run);
run = [];
images = 0;
tokens = 0;
};
for (const node of parent.childNodes) {
if (node.nodeType === Node.ELEMENT_NODE) {
const el = node;
if (el.tagName === "IMG" && el.hasAttribute("alt")) {
run.push(el);
images++;
tokens++;
} else if (run.length > 0 && INLINE_FORMATTING_TAGS.has(el.tagName) && !el.querySelector("img[alt]")) {
for (const child of el.childNodes) {
if (child.nodeType === Node.TEXT_NODE) {
const words = (child.nodeValue ?? "").split(/\s+/).filter(Boolean);
if (words.length) {
run.push(child);
tokens += words.length;
}
}
}
} else {
flush();
scan(el);
}
} else if (node.nodeType === Node.TEXT_NODE) {
const words = (node.nodeValue ?? "").split(/\s+/).filter(Boolean);
if (words.length) {
run.push(node);
tokens += words.length;
}
}
}
flush();
}
scan(root);
return runs;
}
function gifNodeText(node) {
return node.nodeType === Node.TEXT_NODE ? node.nodeValue ?? "" : node.getAttribute("alt") ?? "";
}
function extractGifText(nodes) {
return nodes.map(gifNodeText).join(" ").split(/\s+/).filter(Boolean).join(" ");
}
// src/loader.ts
function extractSyntaxHintUrls(doc, pageUrl) {
const base = new URL(pageUrl);
const urls = /* @__PURE__ */ new Set();
for (const b of doc.querySelectorAll("b")) {
if (b.textContent?.trim() === "Syntax hints:") {
const cell = b.closest("td") ?? b.closest("tr");
for (const a of cell?.querySelectorAll("a[href]") ?? []) {
const href = a.getAttribute("href");
if (href && !href.startsWith("#")) urls.add(new URL(href, base).href);
}
}
}
return [...urls];
}
function extractRefUrls(doc, pageUrl) {
const base = new URL(pageUrl);
const urls = /* @__PURE__ */ new Set();
const proofTable = doc.querySelector('table[summary="Proof of theorem"]');
for (const tr of proofTable?.querySelectorAll("tr") ?? []) {
const tds = tr.querySelectorAll("td");
if (tds.length >= 3) {
for (const a of tds[2].querySelectorAll("a[href]")) {
const href = a.getAttribute("href");
if (href && !href.startsWith("#")) urls.add(new URL(href, base).href);
}
}
}
return [...urls];
}
function extractBreakdownRefUrls(doc, pageUrl) {
const base = new URL(pageUrl);
const urls = /* @__PURE__ */ new Set();
const table = doc.querySelector(
'table[summary="Detailed syntax breakdown of definition"]'
);
for (const tr of table?.querySelectorAll("tr") ?? []) {
const tds = tr.querySelectorAll("td");
if (tds.length >= 3) {
for (const a of tds[2].querySelectorAll("a[href]")) {
const href = a.getAttribute("href");
if (href && !href.startsWith("#")) urls.add(new URL(href, base).href);
}
}
}
return [...urls];
}
// src/kind.ts
var rgbKey = (c) => c.join(",");
var NAMED_COLORS = {
black: [0, 0, 0],
white: [255, 255, 255],
red: [255, 0, 0],
green: [0, 128, 0],
blue: [0, 0, 255],
gray: [128, 128, 128],
grey: [128, 128, 128]
};
function parseCssColor(value) {
const v = value.trim().toLowerCase();
if (v in NAMED_COLORS) return NAMED_COLORS[v];
const m = v.match(/^#([0-9a-f]{3}|[0-9a-f]{6})$/);
if (!m) return null;
const h = m[1].length === 3 ? [...m[1]].map((d) => d + d).join("") : m[1];
const at = (i) => parseInt(h.slice(i, i + 2), 16);
return [at(0), at(2), at(4)];
}
function colourOf(el) {
const style = el.getAttribute("style") ?? "";
const m = style.match(/color\s*:\s*([^;]+)/i);
if (m) return parseCssColor(m[1]);
const attr = el.getAttribute("color");
return attr ? parseCssColor(attr) : null;
}
function parseKindColors(doc) {
const colors = /* @__PURE__ */ new Map();
const label = [...doc.querySelectorAll("b")].find(
(b) => /colors of variables/i.test((b.textContent ?? "").replace(/\s+/g, " "))
);
const cell = label?.closest("td") ?? label?.parentElement;
if (!cell) return colors;
for (const el of cell.querySelectorAll("[style], [color]")) {
const name = el.textContent?.trim();
const rgb = colourOf(el);
if (name && rgb) colors.set(rgbKey(rgb), KIND_ALIASES[name] ?? name);
}
return colors;
}
function parseKindNames(doc) {
return new Set(parseKindColors(doc).values());
}
function dominantInk(data) {
const counts = /* @__PURE__ */ new Map();
for (let i = 0; i + 3 < data.length; i += 4) {
const r = data[i], g = data[i + 1], b = data[i + 2], a = data[i + 3];
if (a < 128) continue;
if (r > 230 && g > 230 && b > 230) continue;
const key = `${r},${g},${b}`;
counts.set(key, (counts.get(key) ?? 0) + 1);
}
let best = null;
let bestCount = 0;
for (const [key, n] of counts) {
if (n > bestCount) {
best = key;
bestCount = n;
}
}
return best ? best.split(",").map(Number) : null;
}
function variableKindOfImg(img, colors, sample) {
const ink = dominantInk(sample(img));
if (!ink) return null;
const exact = colors.get(rgbKey(ink));
if (exact) return exact;
for (const [key, kind] of colors) {
const [r, g, b] = key.split(",").map(Number);
if (Math.abs(ink[0] - r) <= 2 && Math.abs(ink[1] - g) <= 2 && Math.abs(ink[2] - b) <= 2)
return kind;
}
return null;
}
var canvasSampler = (img) => {
const el = img;
const w = el.naturalWidth || el.width;
const h = el.naturalHeight || el.height;
if (!w || !h) return new Uint8ClampedArray();
const canvas = document.createElement("canvas");
canvas.width = w;
canvas.height = h;
const ctx = canvas.getContext("2d");
if (!ctx) return new Uint8ClampedArray();
ctx.drawImage(el, 0, 0);
return ctx.getImageData(0, 0, w, h).data;
};
// src/token.ts
function* splitConstants(text) {
const re = /[(){}]|[^(){}\s]+/g;
let m;
while (m = re.exec(text)) {
yield { text: m[0], start: m.index, end: m.index + m[0].length };
}
}
function* munchConstants(text, vocab, maxLen) {
let i = 0;
while (i < text.length) {
if (/\s/.test(text[i])) {
i++;
continue;
}
let len = 0;
for (let l = Math.min(maxLen, text.length - i); l >= 1; l--) {
if (vocab.has(text.slice(i, i + l))) {
len = l;
break;
}
}
if (len === 0) len = 1;
yield { text: text.slice(i, i + len), start: i, end: i + len };
i += len;
}
}
function isSubscript(el) {
return el.tagName === "SUB" || el.querySelector("sub") !== null;
}
var INLINE_FORMATTING_TAGS2 = /* @__PURE__ */ new Set([
"B",
"SMALL",
"I",
"EM",
"STRONG",
"TT",
"FONT",
"SUB"
]);
function runLocation(run, start, end) {
const a = run[start];
let sub;
for (let k = start; k < end; k++) sub = run[k].sub ?? sub;
if (sub) return { type: "folded", node: a.node, offset: a.offset, sub };
const b = run[end - 1];
const endOffset = b.node === a.node ? b.offset + 1 : a.offset + 1;
return { type: "text", node: a.node, start: a.offset, end: endOffset };
}
function locateMathSpan(span, kinds, vocab, colors) {
const out = [];
const maxLen = vocab ? Math.max(1, ...[...vocab].map((c) => c.length)) : 1;
let run = [];
const flush = () => {
if (run.length === 0) return;
const text = run.map((c) => c.ch).join("");
const tokens = vocab ? munchConstants(text, vocab, maxLen) : splitConstants(text);
for (const { text: t, start, end } of tokens) {
out.push({
token: { kind: null, text: t },
location: runLocation(run, start, end)
});
}
run = [];
};
for (const node of span.childNodes) {
if (node.nodeType === Node.ELEMENT_NODE) {
const el = node;
const cls = (el.getAttribute("class") ?? "").trim();
if (kinds.has(cls)) {
flush();
const text = el.textContent?.trim() ?? "";
if (text)
out.push({
token: { kind: cls, text },
location: { type: "element", node: el }
});
} else if (cls === SYMVAR_CSS_CLASS && colors) {
const style = el.getAttribute("style") ?? "";
const m = style.match(/color\s*:\s*([^;]+)/i);
const rgb = m ? parseCssColor(m[1]) : null;
const kind = rgb ? colors.get(rgbKey(rgb)) ?? SYMVAR_KIND : SYMVAR_KIND;
flush();
const text = el.textContent?.trim() ?? "";
if (text)
out.push({
token: { kind, text },
location: { type: "element", node: el }
});
} else if (INLINE_FORMATTING_TAGS2.has(el.tagName) && run.length > 0) {
const base = run[run.length - 1];
const isSub = isSubscript(el);
const chars = el.textContent ?? "";
for (let k = 0; k < chars.length; k++)
run.push({
ch: chars[k],
node: base.node,
offset: base.offset,
...isSub && { sub: el }
});
} else if (INLINE_FORMATTING_TAGS2.has(el.tagName)) {
const chars = el.textContent ?? "";
for (let k = 0; k < chars.length; k++)
run.push({ ch: chars[k], node, offset: k });
} else {
flush();
for (const { text } of splitConstants(el.textContent ?? "")) {
out.push({
token: { kind: null, text },
location: { type: "element", node: el }
});
}
}
} else if (node.nodeType === Node.TEXT_NODE) {
const tn = node;
const value = tn.nodeValue ?? "";
for (let i = 0; i < value.length; i++) {
run.push({ ch: value[i], node: tn, offset: i });
}
}
}
flush();
return out;
}
function locateGifRun(nodes, colors, sample, cache = /* @__PURE__ */ new Map()) {
const out = [];
for (const node of nodes) {
if (node.nodeType === Node.TEXT_NODE) {
const tn = node;
for (const { text: text2, start, end } of splitConstants(tn.nodeValue ?? "")) {
out.push({
token: { kind: null, text: text2 },
location: { type: "text", node: tn, start, end }
});
}
continue;
}
const img = node;
const text = (img.getAttribute("alt") ?? "").trim();
const src = img.getAttribute("src") ?? "";
let kind = cache.get(src);
if (kind === void 0) {
kind = variableKindOfImg(img, colors, sample);
cache.set(src, kind);
}
out.push({
token: kind === null ? { kind: null, text } : { kind, text },
location: { type: "element", node: img }
});
}
return out;
}
function tokenizeMathSpan(span, kinds, vocab, colors) {
return locateMathSpan(span, kinds, vocab, colors).map((lt) => lt.token);
}
function chunkifyMathSpan(span, kinds, colors) {
const chunks = [];
const locations = [];
let textAccum = "";
let firstLoc = null;
const flushText = () => {
if (textAccum) {
chunks.push({ kind: null, text: textAccum });
locations.push(firstLoc);
textAccum = "";
firstLoc = null;
}
};
const addText = (text, loc) => {
if (!text) return;
if (!firstLoc) firstLoc = loc;
textAccum += text;
};
for (const node of span.childNodes) {
if (node.nodeType === Node.ELEMENT_NODE) {
const el = node;
const cls = (el.getAttribute("class") ?? "").trim();
if (kinds.has(cls)) {
flushText();
const text = el.textContent?.trim() ?? "";
if (text) {
chunks.push({ kind: cls, text });
locations.push({ type: "element", node: el });
}
} else if (cls === "symvar" && colors) {
const style = el.getAttribute("style") ?? "";
const m = style.match(/color\s*:\s*([^;]+)/i);
const rgb = m ? parseCssColor(m[1]) : null;
const kind = rgb ? colors.get(rgbKey(rgb)) ?? null : null;
if (kind) {
flushText();
const text = el.textContent?.trim() ?? "";
if (text) {
chunks.push({ kind, text });
locations.push({ type: "element", node: el });
}
}
} else if (INLINE_FORMATTING_TAGS2.has(el.tagName)) {
const text = el.textContent ?? "";
addText(text, { type: "element", node: el });
} else {
const text = el.textContent ?? "";
addText(text, { type: "element", node: el });
}
} else if (node.nodeType === Node.TEXT_NODE) {
const tn = node;
const value = tn.nodeValue ?? "";
if (value)
addText(value, { type: "text", node: tn, start: 0, end: value.length });
}
}
flushText();
return { chunks, locations };
}
function formatTokens(tokens) {
return tokens.map((t) => t.kind ? `${t.text}:${t.kind}` : t.text).join(" ");
}
// src/rule.ts
function runTokens(run) {
return extractGifText(run).split(" ");
}
function gifAssertionRule(doc) {
const assertion = doc.querySelector('table[summary="Assertion"]');
if (!assertion) return null;
const [conclusionRun] = findGifRuns(assertion);
if (!conclusionRun) return null;
const hypotheses = doc.querySelector('table[summary^="Hypothes"]');
const assumptions = hypotheses ? findGifRuns(hypotheses).map(runTokens) : [];
return { assumptions, conclusion: runTokens(conclusionRun) };
}
function uniAssertionRule(doc) {
const kinds = parseKindNames(doc);
const tokens = (span) => tokenizeMathSpan(span, kinds).map((t) => t.text);
const conclusion = doc.querySelector('table[summary="Assertion"] span.math');
if (!conclusion) return null;
const assumptions = [
...doc.querySelectorAll('table[summary^="Hypothes"] span.math')
].map(tokens);
return { assumptions, conclusion: tokens(conclusion) };
}
// src/grammar.ts
var GRAMMAR_CACHE_VERSION = "7";
function collectConstants(rules) {
const types = /* @__PURE__ */ new Set();
const variables = /* @__PURE__ */ new Set();
for (const rule of rules) {
types.add(rule.conclusion[0]);
for (const a of rule.assumptions) {
types.add(a[0]);
if (a.length === 2) variables.add(a[1]);
}
}
const constants = /* @__PURE__ */ new Set();
for (const rule of rules) {
for (const token of rule.conclusion.slice(1)) {
if (!types.has(token) && !variables.has(token)) constants.add(token);
}
}
return constants;
}
async function assembleGrammar(doc, pageUrl, fetcher, topRule, extract, kind, cache) {
const parser = new DOMParser();
const fetchDoc = async (url) => parser.parseFromString(await fetcher(url), "text/html");
const syntaxUrls = new Set(extractSyntaxHintUrls(doc, pageUrl));
for (const page of PRIMITIVE_SYNTAX_PAGES)
syntaxUrls.add(new URL(`${page}.html`, pageUrl).href);
const refHints = await Promise.all(
extractRefUrls(doc, pageUrl).map(
(url) => cache.get(`hints:${url}`, async () => {
const refDoc = await fetchDoc(url);
const hints = extractSyntaxHintUrls(refDoc, url);
if (hints.length > 0) return hints;
return extractBreakdownRefUrls(refDoc, url);
}).catch(() => [])
)
);
for (const urls of refHints) for (const url of urls) syntaxUrls.add(url);
const rules = await Promise.all(
[...syntaxUrls].map(
(url) => cache.get(`rule:${kind}:${url}`, async () => {
const rule = extract(await fetchDoc(url));
if (rule) rule.label = labelOf(url);
return rule;
}).catch(() => null)
)
);
const filtered = rules.filter((r) => r !== null);
const patternCharLen = (r) => r.conclusion.reduce((sum, t) => sum + t.length, 0);
filtered.sort(
(a, b) => b.conclusion.length - a.conclusion.length || patternCharLen(b) - patternCharLen(a)
);
return [topRule, ...filtered];
}
var labelOf = (url) => (url.split("/").pop() ?? "").replace(/\.html$/, "");
function usedLabels(proof, into) {
if (proof.rule.label) into.add(proof.rule.label);
for (const sub of proof.subproofs) usedLabels(sub, into);
}
function missingSyntaxHints(proofs, declared) {
const used = /* @__PURE__ */ new Set();
for (const proof of proofs) usedLabels(proof, used);
return [...used].filter((l) => l !== "cv" && !declared.has(l)).sort();
}
var memoOnly = () => createCache(null, GRAMMAR_CACHE_VERSION);
var assembleGifGrammar = (doc, pageUrl, fetcher, cache = memoOnly()) => assembleGrammar(
doc,
pageUrl,
fetcher,
GIF_TOP_RULE,
gifAssertionRule,
"gif",
cache
);
var assembleUniGrammar = (doc, pageUrl, fetcher, cache = memoOnly()) => assembleGrammar(
doc,
pageUrl,
fetcher,
UNI_TOP_RULE,
uniAssertionRule,
"uni",
cache
);
// src/indent.ts
function expressionParts(cell) {
const leader = cell.querySelector("span.i");
const math = cell.querySelector("span.math");
const turnstile = math ? math.firstElementChild : cell.querySelector("img[alt]");
return leader && turnstile ? { leader, turnstile } : null;
}
function indentProofExpressions(table) {
const measurements = [];
for (const tr of table.querySelectorAll("tr")) {
const tds = tr.querySelectorAll("td");
if (tds.length < 4) continue;
const cell = tds[3];
const parts = expressionParts(cell);
if (!parts) continue;
const indent = parts.turnstile.getBoundingClientRect().right - parts.leader.getBoundingClientRect().left;
if (indent > 0) measurements.push({ cell, indent });
}
for (const { cell, indent } of measurements) {
cell.style.paddingLeft = `${indent}px`;
cell.style.textIndent = `${-indent}px`;
}
}
// src/space.ts
var EX_PER_UNIT = 0.2;
var SPACE_CLASS = "mm-site-format-space";
function spacer(units) {
const span = document.createElement("span");
span.className = SPACE_CLASS;
span.style.cssText = `padding-left:${(units * EX_PER_UNIT).toFixed(2)}ex`;
return span;
}
function insertSpacers(located, units, onSplit) {
const base = located.length - units.length;
if (base < 0) return;
for (let i = units.length - 1; i >= 1; i--) {
if (units[i] <= 0) continue;
insertBefore(located[base + i].location, spacer(units[i]), onSplit);
}
}
function insertBefore(loc, node, onSplit) {
if (loc.type === "element") {
loc.node.parentNode?.insertBefore(node, loc.node);
return;
}
const at = loc.type === "folded" ? loc.offset : loc.start;
if (at === 0) {
loc.node.parentNode?.insertBefore(node, loc.node);
} else {
const fresh = loc.node.splitText(at);
onSplit?.(loc.node, fresh);
fresh.parentNode?.insertBefore(node, fresh);
}
}
// src/spans.ts
var nodeSpansCache = /* @__PURE__ */ new WeakMap();
function nodeSpans(proof) {
const cached = nodeSpansCache.get(proof);
if (cached) return cached;
const spans = [];
function walk(p, start) {
let offset = start;
let nextSub = 0;
for (const patternToken of p.rule.conclusion.slice(1)) {
if (p.subst.has(patternToken)) {
offset = walk(p.subproofs[nextSub++], offset);
} else {
offset += 1;
}
}
spans.push([start, offset]);
return offset;
}
walk(proof, 0);
nodeSpansCache.set(proof, spans);
return spans;
}
function nodeLocationSpans(proof, locationCount) {
const spans = nodeSpans(proof);
const rootEnd = Math.max(...spans.map((s) => s[1]));
const base = locationCount - rootEnd;
return spans.map(([s, e]) => [s + base, e + base]);
}
function smallestSpanContaining(spans, index) {
let best;
for (const [start, end] of spans) {
if (start <= index && index < end) {
if (!best || end - start < best[1] - best[0]) best = [start, end];
}
}
return best;
}
function spacingOf(proof, memo) {
const cached = memo.get(proof);
if (cached !== void 0) return cached;
const s = proof.subproofs.length === 0 ? -1 : Math.max(...proof.subproofs.map((p) => spacingOf(p, memo))) + 1;
memo.set(proof, s);
return s;
}
function gapUnits(proof) {
const memo = /* @__PURE__ */ new Map();
const units = [];
function walk(p, start) {
const spacing = spacingOf(p, memo);
const pattern = p.rule.conclusion.slice(1);
const holes = pattern.flatMap((tok, j) => p.subst.has(tok) ? [j] : []);
const firstHole = holes[0];
const lastHole = holes[holes.length - 1];
let offset = start;
let nextSub = 0;
pattern.forEach((tok, j) => {
if (j > 0) {
const interior = firstHole !== void 0 && j - 1 >= firstHole && j <= lastHole;
units[offset] = interior ? spacing : 0;
}
if (p.subst.has(tok)) offset = walk(p.subproofs[nextSub++], offset);
else offset += 1;
});
return offset;
}
walk(proof, 0);
units[0] = 0;
return units;
}
// src/highlight.ts
function rangeForSpan(locations, [start, end]) {
const range = document.createRange();
const first = locations[start];
const last = locations[end - 1];
if (first.type === "element") range.setStartBefore(first.node);
else if (first.type === "folded") range.setStart(first.node, first.offset);
else range.setStart(first.node, first.start);
if (last.type === "element") range.setEndAfter(last.node);
else if (last.type === "folded") range.setEndAfter(last.sub);
else range.setEnd(last.node, last.end);
return range;
}
function spanToHighlight(proof, locationCount, index) {
return smallestSpanContaining(nodeLocationSpans(proof, locationCount), index) ?? null;
}
function buildOccurrenceIndex(expressions) {
const index = /* @__PURE__ */ new Map();
for (const expr of expressions) {
if (!expr.proof) continue;
for (const span of nodeLocationSpans(expr.proof, expr.locations.length)) {
const key = expr.tokens.slice(span[0], span[1]).map((t) => t.text).join(" ");
let list = index.get(key);
if (!list) {
list = [];
index.set(key, list);
}
list.push({ expr, span });
}
}
return index;
}
function findTokenAt(locations, node, offset) {
for (let i = 0; i < locations.length; i++) {
const loc = locations[i];
if (loc.type === "text") {
if (loc.node === node && offset >= loc.start && offset < loc.end)
return i;
} else if (loc.type === "folded") {
if (loc.node === node && offset >= loc.offset && offset < loc.offset + 1)
return i;
if (loc.sub === node || loc.sub.contains(node)) return i;
} else if (loc.node === node || loc.node.contains(node)) {
return i;
}
}
return null;
}
var HIGHLIGHT_NAME = "mm-site-format";
var HIGHLIGHT_CLASS = "mm-site-format-hl";
var MATCH_NAME = "mm-site-format-match";
var MATCH_CLASS = "mm-site-format-match-hl";
var sharedHighlights = /* @__PURE__ */ new Map();
function createPainter(name = HIGHLIGHT_NAME, className = HIGHLIGHT_CLASS, color = HIGHLIGHT_COLOR) {
if (typeof CSS === "undefined" || !CSS?.highlights || typeof Highlight === "undefined") {
return null;
}
let highlight = sharedHighlights.get(name);
if (!highlight) {
highlight = new Highlight();
CSS.highlights.set(name, highlight);
sharedHighlights.set(name, highlight);
const style = document.createElement("style");
style.textContent = `::highlight(${name}){background-color:${color}}.${className}{background-color:${color}}`;
document.head.appendChild(style);
}
let painted = [];
const clear = () => {
highlight.clear();
for (const el of painted) el.classList.remove(className);
painted = [];
};
const paintOne = ({ locations, span: [start, end] }) => {
const range = rangeForSpan(locations, [start, end]);
highlight.add(range);
for (let i = start; i < end; i++) {
const loc = locations[i];
if (loc.type === "element") {
loc.node.classList.add(className);
painted.push(loc.node);
}
}
const ancestor = range.commonAncestorContainer;
const root = ancestor.nodeType === Node.ELEMENT_NODE ? ancestor : ancestor.parentElement;
for (const spacer2 of root?.querySelectorAll(`.${SPACE_CLASS}`) ?? []) {
if (range.intersectsNode(spacer2)) {
spacer2.classList.add(className);
painted.push(spacer2);
}
}
};
return {
clear,
paint(items) {
clear();
for (const item of items) paintOne(item);
}
};
}
function createHighlighter() {
const primary = createPainter();
const secondary = createPainter(
MATCH_NAME,
MATCH_CLASS,
HIGHLIGHT_MATCH_COLOR
);
if (!primary || !secondary) return null;
return {
clear() {
primary.clear();
secondary.clear();
},
highlight(index, expr, span) {
const [start, end] = span;
const key = expr.tokens.slice(start, end).map((t) => t.text).join(" ");
const all = index.get(key) ?? [];
const others = all.filter(
(o) => o.expr !== expr || o.span[0] !== start || o.span[1] !== end
);
secondary.paint(
others.map((o) => ({ locations: o.expr.locations, span: o.span }))
);
primary.paint([{ locations: expr.locations, span }]);
}
};
}
function caretAt(x, y) {
const d = document;
if (d.caretPositionFromPoint) {
const c = d.caretPositionFromPoint(x, y);
return c ? { node: c.offsetNode, offset: c.offset } : null;
}
if (d.caretRangeFromPoint) {
const r = d.caretRangeFromPoint(x, y);
return r ? { node: r.startContainer, offset: r.startOffset } : null;
}
return null;
}
function tokenAtPoint(locations, x, y) {
const el = document.elementFromPoint(x, y);
if (el) {
for (let i = 0; i < locations.length; i++) {
const loc = locations[i];
if (loc.type === "element" && (loc.node === el || loc.node.contains(el)))
return i;
}
}
if (el?.classList.contains(SPACE_CLASS)) {
for (let sib = el.nextSibling; sib; sib = sib.nextSibling) {
const i = findTokenAt(locations, sib, 0);
if (i !== null) return i;
}
}
const caret = caretAt(x, y);
if (!caret) return null;
const exact = findTokenAt(locations, caret.node, caret.offset);
if (exact !== null) return exact;
if (caret.node.nodeType === Node.TEXT_NODE) {
let best = null;
let bestEnd = -1;
for (let j = 0; j < locations.length; j++) {
const loc = locations[j];
if (loc.type === "text" && loc.node === caret.node && loc.end <= caret.offset && loc.end > bestEnd) {
bestEnd = loc.end;
best = j;
}
}
if (best !== null) return best;
}
return null;
}
function installHover(localExpressions, index, highlighter) {
if (!highlighter) return;
for (const expr of localExpressions) {
const proof = expr.proof;
const container = expr.locations[0]?.node.parentElement;
if (!proof || !container) continue;
container.addEventListener("mousemove", (event) => {
const i = tokenAtPoint(expr.locations, event.clientX, event.clientY);
const span = i === null ? null : spanToHighlight(proof, expr.locations.length, i);
if (span) highlighter.highlight(index, expr, span);
else highlighter.clear();
});
container.addEventListener("mouseleave", () => highlighter.clear());
}
}
// src/parse.ts
function makeParser(tokens, rules, kindOf) {
const memo = /* @__PURE__ */ new Map();
const active = /* @__PURE__ */ new Set();
const parse = (pos, type) => {
const key = `${pos}\0${type}`;
const cached = memo.get(key);
if (cached !== void 0) return cached;
if (active.has(key)) return null;
active.add(key);
const result = compute(pos, type);
active.delete(key);
memo.set(key, result);
return result;
};
const compute = (pos, type) => {
const token = tokens[pos];
if (token !== void 0 && kindOf(token) === type) {
return {
proof: {
rule: { assumptions: [], conclusion: [type, token] },
subst: /* @__PURE__ */ new Map(),
subproofs: []
},
next: pos + 1
};
}
for (const rule of rules) {
if (rule.conclusion[0] !== type) continue;
const matched = matchPattern(rule.conclusion.slice(1), pos);
if (matched) {
return {
proof: { rule, subst: matched.subst, subproofs: matched.subproofs },
next: matched.next
};
}
}
return null;
};
const matchPattern = (pattern, pos) => {
const subst = /* @__PURE__ */ new Map();
const subproofs = [];
let p = pos;
for (const patternToken of pattern) {
const holeKind = kindOf(patternToken);
if (holeKind === void 0) {
if (tokens[p] !== patternToken) return null;
p += 1;
continue;
}
const sub = parse(p, holeKind);
if (!sub) return null;
const consumed = tokens.slice(p, sub.next);
const existing = subst.get(patternToken);
if (existing) {
if (existing.length !== consumed.length || existing.some((t, j) => t !== consumed[j]))
return null;
} else {
subst.set(patternToken, consumed);
subproofs.push(sub.proof);
}
p = sub.next;
}
return { subst, subproofs, next: p };
};
return parse;
}
function parseExpression(tokens, type, rules, kindOf) {
const result = makeParser(tokens, rules, kindOf)(0, type);
return result && result.next === tokens.length ? result.proof : null;
}
function proofConclusion(proof) {
const out = [];
for (const token of proof.rule.conclusion) {
const replacement = proof.subst.get(token);
if (replacement) out.push(...replacement);
else out.push(token);
}
return out;
}
function posKey(pos) {
return `${pos.chunk}:${pos.offset}`;
}
function skipWs(chunks, pos) {
let { chunk, offset } = pos;
while (chunk < chunks.length) {
const c = chunks[chunk];
if (c.kind !== null) break;
while (offset < c.text.length && /\s/.test(c.text[offset])) offset++;
if (offset < c.text.length) break;
chunk++;
offset = 0;
}
return { chunk, offset };
}
function atEnd(chunks, pos) {
return pos.chunk >= chunks.length;
}
function makeChunkParser(chunks, rules, kindOf) {
const memo = /* @__PURE__ */ new Map();
const active = /* @__PURE__ */ new Set();
const parse = (pos, type) => {
pos = skipWs(chunks, pos);
const key = `${posKey(pos)}\0${type}`;
const cached = memo.get(key);
if (cached !== void 0) return cached;
if (active.has(key)) return null;
active.add(key);
const result = compute(pos, type);
active.delete(key);
memo.set(key, result);
return result;
};
const compute = (pos, type) => {
if (atEnd(chunks, pos)) return null;
const c = chunks[pos.chunk];
if (c.kind !== null && pos.offset === 0 && c.kind === type) {
return {
proof: {
rule: { assumptions: [], conclusion: [type, c.text] },
subst: /* @__PURE__ */ new Map(),
subproofs: []
},
next: { chunk: pos.chunk + 1, offset: 0 }
};
}
if (c.kind === null) {
const rest = c.text.slice(pos.offset);
const wordEnd = rest.search(/\s|$/);
const word = rest.slice(0, wordEnd || rest.length);
if (word && kindOf(word) === type) {
const nextOffset = pos.offset + word.length;
const next = nextOffset >= c.text.length ? { chunk: pos.chunk + 1, offset: 0 } : { chunk: pos.chunk, offset: nextOffset };
return {
proof: {
rule: { assumptions: [], conclusion: [type, word] },
subst: /* @__PURE__ */ new Map(),
subproofs: []
},
next
};
}
}
for (const rule of rules) {
if (rule.conclusion[0] !== type) continue;
const matched = matchPattern(rule, pos);
if (matched) {
return {
proof: { rule, subst: matched.subst, subproofs: matched.subproofs },
next: matched.next
};
}
}
return null;
};
const matchPattern = (rule, pos) => {
const ruleVars = /* @__PURE__ */ new Map();
for (const a of rule.assumptions) {
if (a.length === 2) ruleVars.set(a[1], a[0]);
}
const pattern = rule.conclusion.slice(1);
const subst = /* @__PURE__ */ new Map();
const subproofs = [];
let p = skipWs(chunks, pos);
for (const patternToken of pattern) {
p = skipWs(chunks, p);
if (atEnd(chunks, p)) return null;
const holeKind = ruleVars.get(patternToken);
if (holeKind === void 0) {
const c = chunks[p.chunk];
if (c.kind !== null) return null;
if (!c.text.startsWith(patternToken, p.offset)) return null;
const nextOffset = p.offset + patternToken.length;
p = nextOffset >= c.text.length ? { chunk: p.chunk + 1, offset: 0 } : { chunk: p.chunk, offset: nextOffset };
continue;
}
const sub = parse(p, holeKind);
if (!sub) return null;
const consumed = proofConclusion(sub.proof).slice(1);
const existing = subst.get(patternToken);
if (existing) {
if (existing.length !== consumed.length || existing.some((t, i) => t !== consumed[i]))
return null;
} else {
subst.set(patternToken, consumed);
subproofs.push(sub.proof);
}
p = sub.next;
}
return { subst, subproofs, next: p };
};
return parse;
}
function parseChunks(chunks, type, rules, kindOf) {
const parser = makeChunkParser(chunks, rules, kindOf);
const result = parser({ chunk: 0, offset: 0 }, type);
if (!result) return null;
const end = skipWs(chunks, result.next);
return atEnd(chunks, end) ? result.proof : null;
}
// src/page.ts
function buildKindRegistry(located, rules) {
const registry = /* @__PURE__ */ new Map();
for (const lts of located) {
for (const { token } of lts)
if (token.kind) registry.set(token.text, token.kind);
}
for (const rule of rules) {
for (const a of rule.assumptions) {
if (a.length === 2) registry.set(a[1], a[0]);
}
}
return (token) => registry.get(token);
}
function buildChunkKindRegistry(allChunks, rules) {
const registry = /* @__PURE__ */ new Map();
for (const chunks of allChunks) {
for (const chunk of chunks)
if (chunk.kind) registry.set(chunk.text, chunk.kind);
}
for (const rule of rules) {
for (const a of rule.assumptions) {
if (a.length === 2) registry.set(a[1], a[0]);
}
}
return (token) => registry.get(token);
}
function parseLocated(located, rules, kindOf) {
const resolve = kindOf ?? buildKindRegistry(located, rules);
const turnstile = rules[0]?.conclusion[1];
return located.map((lts) => {
const tokens = lts.map((lt) => lt.token);
const locations = lts.map((lt) => lt.location);
const expr = tokens.map((t) => t.text);
const proof = expr[0] === turnstile ? parseExpression(expr, TOP_TYPE, rules, resolve) : parseExpression(expr.slice(1), expr[0] ?? "", rules, resolve);
return { tokens, locations, proof };
});
}
function withLocations(expr, relocated) {
return {
tokens: relocated.map((lt) => lt.token),
locations: relocated.map((lt) => lt.location),
proof: expr.proof
};
}
async function parseGifExpressions(doc, pageUrl, fetcher, sample, root = doc, cache = createCache(null, GRAMMAR_CACHE_VERSION)) {
const t0 = DEV_PERF_LOG ? performance.now() : 0;
const colors = parseKindColors(doc);
const kindCache = /* @__PURE__ */ new Map();
const runs = findGifRuns(root);
const located = runs.map(
(run) => locateGifRun(run, colors, sample, kindCache)
);
const t1 = DEV_PERF_LOG ? performance.now() : 0;
const rules = await assembleGifGrammar(doc, pageUrl, fetcher, cache);
const t2 = DEV_PERF_LOG ? performance.now() : 0;
const parsed = parseLocated(located, rules);
const t3 = DEV_PERF_LOG ? performance.now() : 0;
const result = parsed.map((expr, i) => {
if (!expr.proof) return expr;
const nodes = [...runs[i]];
insertSpacers(located[i], gapUnits(expr.proof), (oldNode, freshNode) => {
const k = nodes.indexOf(oldNode);
if (k >= 0) nodes.splice(k + 1, 0, freshNode);
});
return withLocations(expr, locateGifRun(nodes, colors, sample, kindCache));
});
if (DEV_PERF_LOG) {
const t4 = performance.now();
const parsedCount = parsed.filter((e) => e.proof !== null).length;
console.log(
`[mm-site-format] PERF parseGifExpressions: ${runs.length} runs, ${parsedCount} parsed, ${rules.length} rules | tokenize=${(t1 - t0).toFixed(0)}ms grammar=${(t2 - t1).toFixed(0)}ms parse=${(t3 - t2).toFixed(0)}ms space=${(t4 - t3).toFixed(0)}ms total=${(t4 - t0).toFixed(0)}ms`
);
}
return result;
}
async function parseUniExpressions(doc, pageUrl, fetcher, root = doc, cache = createCache(null, GRAMMAR_CACHE_VERSION)) {
const t0 = DEV_PERF_LOG ? performance.now() : 0;
const colors = parseKindColors(doc);
const kinds = new Set(colors.values());
const rules = await assembleUniGrammar(doc, pageUrl, fetcher, cache);
const t1 = DEV_PERF_LOG ? performance.now() : 0;
const constants = collectConstants(rules);
const spans = findMathSpans(root);
const chunked = spans.map((span) => chunkifyMathSpan(span, kinds, colors));
const chunkKindOf = buildChunkKindRegistry(
chunked.map((c) => c.chunks),
rules
);
const t2 = DEV_PERF_LOG ? performance.now() : 0;
const turnstile = rules[0]?.conclusion[1];
const proofs = chunked.map(({ chunks }) => {
let parseChunksArr = chunks;
let type = TOP_TYPE;
if (chunks.length > 0 && chunks[0].kind === null && chunks[0].text.trimStart().startsWith(turnstile ?? "\0")) {
type = TOP_TYPE;
parseChunksArr = chunks;
} else if (chunks.length > 0 && chunks[0].kind === null) {
const text = chunks[0].text;
const stripped = text.trimStart();
const wordEnd = stripped.search(/\s|$/);
type = stripped.slice(0, wordEnd || stripped.length);
const afterWord = stripped.slice(wordEnd || stripped.length);
if (afterWord.trimStart()) {
parseChunksArr = [{ kind: null, text: afterWord }, ...chunks.slice(1)];
} else {
parseChunksArr = chunks.slice(1);
}
}
return parseChunks(parseChunksArr, type, rules, chunkKindOf);
});
const t3 = DEV_PERF_LOG ? performance.now() : 0;
const result = proofs.map((proof, i) => {
const located = locateMathSpan(spans[i], kinds, constants, colors);
const tokens = located.map((lt) => lt.token);
const locations = located.map((lt) => lt.location);
if (!proof) return { tokens, locations, proof: null };
insertSpacers(located, gapUnits(proof));
const relocated = locateMathSpan(spans[i], kinds, constants, colors);
return {
tokens: relocated.map((lt) => lt.token),
locations: relocated.map((lt) => lt.location),
proof
};
});
if (DEV_PERF_LOG) {
const t4 = performance.now();
const parsed = proofs.filter((p) => p !== null).length;
console.log(
`[mm-site-format] PERF parseUniExpressions: ${spans.length} spans, ${parsed} parsed, ${rules.length} rules | grammar=${(t1 - t0).toFixed(0)}ms chunkify=${(t2 - t1).toFixed(0)}ms parse=${(t3 - t2).toFixed(0)}ms retokenize+space=${(t4 - t3).toFixed(0)}ms total=${(t4 - t0).toFixed(0)}ms`
);
}
return result;
}
// src/proof.ts
function substituteExpr(sub, expr) {
const out = [];
for (const token of expr) {
const replacement = sub.get(token);
if (replacement) out.push(...replacement);
else out.push(token);
}
return out;
}
function substitute(sub, rule) {
return {
assumptions: rule.assumptions.map((a) => substituteExpr(sub, a)),
conclusion: substituteExpr(sub, rule.conclusion)
};
}
// src/diff.ts
var keyCache = /* @__PURE__ */ new WeakMap();
function proofKey(p) {
let k = keyCache.get(p);
if (k === void 0) {
k = substitute(p.subst, p.rule).conclusion.join(" ");
keyCache.set(p, k);
}
return k;
}
function collectKeys(p, out) {
out.add(proofKey(p));
for (const sub of p.subproofs) collectKeys(sub, out);
}
function findMaximalMatches(p, available, out) {
if (available.has(proofKey(p))) {
out.add(p);
return;
}
for (const sub of p.subproofs) findMaximalMatches(sub, available, out);
}
var commonSubtreeDiff = (a, b) => {
const keysA = /* @__PURE__ */ new Set();
const keysB = /* @__PURE__ */ new Set();
collectKeys(a, keysA);
collectKeys(b, keysB);
const unchangedInA = /* @__PURE__ */ new Set();
const unchangedInB = /* @__PURE__ */ new Set();
findMaximalMatches(a, keysB, unchangedInA);
findMaximalMatches(b, keysA, unchangedInB);
return { unchangedInA, unchangedInB };
};
var diffCache = /* @__PURE__ */ new WeakMap();
function cachedDiff(algo, a, b) {
let bMap = diffCache.get(a);
if (!bMap) {
bMap = /* @__PURE__ */ new WeakMap();
diffCache.set(a, bMap);
}
let result = bMap.get(b);
if (!result) {
result = algo(a, b);
bMap.set(b, result);
}
return result;
}
function changedLocationSpans(proof, locationCount, unchanged) {
const unchangedSpans = [];
let rootEnd = 0;
function walk(p, start) {
let offset = start;
let nextSub = 0;
for (const tok of p.rule.conclusion.slice(1)) {
if (p.subst.has(tok)) offset = walk(p.subproofs[nextSub++], offset);
else offset += 1;
}
if (unchanged.has(p)) unchangedSpans.push([start, offset]);
if (offset > rootEnd) rootEnd = offset;
return offset;
}
walk(proof, 0);
const base = locationCount - rootEnd;
unchangedSpans.sort((x, y) => x[0] - y[0]);
const changed = [];
let cursor = 0;
for (const [s, e] of unchangedSpans) {
if (cursor < s) changed.push([cursor + base, s + base]);
cursor = cursor > e ? cursor : e;
}
if (cursor < rootEnd) changed.push([cursor + base, rootEnd + base]);
return changed;
}
// src/tooltip.ts
var tooltipEl = null;
function getTooltip() {
if (!tooltipEl) {
tooltipEl = document.createElement("div");
tooltipEl.className = "mm-site-format-ref-tooltip";
tooltipEl.style.display = "none";
}
if (!tooltipEl.isConnected) document.body.appendChild(tooltipEl);
return tooltipEl;
}
function positionTooltip(tt, e) {
const GAP = 12;
const ttRect = tt.getBoundingClientRect();
let left = e.clientX + GAP;
let top = e.clientY + GAP;
if (window.innerWidth > 0 && left + ttRect.width > window.innerWidth)
left = e.clientX - ttRect.width - GAP;
if (window.innerHeight > 0 && top + ttRect.height > window.innerHeight)
top = e.clientY - ttRect.height - GAP;
tt.style.left = `${Math.round(Math.max(0, left))}px`;
tt.style.top = `${Math.round(Math.max(0, top))}px`;
}
function attachTooltip(ref, getContent) {
const titles = [];
if (ref.hasAttribute("title")) {
titles.push(ref.getAttribute("title"));
ref.removeAttribute("title");
}
for (const a of ref.querySelectorAll("a[title]")) {
titles.push(a.getAttribute("title"));
a.removeAttribute("title");
}
const populate = (tt, node) => {
tt.replaceChildren(node);
if (titles.length > 0) {
const desc = document.createElement("div");
desc.className = "mm-site-format-ref-tooltip-desc";
desc.textContent = titles.join("\n");
tt.appendChild(desc);
}
};
let lastEvent = null;
ref.addEventListener("mouseenter", (e) => {
lastEvent = e;
const tt = getTooltip();
const result = getContent();
if (result instanceof Promise) {
tt.replaceChildren(document.createTextNode("\u2026"));
tt.style.display = "";
positionTooltip(tt, e);
result.then((node) => {
if (!lastEvent) return;
if (node === null) {
tt.style.display = "none";
return;
}
populate(tt, node);
positionTooltip(tt, lastEvent);
}).catch(() => {
});
} else if (result !== null) {
populate(tt, result);
tt.style.display = "";
positionTooltip(tt, e);
}
});
ref.addEventListener("mouseleave", () => {
lastEvent = null;
getTooltip().style.display = "none";
});
}
// src/render.ts
var OPERATOR = "\u21D0";
var TERMINAL = "\u21D4";
function clone(source) {
const span = document.createElement("span");
for (const node of source.childNodes) span.appendChild(node.cloneNode(true));
return span;
}
function appendSeries(parent, items) {
items.forEach((item, i) => {
if (i > 0)
parent.append(
i < items.length - 1 ? ", " : items.length > 2 ? ", and " : " and "
);
parent.append(item);
});
}
var CONTENT_CLASS = {
expr: "mm-site-format-calc-expr",
hint: "mm-site-format-calc-hint",
subcalc: "mm-site-format-calc-subcalc"
};
var ROW_CLASS = {
expr: "",
hint: "mm-site-format-calc-row--hint",
subcalc: "mm-site-format-calc-row--subcalc"
};
function row(operator, content, kind) {
const tr = document.createElement("tr");
tr.className = ROW_CLASS[kind];
const op = document.createElement("td");
op.className = "mm-site-format-calc-op";
if (typeof operator === "string") op.textContent = operator;
else op.appendChild(operator);
const main = document.createElement("td");
main.className = CONTENT_CLASS[kind];
main.appendChild(content);
tr.append(op, main);
return tr;
}
function installDiffHover(opCell, aboveExpr, belowExpr, options) {
const painter = options.diffPainter;
const algo = options.diffAlgorithm ?? commonSubtreeDiff;
const exprFor = options.exprFor;
opCell.style.cursor = "crosshair";
opCell.addEventListener("mouseenter", () => {
if (!exprFor) return;
const above = exprFor(aboveExpr);
const below = exprFor(belowExpr);
if (!above?.proof || !below?.proof) return;
const { unchangedInA, unchangedInB } = cachedDiff(
algo,
above.proof,
below.proof
);
const items = [
...changedLocationSpans(
above.proof,
above.locations.length,
unchangedInA
).map((span) => ({ locations: above.locations, span })),
...changedLocationSpans(
below.proof,
below.locations.length,
unchangedInB
).map((span) => ({ locations: below.locations, span }))
];
painter.paint(items);
});
opCell.addEventListener("mouseleave", () => painter.clear());
}
function appendStep(step, tbody, options) {
const expr = clone(step.expressionHtml);
tbody.appendChild(row("", expr, "expr"));
const effectiveSpine = step.spine !== null ? step.subcalculations[step.spine] : null;
const items = [];
let nested = 0;
step.subcalculations.forEach((sub, i) => {
if (i === step.spine) return;
if (sub.kind === "given") {
const refEl = clone(sub.hypothesisRefHtml);
const href = sub.hypothesisRefHtml.querySelector("a")?.getAttribute("href") ?? null;
const fetchRule2 = options?.fetchRuleTooltip;
attachTooltip(
refEl,
href && fetchRule2 && !href.startsWith("#") ? () => fetchRule2(href) : () => clone(sub.expressionHtml)
);
items.push(refEl);
for (let li = 0; li < (sub.leafRefHtmls ?? []).length; li++) {
const leafRef = sub.leafRefHtmls[li];
const leafEl = clone(leafRef);
const leafHref = leafRef.querySelector("a")?.getAttribute("href") ?? null;
const leafExpr = sub.leafExpressionHtmls?.[li];
attachTooltip(
leafEl,
leafHref && fetchRule2 && !leafHref.startsWith("#") ? () => fetchRule2(leafHref) : leafExpr ? () => clone(leafExpr) : () => clone(sub.expressionHtml)
);
items.push(leafEl);
}
} else nested++;
});
if (nested > 0)
items.push(
document.createTextNode(nested === 1 ? "subproof" : "subproofs")
);
const ruleRef = clone(step.inferenceRuleRefHtml);
const ruleHref = step.inferenceRuleRefHtml.querySelector("a")?.getAttribute("href") ?? null;
const fetchRule = options?.fetchRuleTooltip;
attachTooltip(
ruleRef,
ruleHref && fetchRule ? () => fetchRule(ruleHref) : () => expr.cloneNode(true)
);
items.push(ruleRef);
const hint = document.createElement("span");
hint.append("{ using ");
appendSeries(hint, items);
for (const foldedRefEl of step.foldedRuleRefs ?? []) {
const ref = clone(foldedRefEl);
const href = foldedRefEl.querySelector("a")?.getAttribute("href") ?? null;
attachTooltip(
ref,
href && fetchRule ? () => fetchRule(href) : () => expr.cloneNode(true)
);
hint.append("; using ");
hint.append(ref);
}
hint.append(" }");
const ended = effectiveSpine === null;
const hintRow = row(ended ? TERMINAL : OPERATOR, hint, "hint");
tbody.appendChild(hintRow);
step.subcalculations.forEach((sub, i) => {
if (sub.kind === "step" && i !== step.spine) {
const placeholder = document.createElement("table");
const pTbody = document.createElement("tbody");
placeholder.appendChild(pTbody);
const conclusionExpr = clone(sub.expressionHtml);
pTbody.appendChild(row("", conclusionExpr, "expr"));
makeLazyCollapsible(placeholder, sub, options);
tbody.appendChild(row("", placeholder, "subcalc"));
}
});
if (ended) {
tbody.appendChild(row("", document.createTextNode("TRUE"), "expr"));
return expr;
}
let spineExpr = null;
if (effectiveSpine?.kind === "given")
spineExpr = appendGiven(effectiveSpine, tbody, options);
else if (effectiveSpine?.kind === "step")
spineExpr = appendStep(effectiveSpine, tbody, options);
if (options?.diffPainter && spineExpr) {
const opCell = hintRow.firstElementChild;
installDiffHover(opCell, expr, spineExpr, options);
}
return expr;
}
function appendGiven(given, tbody, options) {
const ref = document.createElement("span");
ref.append("(", clone(given.hypothesisRefHtml), ")");
const expr = clone(given.expressionHtml);
const href = given.hypothesisRefHtml.querySelector("a")?.getAttribute("href") ?? null;
const fetchRule = options?.fetchRuleTooltip;
attachTooltip(
ref,
href && fetchRule && !href.startsWith("#") ? () => fetchRule(href) : () => expr.cloneNode(true)
);
tbody.appendChild(row(ref, expr, "expr"));
return expr;
}
function makeLazyCollapsible(table, calc, options) {
const tbody = table.querySelector("tbody");
const conclusion = tbody.firstElementChild;
const marker = document.createElement("span");
marker.className = "mm-site-format-fold";
const markerCell = conclusion.firstElementChild ?? conclusion;
markerCell.style.textAlign = "left";
markerCell.appendChild(marker);
let collapsed = true;
let rendered = false;
let restRows = [];
const expand = () => {
if (!rendered) {
const full = renderCalcTable(calc, options);
const fullTbody = full.querySelector("tbody");
const fullRows = [...fullTbody.children];
const realConclusion = fullRows[0];
conclusion.replaceWith(realConclusion);
const markerCell2 = realConclusion.firstElementChild ?? realConclusion;
markerCell2.style.textAlign = "left";
markerCell2.appendChild(marker);
restRows = fullRows.slice(1);
for (const r of restRows) tbody.appendChild(r);
if (restRows.length > 0) {
restRows[0].style.cursor = "pointer";
restRows[0].addEventListener("click", toggle);
}
rendered = true;
options?.onLazyRender?.(tbody);
}
for (const r of restRows) r.style.display = "";
marker.textContent = "\u25BC";
};
const refresh = () => {
if (collapsed) {
for (const r of restRows) r.style.display = "none";
marker.textContent = "\u25B6";
} else {
expand();
}
};
const toggle = () => {
collapsed = !collapsed;
refresh();
};
marker.addEventListener("click", (e) => {
e.stopPropagation();
toggle();
});
conclusion.style.cursor = "pointer";
conclusion.addEventListener("click", toggle);
refresh();
}
function renderCalcTable(calc, options) {
const table = document.createElement("table");
const tbody = document.createElement("tbody");
table.appendChild(tbody);
if (calc.kind === "given") appendGiven(calc, tbody, options);
else appendStep(calc, tbody, options);
return table;
}
function renderCalculation(calc, options) {
const box = document.createElement("div");
box.className = "mm-site-format-calc";
box.appendChild(renderCalcTable(calc, options));
return box;
}
// src/rule-tooltip.ts
var OP_IMPLIES = " \u21D0\xA0\xA0";
var OP_AND = " &\xA0\xA0";
function buildRuleContent(doc) {
const conclusionSpan = doc.querySelector(
'table[summary="Assertion"] span.math'
);
if (conclusionSpan) {
const hypSpans = [
...doc.querySelectorAll('table[summary^="Hypothes"] span.math')
];
const container2 = document.createElement("span");
container2.appendChild(conclusionSpan.cloneNode(true));
hypSpans.forEach((hyp, i) => {
container2.append(
document.createElement("br"),
i === 0 ? OP_IMPLIES : OP_AND
);
container2.appendChild(hyp.cloneNode(true));
});
return container2;
}
const assertionTable = doc.querySelector('table[summary="Assertion"]');
if (!assertionTable) return null;
const [conclusionRun] = findGifRuns(assertionTable);
if (!conclusionRun) return null;
const hypTable = doc.querySelector('table[summary^="Hypothes"]');
const hypRuns = hypTable ? findGifRuns(hypTable) : [];
const container = document.createElement("span");
for (const node of conclusionRun) container.appendChild(node.cloneNode(true));
hypRuns.forEach((run, i) => {
container.append(
document.createElement("br"),
i === 0 ? OP_IMPLIES : OP_AND
);
for (const node of run) container.appendChild(node.cloneNode(true));
});
return container;
}
function attachRuleTooltipsToPage(root, fetchRuleTooltip) {
const nbspOnly = /^\s*\u00a0\s*$/;
for (const a of root.querySelectorAll("a[href]")) {
const href = a.getAttribute("href");
if (href.startsWith("#")) continue;
const next = a.nextSibling;
if (next?.nodeType === Node.TEXT_NODE && nbspOnly.test(next.textContent ?? "") && next.nextSibling?.classList?.contains("r")) {
attachTooltip(a, () => fetchRuleTooltip(href));
}
}
}
function makeRuleTooltipFetcher(pageUrl, fetcher) {
const cache = /* @__PURE__ */ new Map();
const parser = new DOMParser();
return function fetchRuleTooltip(href) {
const url = new URL(href, pageUrl).href;
let pending = cache.get(url);
if (!pending) {
pending = fetcher(url).then(
(html) => buildRuleContent(parser.parseFromString(html, "text/html"))
).catch(() => null);
cache.set(url, pending);
}
return pending;
};
}
// src/spine.ts
function structuralOverlap(a, b) {
const aLeaf = a.subproofs.length === 0;
const bLeaf = b.subproofs.length === 0;
if (aLeaf && bLeaf) return 1;
if (aLeaf || bLeaf) return 0;
if (a.rule.conclusion.join(" ") !== b.rule.conclusion.join(" ")) return 0;
if (a.subproofs.length !== b.subproofs.length) return 0;
let matched = 1;
for (let i = 0; i < a.subproofs.length; i++) {
const ai = a.subproofs[i];
const bi = b.subproofs[i];
const aiLeaf = ai.subproofs.length === 0;
const biLeaf = bi.subproofs.length === 0;
if (aiLeaf && biLeaf) matched++;
else if (!aiLeaf && !biLeaf && ai.rule.conclusion.join(" ") === bi.rule.conclusion.join(" "))
matched++;
}
return matched;
}
function treeSize(proof) {
let n = 1;
for (const child of proof.subproofs) n += treeSize(child);
return n;
}
function lcsLength(a, b) {
const prev = new Array(b.length + 1).fill(0);
for (let i = 1; i <= a.length; i++) {
let diag = 0;
for (let j = 1; j <= b.length; j++) {
const here = prev[j];
prev[j] = a[i - 1] === b[j - 1] ? diag + 1 : Math.max(prev[j], prev[j - 1]);
diag = here;
}
}
return prev[b.length];
}
function anchorSpine(anchorTokens, subproofTokens) {
const scores = subproofTokens.map(
(t) => t !== null ? lcsLength(anchorTokens, t) : -1
);
const best = Math.max(...scores);
if (best < 0) return null;
const bestIndices = scores.reduce(
(acc, s, i) => s === best ? [...acc, i] : acc,
[]
);
return bestIndices.length === 1 ? bestIndices[0] : null;
}
var SMALL_STEP_MAX_DIFF = 2;
function isSmallStep(step, continuation) {
const lcs = lcsLength(step, continuation);
const ratio = Math.log2(
(continuation.length - lcs + 1) / (step.length - lcs + 1)
);
return ratio <= SMALL_STEP_MAX_DIFF;
}
function maxSubtreeOverlap(target, tree) {
let best = structuralOverlap(target, tree);
for (const child of tree.subproofs) {
const c = maxSubtreeOverlap(target, child);
if (c > best) best = c;
}
return best;
}
function divergingSubtreeOverlap(conclusion, hypothesis) {
const cLeaf = conclusion.subproofs.length === 0;
const hLeaf = hypothesis.subproofs.length === 0;
if (cLeaf && hLeaf) return 0;
if (cLeaf || hLeaf || conclusion.rule.conclusion.join(" ") !== hypothesis.rule.conclusion.join(" ") || conclusion.subproofs.length !== hypothesis.subproofs.length)
return maxSubtreeOverlap(conclusion, hypothesis);
let total = 0;
for (let i = 0; i < conclusion.subproofs.length; i++)
total += divergingSubtreeOverlap(
conclusion.subproofs[i],
hypothesis.subproofs[i]
);
return total;
}
function firstDivergingPosition(conclusion, hypothesis) {
for (let i = 0; i < conclusion.subproofs.length; i++) {
const ci = conclusion.subproofs[i];
const hi = hypothesis.subproofs[i];
const ciLeaf = ci.subproofs.length === 0;
const hiLeaf = hi.subproofs.length === 0;
if (ciLeaf && hiLeaf) continue;
if (!ciLeaf && !hiLeaf && ci.rule.conclusion.join(" ") === hi.rule.conclusion.join(" "))
continue;
return i;
}
return conclusion.subproofs.length;
}
function chooseSpine(conclusion, subproofs) {
if (subproofs.length === 0) return null;
const overlap = subproofs.map((s) => structuralOverlap(conclusion, s.parse));
const best = Math.max(...overlap);
const top = subproofs.map((s, i) => ({ index: i, trivial: s.trivial, size: treeSize(s.parse) })).filter(({ index }) => overlap[index] === best);
const nonTrivial = top.filter((t) => !t.trivial);
if (nonTrivial.length === 0) return top.length === 1 ? top[0].index : null;
if (nonTrivial.length === 1) return nonTrivial[0].index;
const fdp = nonTrivial.map(
(t) => firstDivergingPosition(conclusion, subproofs[t.index].parse)
);
const minFdp = Math.min(...fdp);
const fdpTop = nonTrivial.filter((_, i) => fdp[i] === minFdp);
if (fdpTop.length === 1) return fdpTop[0].index;
const mso = fdpTop.map(
(t) => divergingSubtreeOverlap(conclusion, subproofs[t.index].parse)
);
const minMso = Math.min(...mso);
const msoTop = fdpTop.filter((_, i) => mso[i] === minMso);
if (msoTop.length === 1) return msoTop[0].index;
const minSize = Math.min(...msoTop.map((t) => t.size));
const smallest = msoTop.filter((t) => t.size === minSize);
return smallest.length === 1 ? smallest[0].index : null;
}
// src/styles.ts
var CSS2 = `
.mm-site-format-calc { box-sizing:border-box; border:1px solid #ccc; padding:6px 10px; margin:8px 0; text-align:left; font-weight:normal }
.mm-site-format-calc table { border:none; border-collapse:collapse; margin:0 }
.mm-site-format-calc td { border:none; vertical-align:top }
.mm-site-format-calc-op { padding-right:0.6em; white-space:nowrap; text-align:right }
.mm-site-format-calc-expr { padding-left:1.6em; text-indent:-1.6em }
.mm-site-format-calc-hint { padding-left:calc(1.5em + 1.3ch); text-indent:-1.3ch }
.mm-site-format-calc-subcalc { padding-left:2em }
.mm-site-format-calc-row--hint > td { padding-top:0.3em; padding-bottom:0.3em }
.mm-site-format-calc-row--subcalc > td { padding-top:0.5em; padding-bottom:0.5em }
.mm-site-format-calc-label { font-size:0.9em; font-style:italic; color:#555; margin:0.8em 0 0.2em; border-top:1px solid #ddd; padding-top:0.4em }
.mm-site-format-fold { cursor:pointer; user-select:none; opacity:0.6 }
.mm-site-format-banner { position:fixed; bottom:0; right:0; background:#333; color:#fff; padding:4px 8px; font-size:12px; opacity:0.8; z-index:9999 }
.mm-site-format-parse-warn { color:#f90 }
.mm-site-format-view-box { position:fixed; top:0; right:0; background:#f4f4f4; border:1px solid #ccc; border-top:none; border-right:none; padding:4px 8px; font-size:13px; z-index:9999 }
.mm-site-format-ref-tooltip { position:fixed; z-index:10000; background:InfoBackground; color:InfoText; border:1px solid InfoText; padding:4px 6px; font:small/1.4 sans-serif; pointer-events:none; max-width:80vw }
.mm-site-format-ref-tooltip-desc { margin-top:4px; padding-top:4px; border-top:1px solid InfoText; white-space:pre-wrap }
`;
var STYLE_ID = "mm-site-format-styles";
function injectStyles() {
if (document.getElementById(STYLE_ID)) return;
const style = document.createElement("style");
style.id = STYLE_ID;
style.textContent = CSS2;
document.head.appendChild(style);
}
// src/table.ts
function parseProofTableLazy(doc) {
const table = doc.querySelector('table[summary="Proof of theorem"]');
if (!table) return null;
const rows = /* @__PURE__ */ new Map();
let lastStep = 0;
for (const tr of table.querySelectorAll("tr")) {
const tds = tr.querySelectorAll("td");
if (tds.length < 4) continue;
const step = Number(tds[0].textContent?.trim());
if (!Number.isInteger(step)) continue;
const hyps = [...(tds[1].textContent ?? "").matchAll(/\d+/g)].map(
(m) => Number(m[0])
);
rows.set(step, {
ref: tds[2],
expression: tds[3],
// raw cell -- clone deferred
cell: tds[3],
hyps
});
if (step > lastStep) lastStep = step;
}
if (rows.size === 0) return null;
const memo = /* @__PURE__ */ new Map();
const build = (step) => {
const cached = memo.get(step);
if (cached) return cached;
const row2 = rows.get(step);
if (!row2) throw new Error(`proof table references missing step ${step}`);
const node = {
refHtml: row2.ref,
expressionHtml: row2.expression,
// still the raw cell
expressionCell: row2.cell,
subproofs: row2.hyps.map(build)
};
memo.set(step, node);
return node;
};
const tree = build(lastStep);
const stepOf = /* @__PURE__ */ new Map();
for (const [step, node] of memo) stepOf.set(node, step);
return { tree, stepOf };
}
function materializeExpressions(tree) {
const visited = /* @__PURE__ */ new Set();
const walk = (node) => {
if (visited.has(node)) return;
visited.add(node);
const cell = node.expressionHtml;
const html = cell.innerHTML;
const ownerDoc = cell.ownerDocument;
let cached = null;
Object.defineProperty(node, "expressionHtml", {
get() {
if (!cached) {
cached = ownerDoc.createElement("span");
cached.innerHTML = html;
for (const el of cached.querySelectorAll("span.i, a[name]"))
el.remove();
}
return cached;
},
set(v) {
cached = v;
},
configurable: true,
enumerable: true
});
for (const sub of node.subproofs) walk(sub);
};
walk(tree);
}
// src/parse-status.ts
function isProofExpression(expr) {
const loc = expr.locations[0];
if (!loc) return false;
const el = loc.node instanceof Element ? loc.node : loc.node.parentElement;
if (!el) return false;
if (el.closest('table[summary="Assertion"]')) return true;
if (el.closest('table[summary^="Hypothes"]')) return true;
const proofTable = el.closest('table[summary="Proof of theorem"]');
if (!proofTable) return false;
const td = el.closest("td");
if (!td) return false;
return [...td.parentElement?.children ?? []].indexOf(td) === 3;
}
function installParseWarning(banner, failureCount) {
if (failureCount === 0) return;
const span = banner.ownerDocument.createElement("span");
span.className = "mm-site-format-parse-warn";
const noun = failureCount === 1 ? "expression" : "expressions";
span.title = `${failureCount} ${noun} could not be parsed`;
span.textContent = " \u26A0";
banner.appendChild(span);
}
// src/view.ts
var PARAM = "view";
var TABLE = "table";
function tableSelected(search) {
return new URLSearchParams(search).get(PARAM) === TABLE;
}
function searchWithView(search, table) {
const params = new URLSearchParams(search);
if (table) params.set(PARAM, TABLE);
else params.delete(PARAM);
const s = params.toString();
return s ? `?${s}` : "";
}
var TOGGLE_CLASS = "mm-site-format-view";
function linkWithView(href, base, table) {
let url;
try {
url = new URL(href, base);
} catch {
return null;
}
if (url.protocol !== "http:" && url.protocol !== "https:") return null;
const host = url.hostname;
if (host !== "metamath.org" && !host.endsWith(".metamath.org")) return null;
if (url.searchParams.get(PARAM) === TABLE === table) return null;
if (table) url.searchParams.set(PARAM, TABLE);
else url.searchParams.delete(PARAM);
return url.href;
}
function applyViewToLinks(table) {
for (const anchor of document.querySelectorAll("a[href]")) {
const a = anchor;
if (a.classList.contains(TOGGLE_CLASS)) continue;
if (a.getAttribute("href")?.startsWith("#")) continue;
const next = linkWithView(a.href, location.href, table);
if (next) a.href = next;
}
}
function versionLine() {
for (const a of document.querySelectorAll("a"))
if (/\bversion\b/i.test(a.textContent ?? "") && a.parentElement)
return a.parentElement;
return null;
}
function installViewToggle(calc, proofTable) {
const grids = [...proofTable.tBodies];
let table = tableSelected(location.search);
const apply = () => {
calc.style.display = table ? "none" : "inline-block";
proofTable.style.border = table ? "" : "none";
for (const grid of grids) {
grid.style.display = table ? "" : "none";
grid.style.visibility = "";
}
};
const here = (forTable) => location.pathname + searchWithView(location.search, forTable) + location.hash;
const link = document.createElement("a");
link.className = TOGGLE_CLASS;
const refresh = () => {
link.textContent = table ? "Calculation version" : "Table version";
link.href = here(!table);
};
const setView = (next, pushHistory) => {
table = next;
apply();
refresh();
if (pushHistory) history.pushState(null, "", here(table));
applyViewToLinks(table);
};
link.addEventListener("click", (event) => {
event.preventDefault();
setView(!table, true);
});
window.addEventListener(
"popstate",
() => setView(tableSelected(location.search), false)
);
const line = versionLine();
if (line) {
line.prepend(link, "\xA0\xA0");
} else {
const box = document.createElement("div");
box.className = `${TOGGLE_CLASS} mm-site-format-view-box`;
box.append(link);
document.body.appendChild(box);
}
apply();
refresh();
}
// src/index.ts
var LOG = "[mm-site-format]";
function makeProofRef(n) {
const synth = document.createElement("span");
const link = document.createElement("a");
link.href = `#mm-site-format-proof-${n}`;
link.textContent = `(${n})`;
link.className = "mm-site-format-proof-ref";
synth.appendChild(link);
return synth;
}
applyViewToLinks(tableSelected(window.location.search));
if (!document.querySelector('table[summary="Proof of theorem"]')) {
console.log(`${LOG} (not a metamath proof page; no processing)`);
} else {
console.log(`${LOG} processing proof page...`);
const _perfStart = DEV_PERF_LOG ? performance.now() : 0;
injectStyles();
const banner = document.createElement("div");
const built = "" ? ` -- built ${""}` : "";
banner.textContent = `MM Site Format ${"0.28.0"} active${built}`;
banner.className = "mm-site-format-banner";
document.body.appendChild(banner);
const proofTable = document.querySelector(
'table[summary="Proof of theorem"]'
);
const proofResult = parseProofTableLazy(document);
const proofTree = proofResult?.tree ?? null;
const stepOf = proofResult?.stepOf ?? /* @__PURE__ */ new Map();
const _tParseTree = DEV_PERF_LOG ? performance.now() : 0;
const grids = proofTable ? [...proofTable.tBodies] : [];
const tableWidth = proofTable ? proofTable.getBoundingClientRect().width : 0;
const tableHeight = proofTable ? proofTable.getBoundingClientRect().height : 0;
if (proofTable) indentProofExpressions(proofTable);
const _tIndent = DEV_PERF_LOG ? performance.now() : 0;
let placeholder = null;
if (proofTree && !tableSelected(window.location.search)) {
for (const grid of grids) grid.style.display = "none";
if (proofTable) {
placeholder = document.createElement("div");
placeholder.className = "mm-site-format-calc";
placeholder.style.width = `${Math.ceil(tableWidth * CALC_WIDTH_FACTOR)}px`;
placeholder.style.maxWidth = "100%";
placeholder.style.height = `${Math.ceil(tableHeight)}px`;
placeholder.style.display = "flex";
placeholder.style.alignItems = "center";
placeholder.style.justifyContent = "center";
placeholder.style.opacity = "0.4";
placeholder.textContent = "\u22EF";
const caption = proofTable.querySelector("caption");
if (caption) caption.appendChild(placeholder);
else proofTable.parentNode?.insertBefore(placeholder, proofTable);
}
}
const restoreGrid = () => {
for (const grid of grids) grid.style.display = "";
placeholder?.remove();
placeholder = null;
};
if (proofTree) materializeExpressions(proofTree);
if (DEV_PERF_LOG) {
const t = performance.now();
console.log(
`[mm-site-format] PERF setup: ${(t - _perfStart).toFixed(0)}ms (parseTable=${(_tParseTree - _perfStart).toFixed(0)}ms indent=${(_tIndent - _tParseTree).toFixed(0)}ms cloneExprs=${(t - _tIndent).toFixed(0)}ms)`
);
}
const choosers = (results) => {
const cache2 = /* @__PURE__ */ new Map();
const exprOf = (node) => {
if (cache2.has(node)) return cache2.get(node);
let found = null;
const cell = node.expressionCell;
if (cell)
for (const r of results) {
const at = r.locations[0]?.node;
if (r.proof && at && cell.contains(at)) {
found = r;
break;
}
}
cache2.set(node, found);
return found;
};
const parseOf = (node) => exprOf(node)?.proof ?? null;
const tokensOf = (node) => exprOf(node)?.tokens.map((t) => t.text) ?? null;
const spineFor = (node, anchor) => {
const conclusion = parseOf(node);
const subs = node.subproofs.map((s) => ({
parse: parseOf(s),
trivial: s.subproofs.length === 0
}));
if (!conclusion || subs.some((s) => !s.parse)) return 0;
const result = chooseSpine(
conclusion,
subs
);
if (result !== null || anchor === null) return result;
return anchorSpine(
anchor,
node.subproofs.map((s) => tokensOf(s))
);
};
const smallFor = (node) => {
if (node.subproofs.length !== 1) return false;
const step = tokensOf(node);
const premise = tokensOf(node.subproofs[0]);
return !!step && !!premise && isSmallStep(step, premise);
};
return { spineFor, smallFor, tokensOf };
};
const sizeToTableWidth = (box) => {
if (!tableWidth) return;
const width = Math.ceil(tableWidth * CALC_WIDTH_FACTOR);
const margin = Math.max(
0,
Math.round(
window.innerWidth - document.body.getBoundingClientRect().width
)
);
box.style.width = `${width}px`;
box.style.maxWidth = `calc(100vw - ${margin}px)`;
};
const calcExprs = [];
let parseNewContent = null;
const diffPainter = createPainter(
"mm-site-format-diff",
"mm-site-format-diff-hl",
DIFF_COLOR
);
const exprFor = diffPainter ? (span) => {
for (const r of calcExprs) {
const at = r.locations[0]?.node;
if (at && span.contains(at)) return r;
}
return null;
} : void 0;
const showCalculation = (results) => {
if (!proofTree || !proofTable) return null;
const _t0 = DEV_PERF_LOG ? performance.now() : 0;
const { spineFor, smallFor, tokensOf: tokensOf_ } = choosers(results);
const _t1 = DEV_PERF_LOG ? performance.now() : 0;
const shared = findSharedNodes(proofTree);
const extracted = [...shared].filter(
(n) => n.subproofs.length > 0 && !n.subproofs.every((s) => s.subproofs.length === 0)
);
const savedRefs = /* @__PURE__ */ new Map();
for (const node of extracted) {
const n = stepOf.get(node);
if (n !== void 0) {
savedRefs.set(node, node.refHtml);
node.refHtml = makeProofRef(n);
}
}
const leafShared = new Set(
[...shared].filter((n) => n.subproofs.length === 0)
);
for (const node of extracted) {
const n = stepOf.get(node);
if (n !== void 0) {
const marker = document.createElement("span");
marker.dataset.proofAnchor = String(n);
marker.style.display = "none";
node.expressionHtml.prepend(marker);
}
}
const calc = proofTreeToCalculation(
proofTree,
spineFor,
smallFor,
tokensOf_,
null,
leafShared,
new Set(extracted)
);
const _t2 = DEV_PERF_LOG ? performance.now() : 0;
const missingSteps = missingCalcRefs(proofTree, stepOf, calc, shared);
if (missingSteps.length > 0) {
console.warn(
`[mm-site-format] calc self-check: steps missing from hints: ${missingSteps.join(", ")}`
);
banner.textContent += ` \u26A0\uFE0F ${missingSteps.length} step(s) missing from calc`;
}
const spineErr = checkSpineValidity(calc);
if (spineErr) {
console.warn(
`[mm-site-format] calc self-check: invalid spine: ${spineErr}`
);
banner.textContent += ` \u26A0\uFE0F invalid spine`;
}
const missingExprs = missingCalcExpressions(
proofTree,
stepOf,
calc,
shared
);
if (missingExprs.length > 0) {
console.warn(
`[mm-site-format] calc self-check: expressions missing: ${missingExprs.join(", ")}`
);
banner.textContent += ` \u26A0\uFE0F ${missingExprs.length} expression(s) missing`;
}
if (DEV_CHECK_SHARED_COVERAGE) {
const sharedMissing = checkSharedSubtreeCoverage(
shared,
stepOf,
spineFor,
smallFor
);
if (sharedMissing.length > 0) {
console.warn(
`[mm-site-format] calc self-check: shared subtree steps missing: ${sharedMissing.join(", ")}`
);
banner.textContent += ` \u26A0\uFE0F ${sharedMissing.length} shared step(s) uncovered`;
}
}
const badRefs = checkRuleRefIntegrity(proofTree, stepOf, calc, shared);
if (badRefs.length > 0) {
console.warn(
`[mm-site-format] calc self-check: rule ref mismatch at steps: ${badRefs.join(", ")}`
);
banner.textContent += ` \u26A0\uFE0F ${badRefs.length} ref mismatch(es)`;
}
const dupes = checkNoDuplicateAppearance(calc, stepOf);
if (dupes.length > 0) {
console.warn(
`[mm-site-format] calc self-check: steps appear both inline and expanded: ${dupes.join(", ")}`
);
banner.textContent += ` \u26A0\uFE0F ${dupes.length} duplicate(s)`;
}
const orphans = checkStepCountConservation(proofTree, stepOf, calc, shared);
if (orphans.length > 0) {
console.warn(
`[mm-site-format] calc self-check: orphan steps: ${orphans.join(", ")}`
);
banner.textContent += ` \u26A0\uFE0F ${orphans.length} orphan(s)`;
}
const onSpine = /* @__PURE__ */ new Set();
{
let t = proofTree;
let anch = null;
while (t.subproofs.length > 0) {
const si = spineFor(t, anch);
if (si === null || si >= t.subproofs.length) break;
anch = tokensOf_(t);
t = t.subproofs[si];
onSpine.add(t);
}
}
const offSpineExtracted = extracted.filter((n) => !onSpine.has(n));
{
let c = calc;
while (c.kind === "step") {
for (const [node, origRef] of savedRefs) {
if (c.inferenceRuleRefHtml === node.refHtml) {
c.inferenceRuleRefHtml = origRef;
break;
}
}
if (c.spine === null) break;
c = c.subcalculations[c.spine];
}
}
for (const [node, ref] of savedRefs) node.refHtml = ref;
let labelNewContent = null;
const renderOpts = {
fetchRuleTooltip,
diffPainter: diffPainter ?? void 0,
exprFor,
onLazyRender: (root) => {
labelNewContent?.(root);
parseNewContent?.(root);
}
};
const rendered = renderCalculation(calc, renderOpts);
const _t3 = DEV_PERF_LOG ? performance.now() : 0;
let _t4 = 0;
for (const node of extracted) {
if (!onSpine.has(node)) continue;
const n = stepOf.get(node);
if (n === void 0) continue;
const marker = rendered.querySelector(`[data-proof-anchor="${n}"]`);
const exprSpan = marker?.parentElement;
const row2 = exprSpan?.closest("tr");
if (row2) {
row2.id = `mm-site-format-proof-${n}`;
const opCell = row2.firstElementChild;
if (opCell && exprSpan) {
opCell.textContent = "";
const ref = makeProofRef(n);
opCell.appendChild(ref);
opCell.style.textAlign = "left";
attachTooltip(ref, () => exprSpan.cloneNode(true));
}
}
}
if (offSpineExtracted.length > 0) {
const box = rendered;
const ordered = [...offSpineExtracted].sort(
(a, b) => (stepOf.get(b) ?? 0) - (stepOf.get(a) ?? 0)
);
for (const node of ordered) {
const n = stepOf.get(node);
const wrapper = document.createElement("div");
wrapper.id = n !== void 0 ? `mm-site-format-proof-${n}` : "";
const label = document.createElement("div");
label.className = "mm-site-format-calc-label";
label.textContent = n !== void 0 ? `Proof of (${n}):` : "Proof:";
wrapper.appendChild(label);
let rendered_ = false;
const renderMiniCalc = () => {
if (rendered_) return;
rendered_ = true;
const others = new Set(shared);
others.delete(node);
const nestedSaved = /* @__PURE__ */ new Map();
for (const other of extracted) {
if (other === node) continue;
const m = stepOf.get(other);
if (m !== void 0) {
nestedSaved.set(other, other.refHtml);
other.refHtml = makeProofRef(m);
}
}
const miniCalc = proofTreeToCalculation(
node,
spineFor,
smallFor,
tokensOf_,
null,
others
);
for (const [other, ref] of nestedSaved) other.refHtml = ref;
wrapper.appendChild(renderCalcTable(miniCalc, renderOpts));
labelNewContent?.(wrapper);
parseNewContent?.(wrapper);
};
wrapper.__renderMiniCalc = renderMiniCalc;
wrapper.style.display = "none";
box.appendChild(wrapper);
}
_t4 = DEV_PERF_LOG ? performance.now() : 0;
box.addEventListener("click", (e) => {
const link = e.target.closest?.(
'a[href^="#mm-site-format-proof-"]'
);
if (!link) return;
const id = link.getAttribute("href").slice(1);
const target = document.getElementById(id);
if (target && target.style.display === "none") {
const lazy = target;
lazy.__renderMiniCalc?.();
target.style.display = "";
}
});
const miniCalcIds = ordered.map((node) => stepOf.get(node)).filter((n) => n !== void 0).map((n) => `mm-site-format-proof-${n}`);
const updateMiniCalcVisibility = () => {
for (const id of miniCalcIds) {
const wrapper = document.getElementById(id);
if (!wrapper) continue;
const links = box.querySelectorAll(`a[href="#${id}"]`);
let anyVisible = false;
for (const link of links) {
let el = link;
let hidden = false;
while (el && el !== box) {
if (el.style.display === "none") {
hidden = true;
break;
}
el = el.parentElement;
}
if (!hidden) {
anyVisible = true;
break;
}
}
const desired = anyVisible ? "" : "none";
if (wrapper.style.display !== desired) {
if (desired === "") {
const lazy = wrapper;
lazy.__renderMiniCalc?.();
}
wrapper.style.display = desired;
}
}
};
updateMiniCalcVisibility();
const observer = new MutationObserver(updateMiniCalcVisibility);
observer.observe(box, {
attributes: true,
attributeFilter: ["style"],
subtree: true
});
const anchorById = /* @__PURE__ */ new Map();
for (const el of box.querySelectorAll("[id^='mm-site-format-proof-']"))
anchorById.set(el.id, el);
const labelProofRefs = (root) => {
for (const link of root.querySelectorAll(
"a.mm-site-format-proof-ref"
)) {
const id = link.getAttribute("href")?.slice(1);
if (!id) continue;
const target = anchorById.get(id) ?? document.getElementById(id);
if (!target) continue;
if (target.contains(link)) continue;
const pos = link.compareDocumentPosition(target);
const dir = pos & Node.DOCUMENT_POSITION_FOLLOWING ? "below" : "above";
const n = id.replace("mm-site-format-proof-", "");
link.textContent = `(${n}) ${dir}`;
}
};
labelProofRefs(box);
labelNewContent = labelProofRefs;
}
const caption = proofTable.querySelector("caption");
placeholder?.remove();
placeholder = null;
if (caption) caption.appendChild(rendered);
else proofTable.parentNode?.insertBefore(rendered, proofTable);
installViewToggle(rendered, proofTable);
if (DEV_PERF_LOG)
console.log(
`[mm-site-format] PERF showCalculation: choosers=${(_t1 - _t0).toFixed(0)}ms proofTreeToCalc=${(_t2 - _t1).toFixed(0)}ms renderMain=${(_t3 - _t2).toFixed(0)}ms miniCalcs=${((_t4 || _t3) - _t3).toFixed(0)}ms postProcess=${(performance.now() - (_t4 || _t3)).toFixed(0)}ms total=${(performance.now() - _t0).toFixed(0)}ms`
);
return rendered;
};
const pageUrl = window.location.href;
const fetchCache = /* @__PURE__ */ new Map();
const fetcher = (url) => {
let body = fetchCache.get(url);
if (!body) {
body = fetch(url).then((r) => r.text());
fetchCache.set(url, body);
}
return body;
};
const fetchRuleTooltip = makeRuleTooltipFetcher(pageUrl, fetcher);
attachRuleTooltipsToPage(document, fetchRuleTooltip);
let store = null;
try {
store = window.sessionStorage;
} catch {
store = null;
}
const cache = createCache(store, GRAMMAR_CACHE_VERSION);
const declaredHints = new Set(
extractSyntaxHintUrls(document, pageUrl).map(
(u) => (u.split("/").pop() ?? "").replace(/\.html$/, "")
)
);
const finish = (install) => (results) => {
const failures = results.filter((r) => !r.proof && isProofExpression(r));
for (const { tokens } of failures)
console.warn(`${LOG} could not parse:`, formatTokens(tokens));
const proofs = results.map((r) => r.proof).filter((p) => p !== null);
const missing = missingSyntaxHints(proofs, declaredHints);
if (missing.length)
console.info(
`${LOG} incomplete Syntax hints -- shown but not listed: ${missing.join(", ")}`
);
installParseWarning(banner, failures.length);
install(results);
};
if (findMathSpans(document).length > 0) {
const occIndex = /* @__PURE__ */ new Map();
const addToIndex = (exprs) => {
const partial = buildOccurrenceIndex(exprs);
for (const [key, occs] of partial) {
const existing = occIndex.get(key);
if (existing) existing.push(...occs);
else occIndex.set(key, [...occs]);
}
};
const highlighter = createHighlighter();
parseUniExpressions(document, pageUrl, fetcher, document, cache).then((results) => {
const _tParsed = DEV_PERF_LOG ? performance.now() : 0;
addToIndex(results);
if (DEV_PERF_LOG) console.log(`[mm-site-format] PERF addToIndex done`);
finish((r) => installHover(r, occIndex, highlighter))(results);
if (DEV_PERF_LOG)
console.log(`[mm-site-format] PERF finish+installHover done`);
const _tHover = DEV_PERF_LOG ? performance.now() : 0;
if (DEV_PERF_LOG)
console.log(`[mm-site-format] PERF calling showCalculation...`);
const calc = showCalculation(results);
if (DEV_PERF_LOG) {
const t = performance.now();
console.log(
`[mm-site-format] PERF post-parse: index+hover=${(_tHover - _tParsed).toFixed(0)}ms showCalculation=${(t - _tHover).toFixed(0)}ms`
);
}
if (calc)
parseUniExpressions(document, pageUrl, fetcher, calc, cache).then(
(calcResults) => {
const _tCalc = DEV_PERF_LOG ? performance.now() : 0;
addToIndex(calcResults);
calcExprs.push(...calcResults);
installHover(calcResults, occIndex, highlighter);
sizeToTableWidth(calc);
parseNewContent = async (root) => {
const r = await parseUniExpressions(
document,
pageUrl,
fetcher,
root,
cache
);
addToIndex(r);
calcExprs.push(...r);
installHover(r, occIndex, highlighter);
};
if (DEV_PERF_LOG)
console.log(
`[mm-site-format] PERF calc pass: ${(performance.now() - _tCalc).toFixed(0)}ms (total since parse: ${(performance.now() - _tParsed).toFixed(0)}ms)`
);
console.log(`${LOG} finished`);
}
);
else console.log(`${LOG} finished`);
}).catch(restoreGrid);
} else {
const occIndex = /* @__PURE__ */ new Map();
const addToIndex = (exprs) => {
const partial = buildOccurrenceIndex(exprs);
for (const [key, occs] of partial) {
const existing = occIndex.get(key);
if (existing) existing.push(...occs);
else occIndex.set(key, [...occs]);
}
};
const highlighter = createHighlighter();
const imagesReady = (imgs) => Promise.all(
imgs.map(
(img) => img.complete ? Promise.resolve() : new Promise((resolve) => {
img.addEventListener("load", () => resolve(), { once: true });
img.addEventListener("error", () => resolve(), { once: true });
})
)
);
const gifImages = (root) => [...root.querySelectorAll("img")];
imagesReady(gifImages(document)).then(
() => parseGifExpressions(
document,
pageUrl,
fetcher,
canvasSampler,
document,
cache
)
).then((results) => {
const _tParsed = DEV_PERF_LOG ? performance.now() : 0;
addToIndex(results);
finish((r) => installHover(r, occIndex, highlighter))(results);
const _tHover = DEV_PERF_LOG ? performance.now() : 0;
const calc = showCalculation(results);
if (DEV_PERF_LOG) {
const t = performance.now();
console.log(
`[mm-site-format] PERF post-parse (GIF): index+hover=${(_tHover - _tParsed).toFixed(0)}ms showCalculation=${(t - _tHover).toFixed(0)}ms`
);
}
if (calc)
imagesReady(gifImages(calc)).then(
() => parseGifExpressions(
document,
pageUrl,
fetcher,
canvasSampler,
calc,
cache
)
).then((calcResults) => {
const _tCalc = DEV_PERF_LOG ? performance.now() : 0;
addToIndex(calcResults);
calcExprs.push(...calcResults);
installHover(calcResults, occIndex, highlighter);
sizeToTableWidth(calc);
parseNewContent = async (root) => {
await imagesReady(gifImages(root));
const r = await parseGifExpressions(
document,
pageUrl,
fetcher,
canvasSampler,
root,
cache
);
addToIndex(r);
calcExprs.push(...r);
installHover(r, occIndex, highlighter);
};
if (DEV_PERF_LOG)
console.log(
`[mm-site-format] PERF calc pass (GIF): ${(performance.now() - _tCalc).toFixed(0)}ms (total since parse: ${(performance.now() - _tParsed).toFixed(0)}ms)`
);
console.log(`${LOG} finished`);
});
else console.log(`${LOG} finished`);
}).catch(restoreGrid);
}
}
})();