Address stack issues in playground, unicode input in playground, fixes to error recovery

playground/src/emul.ts

@@ -205,9 +205,7 @@ export let shim: NodeShim = {
     platform: "linux",
     argv: ["", ""],
     stdout: {
-      // We'll want to replace this one
       write(s) {
-        console.log("*", s);
         shim.stdout += s;
       },
     },

playground/src/main.ts

@@ -102,8 +102,8 @@ document.body.appendChild(iframe);
 
 function run(src: string) {
   console.log("SEND TO", iframe.contentWindow);
-  const fileName = state.currentFile.value
+  const fileName = state.currentFile.value;
-  postMessage({ type: 'compileRequest', fileName, src });
+  postMessage({ type: "compileRequest", fileName, src });
 }
 
 function runOutput() {
@@ -133,7 +133,6 @@ function setOutput(output: string) {
   state.output.value = output;
 }
 
-
 window.onmessage = (ev: MessageEvent<Message>) => {
   console.log("window got", ev.data);
   if ("messages" in ev.data) state.messages.value = ev.data.messages;
@@ -166,7 +165,7 @@ const state = {
   editor: signal<monaco.editor.IStandaloneCodeEditor | null>(null),
   dark: signal(false),
   files: signal<string[]>(["Tour.newt"]),
-  currentFile: signal<string>(localStorage.currentFile ?? 'Tour.newt')
+  currentFile: signal<string>(localStorage.currentFile ?? "Tour.newt"),
 };
 
 // Monitor dark mode state (TODO - let user override system setting)
@@ -197,8 +196,8 @@ async function loadFile(fn: string) {
   } else {
     state.editor.value!.setValue("module Main\n\n-- File not found\n");
   }
-  state.currentFile.value = fn
+  state.currentFile.value = fn;
-  localStorage.currentFile = fn
+  localStorage.currentFile = fn;
 }
 
 // I keep pressing this.
@@ -222,6 +221,16 @@ interface EditorProps {
   initialValue: string;
 }
 
+const ABBREV: Record<string, string> = {
+    '\\x': '×',
+    '\\r': '→',
+    '\\all': '∀',
+    '\\\\': '\\',
+    '\\==': '≡',
+    '\circ': '∘',
+    '\\_1': '₁',
+  }
+
 function Editor({ initialValue }: EditorProps) {
   const ref = useRef<HTMLDivElement>(null);
   useEffect(() => {
@@ -244,6 +253,36 @@ function Editor({ initialValue }: EditorProps) {
         run(value);
         localStorage.code = value;
       }, 1000);
+      let last = ev.changes[ev.changes.length - 1];
+      const model = editor.getModel();
+      // figure out heuristics here, what chars do we want to trigger?
+      if (model && last.text && " ')_".includes(last.text)) {
+        console.log('LAST', last)
+        let { startLineNumber, startColumn } = last.range;
+        const text = model.getValueInRange(
+          new monaco.Range(
+            startLineNumber,
+            Math.max(1, startColumn - 10),
+            startLineNumber,
+            startColumn
+          )
+        );
+        const m = text.match(/(\\[^ ]+)$/);
+        if (m) {
+          let cand = m[0];
+          console.log("GOT", cand);
+          let text = ABBREV[cand];
+          if (text) {
+            const range = new monaco.Range(
+              startLineNumber,
+              startColumn - cand.length,
+              startLineNumber,
+              startColumn
+            );
+            editor.executeEdits("replaceSequence", [{ range, text: text }]);
+          }
+        }
+      }
     });
     if (initialValue === LOADING) loadFile("Tour.newt");
     else run(initialValue);
@@ -363,7 +402,11 @@ function EditWrap({
     h(
       "div",
       { className: "tabBar" },
-      h("select", { onChange: selectFile, value: state.currentFile.value }, options),
+      h(
+        "select",
+        { onChange: selectFile, value: state.currentFile.value },
+        options
+      ),
       h("div", { style: { flex: "1 1" } }),
       h("button", { onClick: runOutput }, svg(play)),
       h("button", { onClick: toggle }, svg(d))

src/Main.idr

@@ -26,6 +26,7 @@ import System
 import System.Directory
 import System.File
 import System.Path
+import Data.Buffer
 
 fail : String -> M a
 fail msg = putStrLn msg >> exitFailure
@@ -69,7 +70,7 @@ writeSource fn = do
 
 parseDecls : String -> Operators -> TokenList -> SnocList Decl -> M (List Decl, Operators)
 parseDecls fn ops [] acc = pure (acc <>> [], ops)
-parseDecls fn ops toks acc =
+parseDecls fn ops toks@(first :: _) acc =
   case partialParse fn (sameLevel parseDecl) ops toks of
     Left (err, toks) => do
       putStrLn $ showError "" err
@@ -79,7 +80,17 @@ parseDecls fn ops toks acc =
   where
     recover : TokenList -> TokenList
     recover [] = []
-    recover (tok :: toks) = if tok.bounds.startCol == 0 then (tok :: toks) else recover toks
+    -- skip to top token, but make sure there is progress
+    recover (tok :: toks) = if tok.bounds.startCol == 0 && tok.bounds /= first.bounds
+      then (tok :: toks)
+      else recover toks
+
+fastReadFile : HasIO io => String -> io (Either FileError String)
+fastReadFile fn = do
+  Right buf <- createBufferFromFile fn | Left err => pure $ Left err
+  len <- rawSize buf
+  Right <$> getString buf 0 len
+
 
 ||| New style loader, one def at a time
 processModule : String -> List String -> String -> M String
@@ -88,7 +99,7 @@ processModule base stk name = do
   let False := elem name top.loaded | _ => pure ""
   modify { loaded $= (name::) }
   let fn = if base == "" then name ++ ".newt" else base ++ "/" ++ name ++ ".newt"
-  Right src <- readFile $ fn
+  Right src <- fastReadFile $ fn
     | Left err => fail "error reading \{fn}: \{show err}"
   let Right toks = tokenise fn src
     | Left err => fail (showError src err)