Fix error underlining and popup problems

.vscode/launch.json

@@ -1,5 +1,5 @@
 {
-  "version": "0.2.4",
+  "version": "0.2.5",
   "configurations": [
     {
       "name": "Run Extension",

juvix.version

@@ -1 +1 @@
-0.6.6
+0.6.8

package.json

@@ -1,6 +1,6 @@
 {
   "name": "juvix-mode",
-  "version": "0.2.4",
+  "version": "0.2.5",
   "license": "GPL-3.0",
   "description": "Juvix Mode for VSCode",
   "displayName": "Juvix",
@@ -442,23 +442,17 @@
         "owner": "juvixerror",
         "source": "Juvix Error",
         "fileLocation": "autoDetect",
-        "pattern": [
-          {
-            "kind": "location",
-            "regexp": "^(.+):(\\d+)(?:-(\\d+))?:(\\d+)-(\\d+): (\\w+).*",
-            "file": 1,
-            "line": 2,
-            "endLine": 3,
-            "column": 4,
-            "endColumn": 5,
-            "severity": 6
-          },
-          {
-            "regexp": "(.*)",
-            "message": 1,
-            "loop": true
-          }
-        ]
+        "pattern": {
+          "kind": "location",
+          "regexp": "^(.+):(\\d+)(?:-(\\d+))?:(\\d+)-(\\d+):\\s+(\\w+):(.*)$",
+          "file": 1,
+          "line": 2,
+          "endLine": 3,
+          "column": 4,
+          "endColumn": 5,
+          "severity": 6,
+          "message": 7
+        }
       }
     ],
     "commands": [
@@ -818,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/check.ts

@@ -1,92 +1,29 @@
-/*---------------------------------------------------------
- * Copyright (C) Microsoft Corporation. All rights reserved.
- *--------------------------------------------------------*/
-
 import * as vscode from 'vscode';
 import * as user from './config';
-import { isJuvixFile, runShellCommand, getDiagnosticFromError } from './utils/base';
+import { isJuvixFile } from './utils/base';
 import { logger } from './utils/debug';
-import { setJuvixCommandStatusBarItem, inProgressJuvixCommandStatusBar, showExecResultJuvixStatusBar } from './statusbar';
 
-export async function activate(context: vscode.ExtensionContext, diagnosticCollection: vscode.DiagnosticCollection) {
+export async function activate(context: vscode.ExtensionContext, typecheckTask: vscode.Task) {
   const config = new user.JuvixConfig();
 
-  const command = 'juvix-mode.typecheck-silent';
-
-  const commandHandler = async (doc: vscode.TextDocument, content: string) => {
-    const activeEditor = vscode.window.activeTextEditor;
-
-    if (activeEditor && activeEditor.document == doc) {
-      if (doc && isJuvixFile(doc)) {
-        const filePath = doc.fileName;
-
-        const typecheckerCall = [
-          config.getJuvixExec(),
-          config.getGlobalFlags(),
-          'typecheck',
-          config.getTypeckeckFlags(),
-          filePath,
-        ].join(' ');
-
-        inProgressJuvixCommandStatusBar('Typecheck');
-        const { stdout, stderr, status } = await runShellCommand(typecheckerCall, content);
-
-        if (status !== 0) {
-          showExecResultJuvixStatusBar(false, 'Typecheck', stderr);
-          const diag = getDiagnosticFromError(stderr);
-          if (diag)
-            diagnosticCollection.set(doc.uri, [diag]);
-        }
-        else {
-          showExecResultJuvixStatusBar(true, 'Typecheck', stdout);
-          diagnosticCollection.delete(doc.uri);
-        }
-        return { stdout, stderr, status };
-      }
-    }
-    return undefined;
-  };
-
-  context.subscriptions.push(
-    vscode.commands.registerCommand(command, commandHandler),
-  );
-
-
-  context.subscriptions.push(
-    vscode.workspace.onDidCloseTextDocument(doc => diagnosticCollection.delete(doc.uri))
-  );
-
-  context.subscriptions.push(
-    vscode.window.onDidChangeActiveTextEditor(_ => {
-      setJuvixCommandStatusBarItem();
-    }
-    ));
-
   switch (config.typecheckOn()) {
     case 'change':
       context.subscriptions.push(
-        vscode.workspace.onDidChangeTextDocument(e => {
+        vscode.workspace.onDidChangeTextDocument(async e => {
           const doc = e.document;
           const activeEditor = vscode.window.activeTextEditor;
           if (activeEditor && activeEditor.document === doc && isJuvixFile(doc))
-            vscode.commands.executeCommand(
-              'juvix-mode.typecheck-silent',
-              doc,
-              doc.getText(),
-            )
+            await vscode.tasks.executeTask(typecheckTask);
         }),
       );
       break;
     case 'save':
       context.subscriptions.push(
-        vscode.workspace.onDidSaveTextDocument(doc => {
+        vscode.workspace.onDidSaveTextDocument(async doc => {
           const activeEditor = vscode.window.activeTextEditor;
-          if (activeEditor && activeEditor.document === doc && isJuvixFile(doc))
-            vscode.commands.executeCommand(
-              'juvix-mode.typecheck-silent',
-              doc,
-              doc.getText(),
-            )
+          if (activeEditor && activeEditor.document === doc && isJuvixFile(doc)) {
+            await vscode.tasks.executeTask(typecheckTask);
+          }
         }),
       );
       break;

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/extension.ts

@@ -53,10 +53,6 @@ export async function activate(context: vscode.ExtensionContext) {
     ];
     modules.forEach(module => module.activate(context));
 
-    let juvixDiagnosticCollection = vscode.languages.createDiagnosticCollection('juvix');
-    check.activate(context, juvixDiagnosticCollection);
-    context.subscriptions.push(juvixDiagnosticCollection);
-
     vscode.commands.executeCommand('setContext', 'juvix-mode:ready', true);
   }
 }

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 [];

src/highlighting.ts

@@ -31,7 +31,6 @@ map that associates a file path to the corresponding information for that file.
 export async function activate(context: vscode.ExtensionContext) {
   if (!config.enableSemanticSyntax()) return;
   try {
-    const semanticTokensProvider = new Highlighter();
     const highlighterProvider =
       vscode.languages.registerDocumentSemanticTokensProvider(
         { language: 'Juvix', scheme: 'file' },
@@ -101,6 +100,13 @@ export const legend: vscode.SemanticTokensLegend = (function () {
 })();
 
 export class Highlighter implements vscode.DocumentSemanticTokensProvider {
+  private _onDidChangeSemanticTokens = new vscode.EventEmitter<void>();
+  public onDidChangeSemanticTokens = this._onDidChangeSemanticTokens.event;
+
+  public triggerRehighlighting(): void {
+    this._onDidChangeSemanticTokens.fire();
+  }
+
   async provideDocumentSemanticTokens(
     document: vscode.TextDocument,
     _token: vscode.CancellationToken,
@@ -184,7 +190,7 @@ export class Highlighter implements vscode.DocumentSemanticTokensProvider {
               ? tk.interval.length
               : tk.interval.endCol
             : contentLines[l].length;
-        // lineLength represent the number of symbols we can see on the screen.
+        // lineLength represents the number of symbols we can see on the screen.
         // However, in js, length for unicode symbols works not as expected, but
         // rather shows the code units number.
         // So we need to actually calculate all the code units.
@@ -267,3 +273,5 @@ export class Highlighter implements vscode.DocumentSemanticTokensProvider {
     return token;
   }
 }
+
+export const semanticTokensProvider = new Highlighter();

src/tasks.ts

@@ -5,6 +5,7 @@
 import * as vscode from 'vscode';
 import * as user from './config';
 import { logger } from './utils/debug';
+import * as check from './check';
 import { inProgressJuvixCommandStatusBar, showExecResultJuvixStatusBar } from './statusbar';
 
 export const TASK_TYPE = 'Juvix';
@@ -37,6 +38,7 @@ export async function activate(context: vscode.ExtensionContext) {
         const cmdName = task.name.replace(' ', '-');
         let useCmdName;
         if (cmdName === 'typecheck-silent') {
+          check.activate(context, task);
           useCmdName = 'typecheck';
         } else {
           useCmdName = cmdName;
@@ -68,7 +70,6 @@ export async function activate(context: vscode.ExtensionContext) {
         context.subscriptions.push(initDisp);
 
         const disp = vscode.tasks.onDidEndTaskProcess(e => {
-
           if (e.execution.task.name === task.name) {
             if (e.exitCode === 0) {
               showExecResultJuvixStatusBar(true, useCmdName, '');
@@ -107,7 +108,13 @@ export class JuvixTaskProvider implements vscode.TaskProvider {
         command: 'typecheck',
         args: [config.getTypeckeckFlags(), '${file}'],
         group: vscode.TaskGroup.Build,
-        reveal: vscode.TaskRevealKind.Silent,
+        reveal: vscode.TaskRevealKind.Always,
+      },
+      {
+        command: 'typecheck-silent',
+        args: [config.getTypeckeckFlags(), '${file}'],
+        group: vscode.TaskGroup.Build,
+        reveal: vscode.TaskRevealKind.Never,
       },
       {
         command: 'compile',
@@ -227,6 +234,9 @@ export async function JuvixTask(
     case 'update-dependencies':
       exec = new vscode.ShellExecution(JuvixExec + `dependencies update`);
       break;
+    case 'typecheck-silent':
+      exec = new vscode.ShellExecution(JuvixExec + ` typecheck ${fl}`);
+      break;
     default:
       exec = new vscode.ShellExecution(JuvixExec + ` ${input}`);
       break;

src/utils/base.ts

@@ -1,6 +1,3 @@
-/*---------------------------------------------------------
- * Copyright (C) Microsoft Corporation. All rights reserved.
- *--------------------------------------------------------*/
 import { spawn, spawnSync } from 'child_process';
 import * as vscode from 'vscode';
 import { Mutex } from 'async-mutex';
@@ -81,29 +78,3 @@ export async function runShellCommand(command: string, input?: string): Promise<
     }
   });
 }
-
-const regexJuvixError = /(?<file>.*):(?<line>\d+):(?<begin_col>\d+)-?(?<end_col>\d+)?:\s(?<err_type>.*):\s?(?<msg>((\n|.)*))/g;
-
-export function getDiagnosticFromError(output: string): vscode.Diagnostic | undefined {
-  const { file, line, begin_col, end_col, err_type, msg } = regexJuvixError.exec(output)!.groups!;
-  if (!msg || !line || !begin_col) return undefined;
-  const range = new vscode.Range(
-    new vscode.Position(parseInt(line) - 1, parseInt(begin_col) - 1),
-    new vscode.Position(parseInt(line) - 1, parseInt(end_col ?? begin_col) - 1),
-  );
-  let severity;
-  switch (err_type) {
-    case 'error':
-      severity = vscode.DiagnosticSeverity.Error;
-      break;
-    case 'warning':
-      severity = vscode.DiagnosticSeverity.Warning;
-      break;
-    case 'info':
-      severity = vscode.DiagnosticSeverity.Information;
-      break;
-  }
-  const diag = new vscode.Diagnostic(range, msg, severity);
-  diag.source = 'Juvix';
-  return diag;
-}