diff --git a/web/root/src/visualizer.ts b/web/root/src/visualizer.ts index de758fa..dc0daaf 100644 --- a/web/root/src/visualizer.ts +++ b/web/root/src/visualizer.ts @@ -4,6 +4,7 @@ import * as vis from "npm:vis-network/standalone"; import { StateEffect } from "npm:@codemirror/state"; import { Machine } from "./automata.ts"; +import { getText } from "./editor.ts"; export const nodes = new vis.DataSet(); export const edges = new vis.DataSet(); @@ -25,8 +26,15 @@ type GraphTheme = { edge_hover: Color; edge_active: Color; - edge_font_size: number; + font_face: string + node_font_size: number; + node_font: string, + node_font_bold: string, + + edge_font_size: number; + edge_font: string, + edge_font_bold: string, }; let _graphTheme: GraphTheme | null = null; @@ -60,8 +68,15 @@ function getGraphTheme(): GraphTheme { edge_hover: cssVar("--graph-edge-hover"), edge_active: cssVar("--graph-edge-active"), - edge_font_size: Number(cssVar("--graph-edge-font-size")), + font_face: cssVar("--graph-font"), + node_font_size: Number(cssVar("--graph-node-font-size")), + node_font: `${cssVar("--graph-node-font-size")}px ${cssVar("--graph-font")}`, + node_font_bold: `bold ${cssVar("--graph-node-font-size")}px ${cssVar("--graph-font")}`, + + edge_font_size: Number(cssVar("--graph-edge-font-size")), + edge_font: `${Number(cssVar("--graph-edge-font-size"))}px ${cssVar("--graph-font")}`, + edge_font_bold: `bold ${Number(cssVar("--graph-edge-font-size"))}px ${cssVar("--graph-font")}`, }; return _graphTheme; @@ -78,7 +93,6 @@ export function updateGraphTheme() { color: gt.fg_0, bold: { color: gt.fg_1, - // mod: "", }, }, }, @@ -86,13 +100,13 @@ export function updateGraphTheme() { labelHighlightBold: true, font: { align: "top", - face: 'arial', + face: gt.font_face, size: gt.edge_font_size, color: gt.fg_0, strokeColor: gt.bg_0, bold: { color: gt.fg_1, - face: 'arial', + face: gt.font_face, size: gt.edge_font_size, mod: "bold", }, @@ -107,6 +121,8 @@ export function updateGraphTheme() { }, }, }); + + setAutomaton(automaton) } let automaton: Machine = { @@ -133,21 +149,38 @@ export function clearAutomaton() { }; } + +let _measureCanvas: HTMLCanvasElement | null = null; + +export function measureTextWidth(text: string, font: string): number { + if (!_measureCanvas) { + _measureCanvas = document.createElement("canvas"); + } + + const ctx = _measureCanvas.getContext("2d")!; + ctx.font = font; + + return ctx.measureText(text).width; +} + export function setAutomaton(auto: Machine) { - console.log(auto); automaton = auto; // Populate nodes for (const state of automaton.states.keys()) { + + const size = measureTextWidth(state, getGraphTheme().node_font)/2+10 if (nodes.get(state)) { nodes.update({ id: state, label: state, + size }); } else { nodes.add({ id: state, label: state, + size }); } } @@ -303,7 +336,7 @@ function renderNode({ ctx.save(); - ctx.font = hover||selected?'bold 14px arial':'14px arial'; + ctx.font = hover||selected?t.node_font_bold:t.node_font; ctx.textAlign = "center"; ctx.textBaseline = "middle"; diff --git a/web/root/style/themes.scss b/web/root/style/themes.scss index ac86de9..4f130af 100644 --- a/web/root/style/themes.scss +++ b/web/root/style/themes.scss @@ -38,6 +38,8 @@ --graph-fg-1: var(--fg-1); --graph-fg-2: var(--fg-2); + --graph-font: arial; + --graph-node-font-size: 14; --graph-edge-font-size: 10;