Fixes #576 supporting markdown in headers and refactoring some stuff

2023-11-27 16:29:19 +01:00
parent 1335820abd
commit 259ad5b488
8 changed files with 36 additions and 31 deletions
@@ -80,7 +80,7 @@ export function filterBox(
 }

 export function showPanel(
-  id: "lhs" | "rhs" | "bhs" | "modal" | "ps" | "preface",
+  id: "lhs" | "rhs" | "bhs" | "modal" | "bottom" | "top",
  mode: number,
  html: string,
  script = "",
@@ -89,7 +89,7 @@ export function showPanel(
 }

 export function hidePanel(
-  id: "lhs" | "rhs" | "bhs" | "modal" | "ps" | "preface",
+  id: "lhs" | "rhs" | "bhs" | "modal" | "bottom" | "top",
 ): Promise<void> {
  return syscall("editor.hidePanel", id);
 }