diff options
Diffstat (limited to 'graph/web')
| -rw-r--r-- | graph/web/index.html | 7 | ||||
| -rw-r--r-- | graph/web/render.js | 39 | ||||
| -rw-r--r-- | graph/web/viewer.js | 17 |
3 files changed, 60 insertions, 3 deletions
diff --git a/graph/web/index.html b/graph/web/index.html index 1badd8e1..f91f1710 100644 --- a/graph/web/index.html +++ b/graph/web/index.html @@ -13,7 +13,7 @@ #graph { min-height:0; overflow:hidden; position:relative; background:#fafbfc; } #elk, #dot { width:100%; height:100%; } #graph svg { display:block; } - .tools { display:flex; align-items:center; gap:14px; margin-top:8px; font-size:12px; } + .tools { display:flex; flex-wrap:wrap; align-items:center; gap:14px; margin-top:8px; font-size:12px; } .hint { color:#616c78; } .ctrl { color:#b63838; } .mem { color:#2867b2; } .data { color:#536477; } .edge { fill:none; stroke-width:1.5; } @@ -22,6 +22,8 @@ .edge.selected { stroke-width:3.5; } .node { cursor:pointer; } .box { stroke:#758191; stroke-width:1; } + .node.near .box { stroke:#c18221; stroke-width:2; } + .node.focus .box { stroke:#9c4900; stroke-width:3; } .node.selected .box { stroke:#1569b9; stroke-width:3; } .head { font-size:10px; fill:#596674; } .label { font-size:12px; fill:#152330; font-weight:600; } @@ -51,10 +53,13 @@ <div id="status" role="status">Connecting to compiler...</div> <div class="tools"> <button id="fit" type="button" disabled>Fit</button> + <button id="save" type="button" disabled>Save SVG</button> <label><input id="assocs" type="checkbox"> Associations</label> + <label><input id="near" type="checkbox" checked> Peep neighborhood</label> <span class="ctrl">Control</span><span class="data">Data</span><span class="mem">Memory</span> <span class="hint">Scroll to zoom · drag to pan · click a node for details</span> </div> + <div id="event" class="hint" role="status"></div> </div> <div id="graph"><div id="elk"></div><div id="dot" hidden></div><pre id="detail" hidden></pre></div> <div class="controls"> diff --git a/graph/web/render.js b/graph/web/render.js index b488ed0e..76cf8c06 100644 --- a/graph/web/render.js +++ b/graph/web/render.js @@ -30,7 +30,7 @@ class GraphView { this.resize.observe(host); } - show(snap, scene) { + show(snap, scene, evt) { if (this.comp !== snap.comp) { this.comp = snap.comp; this.pick = 0; @@ -39,6 +39,7 @@ class GraphView { this.links.selectAll("*").remove(); } this.scene = scene; + this.evt = evt; this.links.selectAll("path.edge").data(scene.edges, e => e.id).join("path") .attr("class", e => "edge " + e.role).attr("id", e => e.id) .attr("d", e => e.path).attr("stroke", e => this.colors[e.role]) @@ -78,6 +79,7 @@ class GraphView { .attr("text-anchor", "middle").text((p, j) => n.n.edges[j].idx); }); this.assocs(document.getElementById("assocs").checked); + this.mark(); this.select(this.pick); if (this.auto) this.fit(); } @@ -100,6 +102,41 @@ class GraphView { assocs(show) { this.links.selectAll(".ASSOC").style("display", show ? null : "none"); } + mark() { + const evt = this.evt; + const show = document.getElementById("near").checked; + const near = new Set(show ? evt?.near : []); + this.nodes.selectAll("g.node").classed("near", n => near.has(n.n.id)) + .classed("focus", n => show && (n.n.id === evt?.node || n.n.id === evt?.repl)); + } + + // Save the whole graph at its layout size, independent of pan/zoom. + save(step) { + const svg = this.svg.node().cloneNode(true); + svg.setAttribute("xmlns", "http://www.w3.org/2000/svg"); + svg.setAttribute("width", this.scene.width); + svg.setAttribute("height", this.scene.height); + svg.setAttribute("viewBox", `0 0 ${this.scene.width} ${this.scene.height}`); + svg.style.fontFamily = getComputedStyle(this.host).fontFamily; + svg.querySelector("g").removeAttribute("transform"); + // Keep styles, markers and labels in the file; no viewer assets are needed. + const style = document.createElementNS(svg.namespaceURI, "style"); + style.textContent = document.querySelector("style").textContent; + svg.prepend(style); + const bg = document.createElementNS(svg.namespaceURI, "rect"); + bg.setAttribute("width", "100%"); bg.setAttribute("height", "100%"); + bg.setAttribute("fill", getComputedStyle(this.host.parentElement).backgroundColor); + svg.insertBefore(bg, svg.querySelector("g")); + const blob = new Blob([new XMLSerializer().serializeToString(svg)], {type: "image/svg+xml"}); + const url = URL.createObjectURL(blob); + const link = document.createElement("a"); + link.href = url; link.download = `simple-${step}.svg`; + document.body.append(link); + link.click(); + link.remove(); + setTimeout(() => URL.revokeObjectURL(url), 1000); + } + fit() { if (!this.scene || !this.host.clientWidth || !this.host.clientHeight) return; const w = this.host.clientWidth, h = this.host.clientHeight; diff --git a/graph/web/viewer.js b/graph/web/viewer.js index e193a4b3..9aaaa154 100644 --- a/graph/web/viewer.js +++ b/graph/web/viewer.js @@ -28,7 +28,20 @@ function updateUI() { document.getElementById("compile").disabled = !socket || socket.readyState !== WebSocket.OPEN || compiling || rendering; document.getElementById("fit").disabled = rendering || current < 0; + document.getElementById("save").disabled = rendering || !frames[current]?.snap; document.getElementById("assocs").disabled = !frames[current]?.snap; + document.getElementById("near").disabled = !frames[current]?.evt; + const evt = frames[current]?.evt; + let label = ""; + if (evt) { + const text = evt.kind === "PHASE" ? "Phase complete" : + evt.kind === "BEFORE" ? `Before peephole #${evt.peep} at node #${evt.node}` : + evt.kind === "RETURN" ? `Return #${evt.repl} for #${evt.node}` : + !evt.repl ? `Removed #${evt.node}` : evt.repl === evt.node ? `Updated #${evt.node}` : + `Replaced #${evt.node} with #${evt.repl}`; + label = `${evt.phase} · ${text}${evt.up ? " (inside peephole #" + evt.up + ")" : ""}`; + } + document.getElementById("event").textContent = label; } function reportError(error) { @@ -75,7 +88,7 @@ async function render(index) { if (frame.snap) { if (!layout) layout = new GraphLayout(); if (!frame.layout) frame.layout = await layout.run(frame.snap); - if (generation === frameGeneration) renderer.show(frame.snap, frame.layout); + if (generation === frameGeneration) renderer.show(frame.snap, frame.layout, frame.evt); } else { document.getElementById("detail").hidden = true; await drawDot(frame.dot); @@ -108,6 +121,8 @@ document.getElementById("fit").addEventListener("click", () => { else render(current); }); document.getElementById("assocs").addEventListener("change", event => renderer.assocs(event.target.checked)); +document.getElementById("near").addEventListener("change", () => renderer.mark()); +document.getElementById("save").addEventListener("click", () => renderer.save(frames[current].snap.step)); document.addEventListener("keydown", event => { if (event.key === "Escape") renderer.select(0); }); |