--vscode option

package.json

@@ -812,6 +812,11 @@
           "default": true,
           "description": "Disable ANSI formatting."
         },
+        "juvix-mode.vscodeErrors": {
+          "type": "boolean",
+          "default": true,
+          "description": "Enable VSCode compatible error formatting."
+        },
         "juvix-mode.showNameIds": {
           "type": "boolean",
           "default": false,

src/config.ts

@@ -121,6 +121,10 @@ export class JuvixConfig {
     return this.workspaceConfig.get('noColors', true);
   }
 
+  public vscodeErrors(): boolean {
+    return this.workspaceConfig.get('vscodeErrors', true);
+  }
+
   public showNameIds(): boolean {
     return this.workspaceConfig.get('showNameIds', false);
   }
@@ -160,6 +164,7 @@ export class JuvixConfig {
   public getGlobalFlags(): string {
     const flags: string[] = [];
     if (this.noColors()) flags.push('--no-colors');
+    if (this.vscodeErrors()) flags.push('--vscode');
     if (this.showNameIds()) flags.push('--show-name-ids');
     if (this.noTermination()) flags.push('--no-termination');
     if (this.noPositivity()) flags.push('--no-positivity');

src/formatter.ts

@@ -34,6 +34,7 @@ export function activate(_context: vscode.ExtensionContext) {
         // this is the way to protect from unexpected behaviour of the `format` command
         return stdout !== '' ? [vscode.TextEdit.replace(range, stdout)] : [];
       } else {
+        // TODO: this should be parsed with the problem matcher
         const errMsg: string = res.stderr.toString();
         logger.warn(errMsg);
         return [];