From b65a76ccd3a35edf76d9599190eeedc6906c9267 Mon Sep 17 00:00:00 2001
From: Steve Dunham <dunhamsteve@gmail.com>
Date: Sat, 14 Sep 2024 21:55:27 -0700
Subject: [PATCH] show newt failure in vscode

---
 TODO.md                                   | 2 +-
 newt-vscode/src/extension.ts              | 9 +++++++++
 newt-vscode/syntaxes/newt.tmLanguage.json | 2 +-
 src/Lib/Check.idr                         | 2 +-
 4 files changed, 12 insertions(+), 3 deletions(-)

diff --git a/TODO.md b/TODO.md
index a193579..9b91586 100644
--- a/TODO.md
+++ b/TODO.md
@@ -27,7 +27,7 @@ I may be done with `U` - I keep typing `Type`.
     - have separate type of implict with `{{}}`
 - [ ] do blocks
 - [ ] some solution for `+` problem (classes? ambiguity?)
-- [ ] show compiler failure in the editor (exit code != 0)
+- [x] show compiler failure in the editor (exit code != 0)
 - [ ] write js files into `out` directory
 - [ ] detect extra clauses in case statements
 - [ ] add test framework
diff --git a/newt-vscode/src/extension.ts b/newt-vscode/src/extension.ts
index 5c2b10c..29c02bc 100644
--- a/newt-vscode/src/extension.ts
+++ b/newt-vscode/src/extension.ts
@@ -17,6 +17,7 @@ export function activate(context: vscode.ExtensionContext) {
     const cmd = config.get<string>("path", "build/exec/newt");
     const command = `${cmd} ${fileName}`;
     exec(command, { cwd }, (err, stdout, _stderr) => {
+      // I think I ignored 1 here because I wanted failure to launch
       if (err && err.code !== 1) {
         vscode.window.showErrorMessage(`newt error: ${err}`);
       }
@@ -25,6 +26,14 @@ export function activate(context: vscode.ExtensionContext) {
       const lines = stdout.split("\n");
       const diagnostics: vscode.Diagnostic[] = [];
 
+      if (err) {
+        let start = new vscode.Position(0,0)
+        let end = new vscode.Position(0,1)
+        let range = document.getWordRangeAtPosition(start) ?? new vscode.Range(start,end)
+        const diag = new vscode.Diagnostic(range, "newt execution failed", vscode.DiagnosticSeverity.Error)
+        diagnostics.push(diag)
+      }
+
       for (let i = 0; i < lines.length; i++) {
         const line = lines[i];
         const match = line.match(/(INFO|ERROR) at \((\d+), (\d+)\): (.*)/);
diff --git a/newt-vscode/syntaxes/newt.tmLanguage.json b/newt-vscode/syntaxes/newt.tmLanguage.json
index 3eca2b0..aa4c512 100644
--- a/newt-vscode/syntaxes/newt.tmLanguage.json
+++ b/newt-vscode/syntaxes/newt.tmLanguage.json
@@ -16,7 +16,7 @@
     },
     {
       "name": "keyword.newt",
-      "match": "\\b(data|where|case|of|let|in|U|module|ptype|pfunc)\\b"
+      "match": "\\b(data|where|case|of|let|in|U|module|ptype|pfunc|infix|infixl|infixr)\\b"
     }
   ]
 }
diff --git a/src/Lib/Check.idr b/src/Lib/Check.idr
index 345ed5f..57c5689 100644
--- a/src/Lib/Check.idr
+++ b/src/Lib/Check.idr
@@ -650,7 +650,7 @@ infer ctx (RPi fc nm icit ty ty2) = do
   let nm := fromMaybe "_" nm
   ty2' <- check (extend ctx nm vty') ty2 (VU fc)
   pure (Pi fc nm icit ty' ty2', (VU fc))
-infer ctx (RLet fc str tm tm1 tm2) = error fc "implement RLet"
+infer ctx (RLet fc nm ty v sc) = error fc "implement RLet"
 infer ctx (RAnn fc tm rty) = do
   ty <- check ctx rty (VU fc)
   vty <- eval ctx.env CBN ty