+ {/* shortcuts / about */}
+
+
~}>
+
+
+
+
- {/* undo / redo */}
-
- Ctrl+Z>}>
-
-
- Ctrl+Shift+Z>}>
-
-
-
+ {/* undo / redo */}
+
+ Ctrl+Z>}>
+
+
+ Ctrl+Shift+Z>}>
+
+
+
- {/* insert rountangle / arrow / ... */}
-
- {([
- ["and", "AND-states",
,
A],
- ["or", "OR-states",
,
O],
- ["pseudo", "pseudo-states",
,
P],
- ["shallow", "shallow history",
,
H],
- ["deep", "deep history",
, <>>],
- ["transition", "transitions",
,
T],
- ["text", "text", <> T >,
X],
- ] as [InsertMode, string, ReactElement, ReactElement][]).map(([m, hint, buttonTxt, keyInfo]) =>
-
- )}
-
-
+ {/* insert rountangle / arrow / ... */}
+
+ {([
+ ["and", "AND-states",
,
A],
+ ["or", "OR-states",
,
O],
+ ["pseudo", "pseudo-states",
,
P],
+ ["shallow", "shallow history",
,
H],
+ ["deep", "deep history",
, <>>],
+ ["transition", "transitions",
,
T],
+ ["text", "text", <> T >,
X],
+ ] as [InsertMode, string, ReactElement, ReactElement][]).map(([m, hint, buttonTxt, keyInfo]) =>
+
+ )}
+
- {/* execution */}
-
-
- {/* init / clear / pause / real time */}
-
-
I}>
-
-
-
C}>
-
-
-
-
Space toggles>}>
-
-
-
-
-
-
-
- {/* speed */}
-
-
- S}>
-
-
- onTimeScaleChange(e.target.value, Math.round(performance.now()))}/>
- F}>
-
-
-
-
-
-
- {/* time, next */}
-
-
-
-
-
-
-
-
-
-
Tab}>
-
-
-
-
-
-
-
-
+ {/* execution */}
- {ast.inputEvents &&
- <>
- {ast.inputEvents.map(({event, paramName}) =>
- <>
- {paramName && <>
>}
- >)}
- >
- }
+ {/* init / clear / pause / real time */}
+
+
I}>
+
+
+
C}>
+
+
+
+
Space toggles>}>
+
+
+
+
+
+ {/* speed */}
+
+
+ S}>
+
+
+ onTimeScaleChange(e.target.value, Math.round(performance.now()))}/>
+ F}>
+
+
+
+
+
+ {/* time, next */}
+
+
+
+
+
+
+
+
+
+
Tab}>
+
+
+
+
+
-
+ {ast.inputEvents &&
+ <>
+ {ast.inputEvents.map(({event, paramName}) =>
+
+ {paramName && <>>}
+
)}
+ >
+ }
+