From 08cc2637f5312d9945db3942054a9c9e20f9d550 Mon Sep 17 00:00:00 2001 From: Steve Dunham Date: Tue, 17 Dec 2024 20:44:39 -0800 Subject: [PATCH] Address stack issues in playground, unicode input in playground, fixes to error recovery --- playground/src/emul.ts | 2 -- playground/src/main.ts | 57 ++++++++++++++++++++++++++++++++++++------ src/Main.idr | 17 ++++++++++--- 3 files changed, 64 insertions(+), 12 deletions(-) diff --git a/playground/src/emul.ts b/playground/src/emul.ts index 5c4e6e8..3e413f5 100644 --- a/playground/src/emul.ts +++ b/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; }, }, diff --git a/playground/src/main.ts b/playground/src/main.ts index 35be5f5..ae9a930 100644 --- a/playground/src/main.ts +++ b/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 - postMessage({ type: 'compileRequest', fileName, src }); + const fileName = state.currentFile.value; + postMessage({ type: "compileRequest", fileName, src }); } function runOutput() { @@ -133,7 +133,6 @@ function setOutput(output: string) { state.output.value = output; } - window.onmessage = (ev: MessageEvent) => { 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(null), dark: signal(false), files: signal(["Tour.newt"]), - currentFile: signal(localStorage.currentFile ?? 'Tour.newt') + currentFile: signal(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 - localStorage.currentFile = fn + state.currentFile.value = fn; + localStorage.currentFile = fn; } // I keep pressing this. @@ -222,6 +221,16 @@ interface EditorProps { initialValue: string; } +const ABBREV: Record = { + '\\x': '×', + '\\r': '→', + '\\all': '∀', + '\\\\': '\\', + '\\==': '≡', + '\circ': '∘', + '\\_1': '₁', + } + function Editor({ initialValue }: EditorProps) { const ref = useRef(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)) diff --git a/src/Main.idr b/src/Main.idr index 1a425a0..fe2969d 100644 --- a/src/Main.idr +++ b/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)