From f40b711a61cb9a4c020d187dc5fb316d6ec281e3 Mon Sep 17 00:00:00 2001
From: SeeBasTStick <sebastian.stock@hhu.de>
Date: Thu, 21 May 2020 11:18:13 +0200
Subject: [PATCH] added warnings
---
.vscode/settings.json | 4 +-
package-lock.json | 10 ++++
package.json | 19 ++++----
server/src/ErrorMatcher.ts | 94 +++++++++++++++++++++++++-------------
server/src/server.ts | 14 +++---
5 files changed, 94 insertions(+), 47 deletions(-)
diff --git a/.vscode/settings.json b/.vscode/settings.json
index 4d7c850..e10b8e4 100644
--- a/.vscode/settings.json
+++ b/.vscode/settings.json
@@ -5,5 +5,7 @@
"typescript.preferences.quoteStyle": "single",
"editor.codeActionsOnSave": {
"source.fixAll.eslint": true
- }
+ },
+ "languageServer.strictChecks": true,
+ "languageServer.wdChecks": true
}
\ No newline at end of file
diff --git a/package-lock.json b/package-lock.json
index fd51cfe..cc4d13b 100644
--- a/package-lock.json
+++ b/package-lock.json
@@ -579,6 +579,11 @@
"integrity": "sha512-MSjYzcWNOA0ewAHpz0MxpYFvwg6yjy1NG3xteoqz644VCo/RPgnr1/GGt+ic3iJTzQ8Eu3TdM14SawnVUmGE6A==",
"dev": true
},
+ "error": {
+ "version": "10.3.0",
+ "resolved": "https://registry.npmjs.org/error/-/error-10.3.0.tgz",
+ "integrity": "sha512-y0yyhFzqncP5zCdlnwFvrorcujP55Du7uouOmmZQPQVXJvKPXWehVeqHe1mb/HLrdYB2z5MFs8v/ZWHv3YvTGg=="
+ },
"es-abstract": {
"version": "1.17.5",
"resolved": "https://registry.npmjs.org/es-abstract/-/es-abstract-1.17.5.tgz",
@@ -1977,6 +1982,11 @@
"is-number": "^7.0.0"
}
},
+ "ts-xor": {
+ "version": "1.0.8",
+ "resolved": "https://registry.npmjs.org/ts-xor/-/ts-xor-1.0.8.tgz",
+ "integrity": "sha512-0u70/SDLSCaX23UddnwAb2GvZZ2N0Rbjnmemn5pHoR40D32Xcva5KRGWV9SdJOKHCjJUlmctmCTvT0z+2yT8aw=="
+ },
"tslib": {
"version": "1.9.3",
"resolved": "https://registry.npmjs.org/tslib/-/tslib-1.9.3.tgz",
diff --git a/package.json b/package.json
index 519db1b..4e912e0 100644
--- a/package.json
+++ b/package.json
@@ -6,6 +6,7 @@
"publisher": "SeeBasTStick",
"icon": "prob2-ui.png",
"author": "Sebastian Stock",
+ "license": "MIT",
"repository": {
"type": "git",
"url": "https://github.com/SeeBasTStick/b-eventb-language-extension"
@@ -57,13 +58,13 @@
"languageServer.wdChecks": {
"scope": "window",
"type": "boolean",
- "default": "off",
+ "default": "false",
"description": "Option for WD Checks"
},
"languageServer.strictChecks": {
"scope": "window",
"type": "boolean",
- "default": "off",
+ "default": "false",
"description": "Option for stricter Checks"
}
}
@@ -77,21 +78,23 @@
"test": "sh ./scripts/e2e.sh"
},
"devDependencies": {
- "@types/mocha": "^5.2.7",
- "@types/node": "^12.12.38",
- "@typescript-eslint/parser": "^2.3.0",
- "eslint": "^6.4.0",
- "mocha": "^6.2.2",
- "typescript": "^3.8.3",
+ "@types/mocha": "^7.0.2",
+ "@types/node": "^14.0.4",
+ "@typescript-eslint/parser": "^2.34.0",
+ "eslint": "^7.0.0",
+ "mocha": "^7.1.2",
+ "typescript": "^3.9.3",
"vscode": "^1.1.37"
},
"dependencies": {
"@types/ndjson": "^1.5.0",
"@types/stream-to-array": "^2.3.0",
"@types/vscode": "^1.45.1",
+ "error": "^10.3.0",
"ndjson": "^1.5.0",
"path": "^0.12.7",
"stream-to-array": "^2.3.0",
+ "ts-xor": "^1.0.8",
"vscode-api": "0.0.0",
"vscode-uri": "^2.1.1"
}
diff --git a/server/src/ErrorMatcher.ts b/server/src/ErrorMatcher.ts
index ee8b8da..c686663 100644
--- a/server/src/ErrorMatcher.ts
+++ b/server/src/ErrorMatcher.ts
@@ -2,7 +2,7 @@ import { Diagnostic, DiagnosticSeverity } from 'vscode-languageserver'
import { TextDocument } from 'vscode-languageserver-textdocument'
import * as fs from 'fs';
import * as readline from 'readline'
-
+import {XOR} from 'ts-xor'
export class ErrorMatcher{
@@ -17,44 +17,74 @@ export class ErrorMatcher{
crlfDelay: Infinity
});
+
+
for await (const line of rl) {
- let obj:Error = JSON.parse(line)
-
- var diagnostic:Diagnostic = {
- severity: DiagnosticSeverity.Error,
- range: {
- start:
+ let obj : XOR<Error, Warning> = JSON.parse(line)
+ let diagnostic : Diagnostic
+ console.log(obj)
+
+ let serveity : DiagnosticSeverity
+ let content : ErrorOrWarning
+ if(obj.error ){
+ content = obj.error
+ serveity = DiagnosticSeverity.Error
+ }
+ else{
+ if(obj.warning){
+ content = obj.warning
+ serveity = DiagnosticSeverity.Warning
+ }else{
+ throw new Error("Parsed Object is neither Warning nor Error - this is wrong")
+ }
+ }
+
+ diagnostic = {
+ severity: serveity,
+ range: {
+ start:
{
- character: obj.error.start.col,
- line:obj.error.start.line - 1
+ character: content.start.col,
+ line: content.start.line - 1
},
end: {
- character:obj.error.end.col,
- line :obj.error.end.line -1
- }
-
- },
- message: obj.error.message,
- source: 'prob_prolog'
- };
+ character:content.end.col,
+ line :content.end.line -1
+ }
+ },
+ message: content.message,
+ source: 'prob_prolog'
+ };
diagnostics.add(diagnostic)
}
return diagnostics
}
+
+
}
-interface Error{
- error : {
- message : string
- type : string
- file : string
- start : {
- line : number
- col : number
- }
- end : {
- line : number
- col : number
- }
- };
-}
\ No newline at end of file
+
+
+export interface Error{
+ error : ErrorOrWarning;
+
+}
+
+export interface Warning{
+ warning : ErrorOrWarning
+}
+
+export interface ErrorOrWarning {
+ message: string;
+ type: string;
+ file: string;
+ start: StartOrEnd;
+ end: StartOrEnd;
+ }
+
+ export interface StartOrEnd {
+ line: number;
+ col: number;
+ }
+
+
\ No newline at end of file
diff --git a/server/src/server.ts b/server/src/server.ts
index c5306b0..dcf4005 100644
--- a/server/src/server.ts
+++ b/server/src/server.ts
@@ -6,7 +6,6 @@ import {
InitializeParams,
DidChangeConfigurationNotification,
CompletionItem,
- CompletionItemKind,
TextDocumentPositionParams,
TextDocumentSyncKind,
InitializeResult,
@@ -21,7 +20,6 @@ import * as fs from 'fs';
import {ErrorMatcher} from './ErrorMatcher';
import * as wordComplition from './wordCompletion'
import * as path from 'path';
-import { settings } from 'cluster';
@@ -147,6 +145,9 @@ documents.onDidSave(change => {
async function validateTextDocument(textDocument: TextDocument): Promise<void> {
+ globalSettings = await getDocumentSettings(textDocument.uri) // Waiting for correct setting; otherwise allways default
+
+
let documentPath:path.ParsedPath = path.parse(URI.parse(textDocument.uri).path);
let errorPath:string = documentPath.dir+'/_error.json'
@@ -160,6 +161,7 @@ async function validateTextDocument(textDocument: TextDocument): Promise<void> {
let diagnostics : Array<Diagnostic> = new Array()
let diagnosticsPromise : Promise<Set<Diagnostic>>
+ console.log(command)
if(correctPath(globalSettings.probHome))
{
exec(command, (err:string, stdout:string, stderr:string) => {
@@ -180,16 +182,16 @@ async function validateTextDocument(textDocument: TextDocument): Promise<void> {
function getCommand(documentPath : string, errorPath : string) : string{
let wdCmd = ""
let strict = ""
-
+ console.log(globalSettings.wdChecks + " " + globalSettings.strictChecks)
if(globalSettings.wdChecks){
- wdCmd = " -wd-check -release_java_parser"
+ wdCmd = " -wd-check -release_java_parser "
}
if(globalSettings.strictChecks){
- strict = " -p STRICT_CLASH_CHECKING TRUE -p TYPE_CHECK_DEFINITIONS TRUE -lint"
+ strict = " -p STRICT_CLASH_CHECKING TRUE -p TYPE_CHECK_DEFINITIONS TRUE -lint "
}
- return globalSettings.probHome + ' -p MAX_INITIALISATIONS 0 -version' + strict + wdCmd + documentPath +" -p " + "NDJSON_ERROR_LOG_FILE " + errorPath
+ return globalSettings.probHome + ' -p MAX_INITIALISATIONS 0 -version ' + strict + wdCmd + documentPath +" -p " + "NDJSON_ERROR_LOG_FILE " + errorPath
}
--
GitLab