editor: better rendering of helper outlines

This commit is contained in:
Joeri Exelmans 2025-10-17 11:34:49 +02:00
parent 9401c02800
commit e8fda9bdf0
8 changed files with 95 additions and 116 deletions

View file

@ -52,6 +52,13 @@ function PseudoStateIcon(props: {}) {
</svg>;
}
function HistoryIcon(props: {kind: "shallow"|"deep"}) {
const w=20, h=20;
const text = props.kind === "shallow" ? "H" : "H*";
return <svg width={w} height={h}><circle cx={w/2} cy={h/2} r={Math.min(w,h)/2-1} fill="white" stroke="black"/><text x={w/2} y={h/2+4} textAnchor="middle" fontSize={11} fontWeight={400}>{text}</text></svg>;
}
export function TopPanel({rt, time, setTime, onInit, onClear, onRaise, ast, mode, setMode}: TopPanelProps) {
const [displayTime, setDisplayTime] = useState("0.000");
const [timescale, setTimescale] = useState(1);
@ -111,6 +118,8 @@ export function TopPanel({rt, time, setTime, onInit, onClear, onRaise, ast, mode
["and", "AND-states", <RountangleIcon kind="and"/>],
["or", "OR-states", <RountangleIcon kind="or"/>],
["pseudo", "pseudo-states", <PseudoStateIcon/>],
["shallow", "shallow history", <HistoryIcon kind="shallow"/>],
["deep", "deep history", <HistoryIcon kind="deep"/>],
["transition", "transitions", <TrendingFlatIcon fontSize="small"/>],
["text", "text", <>&nbsp;T&nbsp;</>],
] as [InsertMode, string, ReactElement][]).map(([m, hint, buttonTxt]) =>