mirror of
https://github.com/ParkerTenBroeck/automata.git
synced 2026-06-07 05:28:45 -04:00
sync
This commit is contained in:
Parker TenBroeck
parent
f1b8c08e8f
commit
7971c61c74
15 changed files with 41485 additions and 252 deletions
|
|
@ -8,44 +8,45 @@ import { oneDark } from "https://esm.sh/@codemirror/theme-one-dark";
|
|||
|
||||
import wasm from "./wasm.js"
|
||||
|
||||
import * as vis from "./js/vis-network.js"
|
||||
|
||||
|
||||
function tokenize(text) {
|
||||
try{
|
||||
return wasm.lex(text);
|
||||
}catch(e){
|
||||
console.log(e)
|
||||
return []
|
||||
}
|
||||
try {
|
||||
return wasm.lex(text);
|
||||
} catch (e) {
|
||||
console.log(e)
|
||||
return []
|
||||
}
|
||||
}
|
||||
|
||||
function compile(text) {
|
||||
try{
|
||||
return wasm.compile(text);
|
||||
}catch(e){
|
||||
console.log(e)
|
||||
return []
|
||||
try {
|
||||
return wasm.compile(text);
|
||||
} catch (e) {
|
||||
console.log(e)
|
||||
return []
|
||||
}
|
||||
}
|
||||
/* ===================================================================== */
|
||||
|
||||
// Map token types -> CSS classes
|
||||
const tokenClass = (t) =>
|
||||
({
|
||||
comment: "tok-comment",
|
||||
keyword: "tok-keyword",
|
||||
error: "tok-error",
|
||||
ident: "tok-ident",
|
||||
punc: "tok-punc",
|
||||
string: "tok-string",
|
||||
lpar: "rb-",
|
||||
lbrace: "rb-",
|
||||
lbracket: "rb-",
|
||||
({
|
||||
comment: "tok-comment",
|
||||
keyword: "tok-keyword",
|
||||
error: "tok-error",
|
||||
ident: "tok-ident",
|
||||
punc: "tok-punc",
|
||||
string: "tok-string",
|
||||
lpar: "rb-",
|
||||
lbrace: "rb-",
|
||||
lbracket: "rb-",
|
||||
|
||||
rpar: "rb-",
|
||||
rbrace: "rb-",
|
||||
rbracket: "rb-",
|
||||
}[t] || "tok-ident");
|
||||
|
||||
rpar: "rb-",
|
||||
rbrace: "rb-",
|
||||
rbracket: "rb-",
|
||||
}[t] || "tok-ident");
|
||||
|
||||
// ===================== Diagnostics helpers =====================
|
||||
function severityClass(sev) {
|
||||
const s = (sev || "error").toLowerCase();
|
||||
if (s === "warning") return "cm-diag-warning";
|
||||
|
|
@ -57,21 +58,11 @@ function sevRank(sev) {
|
|||
if (sev === "warning") return 2;
|
||||
return 1;
|
||||
}
|
||||
function sevLabel(sev) {
|
||||
if (sev === "warning") return "warning";
|
||||
if (sev === "info") return "info";
|
||||
return "error";
|
||||
}
|
||||
function sevAnsiColorClass(sev) {
|
||||
if (sev === "warning") return "ansi-yellow";
|
||||
if (sev === "info") return "ansi-cyan";
|
||||
return "ansi-red";
|
||||
}
|
||||
|
||||
|
||||
function buildAnalysis(text, doc) {
|
||||
const tokens = tokenize(text);
|
||||
const {log, log_formatted} = compile(text);
|
||||
const { log, log_formatted } = compile(text);
|
||||
|
||||
// Build ONE Decoration set: syntax + diagnostics
|
||||
const marks = [];
|
||||
|
|
@ -81,8 +72,8 @@ function buildAnalysis(text, doc) {
|
|||
const start = Math.max(0, Math.min(docLen, tok.start));
|
||||
const end = Math.max(start, Math.min(docLen, tok.end));
|
||||
var tc = tokenClass(tok.kind);
|
||||
if (tc === "rb-"){
|
||||
tc += tok.scope_level.toString();
|
||||
if (tc === "rb-") {
|
||||
tc += tok.scope_level.toString();
|
||||
}
|
||||
if (end > start) {
|
||||
marks.push(Decoration.mark({ class: tc }).range(start, end));
|
||||
|
|
@ -90,7 +81,7 @@ function buildAnalysis(text, doc) {
|
|||
}
|
||||
|
||||
for (const d of log) {
|
||||
if (d.start === undefined || d.end === undefined)continue;
|
||||
if (d.start === undefined || d.end === undefined) continue;
|
||||
const start = Math.max(0, Math.min(docLen, d.start));
|
||||
const endRaw = d.end == null ? d.start : d.end;
|
||||
const end = Math.max(start, Math.min(docLen, endRaw));
|
||||
|
|
@ -238,7 +229,7 @@ function formatTerminal(view) {
|
|||
let s = "";
|
||||
s += `\x1b[90m[compile]\x1b[0m ${log.length} diagnostics\n`;
|
||||
|
||||
term.innerHTML = ansiToHtml(s+log_formatted);
|
||||
term.innerHTML = ansiToHtml(s + log_formatted);
|
||||
}
|
||||
|
||||
const terminalPlugin = ViewPlugin.fromClass(
|
||||
|
|
@ -253,8 +244,8 @@ const terminalPlugin = ViewPlugin.fromClass(
|
|||
}
|
||||
);
|
||||
|
||||
// ===================== Build editor =====================
|
||||
const initialText = `machine=NPDA
|
||||
|
||||
const initialText = `type=NPDA
|
||||
Q = {q0, q1} // states
|
||||
E = {a, b} // alphabet
|
||||
T = {z0, A, B} // stack
|
||||
|
|
@ -325,45 +316,24 @@ setDefaultLayoutWeights();
|
|||
const app = document.getElementById("app");
|
||||
const hSplit = document.getElementById("hSplit");
|
||||
const vSplit = document.getElementById("vSplit");
|
||||
const canvas = document.getElementById("canvas");
|
||||
// const canvas = document.getElementById("canvas");
|
||||
const canvasPane = document.getElementById("canvasPane");
|
||||
|
||||
let draggingH = false;
|
||||
let draggingV = false;
|
||||
|
||||
// --- Canvas height splitter ---
|
||||
hSplit.addEventListener("mousedown", (e) => {
|
||||
draggingH = true;
|
||||
document.body.style.cursor = "row-resize";
|
||||
e.preventDefault();
|
||||
});
|
||||
|
||||
// --- Terminal/editor width splitter ---
|
||||
vSplit.addEventListener("mousedown", (e) => {
|
||||
draggingV = true;
|
||||
document.body.style.cursor = "col-resize";
|
||||
e.preventDefault();
|
||||
});
|
||||
|
||||
function resizeCanvasToPane() {
|
||||
// Keep canvas resolution in sync with CSS size (crisp rendering)
|
||||
const rect = canvasPane.getBoundingClientRect();
|
||||
const dpr = window.devicePixelRatio || 1;
|
||||
const w = Math.max(1, Math.floor(rect.width * dpr));
|
||||
const h = Math.max(1, Math.floor(rect.height * dpr));
|
||||
if (canvas.width !== w) canvas.width = w;
|
||||
if (canvas.height !== h) canvas.height = h;
|
||||
|
||||
// Optional: demo draw
|
||||
const ctx = canvas.getContext("2d");
|
||||
ctx.clearRect(0, 0, canvas.width, canvas.height);
|
||||
ctx.fillStyle = "#1f6feb";
|
||||
ctx.fillRect(20 * dpr, 20 * dpr, 140 * dpr, 60 * dpr);
|
||||
ctx.fillStyle = "#c9d1d9";
|
||||
ctx.font = `${14 * dpr}px ui-monospace, monospace`;
|
||||
ctx.fillText("Canvas area", 30 * dpr, 55 * dpr);
|
||||
}
|
||||
|
||||
window.addEventListener("mousemove", (e) => {
|
||||
const rect = app.getBoundingClientRect();
|
||||
|
||||
|
|
@ -374,7 +344,6 @@ setDefaultLayoutWeights();
|
|||
const maxCanvas = rect.height - 8 - minBottom;
|
||||
const canvasH = Math.max(minCanvas, Math.min(maxCanvas, y));
|
||||
app.style.setProperty("--canvasH", `${canvasH}px`);
|
||||
resizeCanvasToPane();
|
||||
}
|
||||
|
||||
if (draggingV) {
|
||||
|
|
@ -383,7 +352,7 @@ setDefaultLayoutWeights();
|
|||
const x = e.clientX - r.left;
|
||||
const minTerm = 220;
|
||||
const maxTerm = r.width - 8 - 220;
|
||||
const termW = Math.max(minTerm, Math.min(maxTerm, r.width-x));
|
||||
const termW = Math.max(minTerm, Math.min(maxTerm, r.width - x));
|
||||
app.style.setProperty("--termW", `${termW}px`);
|
||||
}
|
||||
});
|
||||
|
|
@ -393,8 +362,251 @@ setDefaultLayoutWeights();
|
|||
draggingV = false;
|
||||
document.body.style.cursor = "";
|
||||
});
|
||||
})();
|
||||
|
||||
// Keep canvas crisp on window resize too
|
||||
window.addEventListener("resize", resizeCanvasToPane);
|
||||
resizeCanvasToPane();
|
||||
})();
|
||||
let network = null;
|
||||
const nodes = new vis.DataSet();
|
||||
const edges = new vis.DataSet();
|
||||
|
||||
|
||||
const automaton = {
|
||||
states: ["q0", "q1"],
|
||||
initialState: "q0",
|
||||
acceptStates: ["q1"],
|
||||
|
||||
transitions: [
|
||||
{
|
||||
from: "q0",
|
||||
to: "q0",
|
||||
label: "ε, z0 → A z0\n"
|
||||
},
|
||||
{
|
||||
from: "q0",
|
||||
to: "q0",
|
||||
label: "ε, z0 → B z0"
|
||||
},
|
||||
{
|
||||
from: "q0",
|
||||
to: "q1",
|
||||
label: "ε, z0 → z0"
|
||||
},
|
||||
{
|
||||
from: "q1",
|
||||
to: "q1",
|
||||
label: "a, A → ε"
|
||||
},
|
||||
{
|
||||
from: "q1",
|
||||
to: "q1",
|
||||
label: "b, B → ε"
|
||||
}
|
||||
]
|
||||
};
|
||||
|
||||
/**@param {{ctx: CanvasRenderingContext2D}} */
|
||||
function renderNode({
|
||||
ctx,
|
||||
id,
|
||||
x,
|
||||
y,
|
||||
state: { selected, hover },
|
||||
style,
|
||||
label,
|
||||
}) {
|
||||
return {
|
||||
drawNode() {
|
||||
ctx.save();
|
||||
var r = style.size;
|
||||
|
||||
|
||||
ctx.beginPath();
|
||||
ctx.arc(x, y, r, 0, 2 * Math.PI);
|
||||
ctx.fillStyle = "red";
|
||||
ctx.fill();
|
||||
ctx.lineWidth = 4;
|
||||
ctx.strokeStyle = "blue";
|
||||
ctx.stroke();
|
||||
|
||||
ctx.fillStyle = "black";
|
||||
ctx.textAlign = 'center';
|
||||
ctx.fillText(label, x, y, r);
|
||||
|
||||
|
||||
ctx.textAlign = 'center';
|
||||
ctx.strokeStyle = 'white';
|
||||
ctx.fillStyle = "black";
|
||||
let cy = y - (r + 10);
|
||||
for (const part of "meow[]\nbeeep".split("\n").reverse()) {
|
||||
const metrics = ctx.measureText(part);
|
||||
cy -= metrics.actualBoundingBoxAscent + metrics.actualBoundingBoxDescent;
|
||||
ctx.strokeText(part, x, cy);
|
||||
ctx.fillText(part, x, cy);
|
||||
}
|
||||
|
||||
|
||||
ctx.restore();
|
||||
},
|
||||
nodeDimensions: { width: 20, height: 20 },
|
||||
};
|
||||
}
|
||||
|
||||
|
||||
// Populate nodes
|
||||
for (const state of automaton.states) {
|
||||
nodes.add({
|
||||
id: state,
|
||||
label: state,
|
||||
});
|
||||
}
|
||||
|
||||
// Populate edges
|
||||
automaton.transitions.forEach((t, i) => {
|
||||
edges.add({
|
||||
id: `e${i}`,
|
||||
from: t.from,
|
||||
to: t.to,
|
||||
label: t.label
|
||||
});
|
||||
});
|
||||
|
||||
// updateGraphFromText();
|
||||
ensureGraph();
|
||||
function updateGraphFromText() {
|
||||
ensureGraph();
|
||||
|
||||
const trans = []
|
||||
|
||||
// Collect state ids
|
||||
const stateSet = new Set();
|
||||
for (const tr of trans) {
|
||||
stateSet.add(tr.from);
|
||||
stateSet.add(tr.to);
|
||||
}
|
||||
|
||||
// Update nodes (add missing, remove stale)
|
||||
const existingNodeIds = new Set(nodes.getIds());
|
||||
const desiredNodeIds = new Set([...stateSet]);
|
||||
|
||||
// remove stale
|
||||
for (const id of existingNodeIds) {
|
||||
if (!desiredNodeIds.has(id)) nodes.remove(id);
|
||||
}
|
||||
// add/update desired
|
||||
for (const id of desiredNodeIds) {
|
||||
const pos = pinnedPositions.get(id);
|
||||
if (!existingNodeIds.has(id)) {
|
||||
nodes.add({
|
||||
id,
|
||||
label: id,
|
||||
...(pos ? { x: pos.x, y: pos.y, fixed: true } : {})
|
||||
});
|
||||
} else if (pos) {
|
||||
nodes.update({ id, x: pos.x, y: pos.y, fixed: true });
|
||||
}
|
||||
}
|
||||
|
||||
// Update edges (stable IDs so edits don't flicker)
|
||||
const desiredEdgeIds = new Set();
|
||||
const nextEdges = [];
|
||||
|
||||
for (let i = 0; i < trans.length; i++) {
|
||||
const tr = trans[i];
|
||||
const id = `${tr.from}::${tr.to}::${tr.label}::${i}`;
|
||||
desiredEdgeIds.add(id);
|
||||
nextEdges.push({ id, from: tr.from, to: tr.to, label: tr.label });
|
||||
}
|
||||
|
||||
const existingEdgeIds = new Set(edges.getIds());
|
||||
for (const id of existingEdgeIds) {
|
||||
if (!desiredEdgeIds.has(id)) edges.remove(id);
|
||||
}
|
||||
// add/update in batch
|
||||
for (const e of nextEdges) {
|
||||
if (!existingEdgeIds.has(e.id)) edges.add(e);
|
||||
else edges.update(e);
|
||||
}
|
||||
|
||||
// If positions exist for all nodes, we can disable physics to “respect” manual layout
|
||||
// Otherwise leave physics on to auto-layout new nodes.
|
||||
const allPinned = [...desiredNodeIds].every((id) => pinnedPositions.has(id));
|
||||
network.setOptions({ physics: { enabled: !allPinned } });
|
||||
|
||||
// Redraw nicely after updates
|
||||
network.fit({ animation: { duration: 200, easingFunction: "easeInOutQuad" } });
|
||||
}
|
||||
|
||||
// ---------- 4) Hook graph updates into your existing single-pass analysis ----------
|
||||
const graphPlugin = ViewPlugin.fromClass(class {
|
||||
constructor(view) {
|
||||
updateGraphFromText(view.state.doc.toString());
|
||||
}
|
||||
update(update) {
|
||||
if (update.docChanged) {
|
||||
updateGraphFromText(update.state.doc.toString());
|
||||
}
|
||||
}
|
||||
});
|
||||
|
||||
function chosen_node(values, id, selected, hovering) {
|
||||
|
||||
console.log(values, id, selected, hovering)
|
||||
}
|
||||
|
||||
function ensureGraph() {
|
||||
if (network) return;
|
||||
|
||||
const container = document.getElementById("graph");
|
||||
network = new vis.Network(
|
||||
container,
|
||||
{ nodes, edges },
|
||||
{
|
||||
layout: { improvedLayout: true },
|
||||
physics: {
|
||||
enabled: true,
|
||||
solver: "barnesHut",
|
||||
barnesHut: { gravitationalConstant: -8000, springLength: 120, springConstant: 0.04 },
|
||||
stabilization: { iterations: 200 }
|
||||
},
|
||||
interaction: {
|
||||
dragNodes: true,
|
||||
hover: true,
|
||||
multiselect: true
|
||||
},
|
||||
nodes: {
|
||||
shape: 'dot',
|
||||
size: 14,
|
||||
font: { color: "#c9d1d9" },
|
||||
color: {
|
||||
background: "#1f6feb",
|
||||
border: "#79c0ff",
|
||||
highlight: { background: "#388bfd", border: "#a5d6ff" }
|
||||
},
|
||||
chosen: {
|
||||
node: chosen_node
|
||||
},
|
||||
shape: "custom",
|
||||
ctxRenderer: renderNode,
|
||||
size: 18,
|
||||
},
|
||||
edges: {
|
||||
arrows: { to: { enabled: true, scaleFactor: 0.8 } },
|
||||
arrowStrikethrough: false,
|
||||
font: { align: "middle", color: "#000000ff" },
|
||||
color: { color: "rgba(201,209,217,0.35)", highlight: "#c9d1d9" },
|
||||
smooth: { type: "dynamic" },
|
||||
arrows: "to",
|
||||
}
|
||||
}
|
||||
);
|
||||
|
||||
// Save positions when user drags nodes
|
||||
|
||||
network.on("dragEnd", (params) => {
|
||||
const pos = network.getPositions(params.nodes);
|
||||
for (const id of params.nodes) {
|
||||
pinnedPositions.set(id, pos[id]);
|
||||
}
|
||||
});
|
||||
|
||||
window.network = network;
|
||||
}
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue