diff --git a/web/root/index.html b/web/root/index.html index a6ff319..ca07724 100644 --- a/web/root/index.html +++ b/web/root/index.html @@ -26,7 +26,54 @@
-
+
+ +
+
+ + + + + + + + + + + + + + +
+
+
+
+
+ +
+ + + + +
+ +
@@ -56,7 +103,7 @@
- +
@@ -88,52 +135,11 @@
- - -
- -
-
- - - - - - - - - - - - -
-
+
-
-
-
- -
-
diff --git a/web/root/src/highlight.ts b/web/root/src/highlight.ts index 0c01cab..6864ddc 100644 --- a/web/root/src/highlight.ts +++ b/web/root/src/highlight.ts @@ -109,7 +109,35 @@ bus.on("highlight/all/remove", (_) => { } }); +globalThis.document.addEventListener("mouseover", (e) => { + const target = (e.target instanceof Element) + ? e.target.closest("[highlight-span]") + : null; -export function highlightable(span: Span, text: string): string{ - return `${text}` + if (!target) return; + + const kind = (target.getAttribute("highlight-kind") ?? "focus") as unknown as HighlightKind; + const span = target.getAttribute("highlight-span")!.split(":").map(Number) as unknown as Span; + + bus.emit("highlight/one/add", {span, kind}); +}); + +document.addEventListener("mouseout", (e) => { + if (!(e.target instanceof Element)) return; + + const from = e.target.closest("[highlight-span]"); + const to = e.relatedTarget instanceof Element + ? e.relatedTarget.closest("[highlight-span]") + : null; + + if (!from || from === to) return; + + const kind = (from.getAttribute("highlight-kind") ?? "focus") as unknown as HighlightKind; + const span = from.getAttribute("highlight-span")!.split(":").map(Number) as unknown as Span; + + bus.emit("highlight/one/remove", {span, kind}); +}); + +export function highlightable(span: Span, text: string, kind?: HighlightKind): string{ + return `${text}` } \ No newline at end of file diff --git a/web/root/src/paths.ts b/web/root/src/paths.ts index 26a4e30..39a3e20 100644 --- a/web/root/src/paths.ts +++ b/web/root/src/paths.ts @@ -30,9 +30,9 @@ function renderFaPath(state: FaState, index: number) { const step = state.path[i]; div.innerHTML = `${i + 1}. ` - + highlightable(step.function, `${DELTA}(${step.from_state})`) + + highlightable(step.function, `${DELTA}(${step.from_state})`, "focus") + " = " - + highlightable(step.transition, step.state); + + highlightable(step.transition, step.state, "warning"); steps.appendChild(div); } @@ -63,9 +63,9 @@ function renderPdaPath(state: PdaState, index: number) { const step = state.path[i]; div.innerHTML = `${i + 1}. ` - + highlightable(step.function, `${DELTA}(${step.from_state}, ${step.from_letter}, , ${step.from_stack})`) + + highlightable(step.function, `${DELTA}(${step.from_state}, ${step.from_letter}, , ${step.from_stack})`, "focus") + " = " - + highlightable(step.transition, `(${step.state}, [ ${step.stack.join(" ")} ])`); + + highlightable(step.transition, `(${step.state}, [ ${step.stack.join(" ")} ])`, "warning"); steps.appendChild(div); } @@ -97,9 +97,9 @@ function renderTmPath(state: TmState, index: number) { div.setAttribute("highlight-span", "${}") div.innerHTML = `${i + 1}. ` - + highlightable(step.function, `${DELTA}(${step.from_state}, ${step.from_symbol})`) + + highlightable(step.function, `${DELTA}(${step.from_state}, ${step.from_symbol})`, "focus") + " = " - + highlightable(step.transition, `(${step.state}, ${step.symbol}, ${step.direction})`); + + highlightable(step.transition, `(${step.state}, ${step.symbol}, ${step.direction})`, "warning"); console.log(div.innerHTML); steps.appendChild(div); } diff --git a/web/root/src/splitters.ts b/web/root/src/splitters.ts index d6a0e88..058c938 100644 --- a/web/root/src/splitters.ts +++ b/web/root/src/splitters.ts @@ -91,13 +91,14 @@ function enableFlexSplitters() { // --split-min-a: 80px // --split-min-b: 180px const defPct = getVarPct(splitter, "--split-default", 60); - const minA = getVarPx(splitter, "--split-min-a", 80); - const minB = getVarPx(splitter, "--split-min-b", 180); + const minA = getVarPx(splitter, "--split-min-a", 220); + const minB = getVarPx(splitter, "--split-min-b", 220); // Set initial size (A is fixed) { const r = parent.getBoundingClientRect(); const px = clamp((defPct / 100) * r.height, minA, r.height - gap - minB); + console.log(r.height, px) setFixedSize(a, "y", px); } @@ -199,4 +200,5 @@ function enableFlexSplitters() { }); } } +enableFlexSplitters(); enableFlexSplitters(); \ No newline at end of file