Add "[Expected]" prefix to expected diagnostics in VSCode. closes #94

SReichelt · Jan 24, 2021 · cea26d4 · cea26d4
1 parent 088f659
commit cea26d4
Show file tree

Hide file tree

Showing 3 changed files with 17 additions and 4 deletions.
diff --git a/src/scripts/check.ts b/src/scripts/check.ts
@@ -90,13 +90,13 @@ function checkItem(libraryDefinition: LibraryDefinition, libraryDataProvider: Li
         prefix = 'Hint';
         break;
       }
-      if (expectedDiagnosticIndex >= 0) {
-        prefix += ' (expected)';
-      }
       let fullMessage = `${prefix}: ${message}`;
       if (libraryDefinition.fileReference) {
         fullMessage = `${libraryDefinition.fileReference.fileName}: ${fullMessage}`;
       }
+      if (expectedDiagnosticIndex >= 0) {
+        fullMessage = `[Expected] ${fullMessage}`;
+      }
       console.error(fullMessage);
     }
     for (let {message} of expectedDiagnostics) {

diff --git a/src/vscode/.gitignore b/src/vscode/.gitignore
@@ -1,4 +1,5 @@
 out
+dist
 /webview
 node_modules
 *.vsix
diff --git a/src/vscode/src/logic/providers/diagnosticsProvider.ts b/src/vscode/src/logic/providers/diagnosticsProvider.ts
@@ -1,5 +1,6 @@
 import * as vscode from 'vscode';
 import * as Logic from 'slate-shared/logics/logic';
+import { getExpectedDiagnostics } from 'slate-shared/logics/diagnostics';
 import { LibraryDocument, LibraryDocumentProvider } from '../data';
 
 export class SlateDiagnosticsProvider {
@@ -18,15 +19,26 @@ export class SlateDiagnosticsProvider {
                 warnAboutMissingProofs: true
             };
             checker.checkDefinition(definition, libraryDocument.documentLibraryDataProvider, options).then((checkResult: Logic.LogicCheckResult) => {
+                const expectedDiagnostics = getExpectedDiagnostics(definition);
                 const diagnostics = checkResult.diagnostics.map((diagnostic: Logic.LogicCheckDiagnostic) =>
-                    new vscode.Diagnostic(this.getRange(libraryDocument, diagnostic), diagnostic.message, this.getSeverity(diagnostic)));
+                    this.createDiagnostic(libraryDocument, diagnostic, expectedDiagnostics));
                 if (libraryDocument.document) {
                     libraryDocument.library.diagnosticCollection.set(libraryDocument.document.uri, diagnostics);
                 }
             });
         }
     }
 
+    private createDiagnostic(libraryDocument: LibraryDocument, diagnostic: Logic.LogicCheckDiagnostic, expectedDiagnostics: Logic.LogicCheckDiagnostic[]): vscode.Diagnostic {
+        let message = diagnostic.message;
+        const expectedDiagnosticIndex = expectedDiagnostics.findIndex((expectedDiagnostic: Logic.LogicCheckDiagnostic) => (expectedDiagnostic.severity === diagnostic.severity && expectedDiagnostic.message === diagnostic.message));
+        if (expectedDiagnosticIndex >= 0) {
+            expectedDiagnostics.splice(expectedDiagnosticIndex, 1);
+            message = `[Expected] ${message}`;
+        }
+        return new vscode.Diagnostic(this.getRange(libraryDocument, diagnostic), message, this.getSeverity(diagnostic));
+    }
+
     private getRange(libraryDocument: LibraryDocument, diagnostic: Logic.LogicCheckDiagnostic): vscode.Range {
         const range = libraryDocument.rangeMap.get(diagnostic.object);
         if (range) {