Work

2022-04-26 19:04:36 +02:00
parent cb2d3f8652
commit 76636dd9b1
41 changed files with 500 additions and 287 deletions
@@ -92,6 +92,18 @@ export function editorSyscalls(editor: Editor): SysCallMapping {
        type: "hide-lhs",
      });
    },
+    "editor.showBhs": (ctx, html: string, flex: number) => {
+      editor.viewDispatch({
+        type: "show-bhs",
+        flex,
+        html,
+      });
+    },
+    "editor.hideBhs": (ctx) => {
+      editor.viewDispatch({
+        type: "hide-bhs",
+      });
+    },
    "editor.insertAtPos": (ctx, text: string, pos: number) => {
      editor.editorView!.dispatch({
        changes: {