Fix #246

client/package.json

@@ -1,7 +1,7 @@
 {
     "name": "viper",
     "displayName": "Viper",
-    "version": "2.4.0",
+    "version": "2.4.1",
     "publisher": "viper-admin",
     "description": "This extension provides interactive IDE features for verifying programs in Viper (Verification Infrastructure for Permission-based Reasoning).",
     "license": "SEE LICENSE IN LICENSE.txt",

client/src/ExtensionState.ts

@@ -204,7 +204,7 @@ export class State {
             }
         }
 
-        State.client = new LanguageClient('languageServer', 'Language Server', serverOptions, clientOptions, brk);
+        State.client = new LanguageClient('languageServer', 'Viper Language Server', serverOptions, clientOptions, brk);
 
         Log.log("Start Language Server", LogLevel.Info);
         // Create the language client and start the client.

server/src/ServerClass.ts

@@ -46,37 +46,35 @@ export class Server {
         else return null;
     }
 
-    static refreshEndings(): Promise<boolean> {
-        return new Promise((resolve, reject) => {
-            Server.connection.sendRequest(Commands.GetViperFileEndings).then((endings: string[]) => {
-                this.viperFileEndings = endings;
-                resolve(true);
-            }, err => {
-                Log.error("GetViperFileEndings request was rejected by the client: " + err);
-            });
-        });
+    static async refreshEndings(): Promise<boolean> {
+        try {
+            const endings: string[] = await Server.connection.sendRequest(Commands.GetViperFileEndings);
+            this.viperFileEndings = endings;
+            return true;
+        } catch (err) {
+            const msg = `GetViperFileEndings request was rejected by the client: ${err}`;
+            Log.error(msg);
+            // rethrow error:
+            throw new Error(msg);
+        }
     }
 
-    static isViperSourceFile(uri: string, firstTry: boolean = true): Promise<boolean> {
-        return new Promise((resolve, reject) => {
-            if (!this.viperFileEndings) {
-                if (firstTry) {
-                    Log.log("Refresh the viper file endings.", LogLevel.Debug);
-                    this.refreshEndings().then(() => {
-                        this.isViperSourceFile(uri, false).then(success => {
-                            resolve(success)
-                        });
-                    })
-                } else {
-                    resolve(false);
-                }
+    static async isViperSourceFile(uri: string, firstTry: boolean = true): Promise<boolean> {
+        if (!this.viperFileEndings) {
+            if (firstTry) {
+                Log.log("Refresh the viper file endings.", LogLevel.Debug);
+                await this.refreshEndings();
+                const success = await this.isViperSourceFile(uri, false);
+                return success;
             } else {
-                resolve(this.viperFileEndings.some(globPattern => {
-                    let regex = globToRexep(globPattern);
-                    return regex.test(uri);
-                }));
+                return false;
             }
-        });
+        } else {
+            return this.viperFileEndings.some(globPattern => {
+                const regex = globToRexep(globPattern);
+                return regex.test(uri);
+            });
+        }
     }
 
     static showHeap(task: VerificationTask, clientIndex: number, isHeapNeeded: boolean) {
@@ -275,11 +273,10 @@ export class Server {
         // ensureViperTools is not already ongoing, start it:
         cachedPromise = this.internalEnsureViperTools(shouldUpdate);
         this.cacheInternalEnsureViperTools = cachedPromise;
+        const loc = await cachedPromise;
         // reset cache when operation is done:
-        return cachedPromise.then(loc => {
-            this.cacheInternalEnsureViperTools = null;
-            return loc;
-        });
+        this.cacheInternalEnsureViperTools = null;
+        return loc;
     }
 
     private static async internalEnsureViperTools(shouldUpdate: boolean): Promise<Location> {
@@ -310,7 +307,8 @@ export class Server {
             const errMsg = `Error installing Viper tools: ${e}`;
             Log.error(errMsg);
             Server.connection.sendNotification(Commands.ViperUpdateComplete, false); //update failed
-            return Promise.reject(errMsg);
+            // rethrow error:
+            throw new Error(errMsg);
         }
     }
 

server/src/Settings.ts

@@ -177,9 +177,8 @@ export class Settings {
         return Settings.settings.verificationBackends.find(b => { return b.name == backendName });
     }
 
-    public static valid(): boolean {
-        Server.sendSettingsCheckedNotification({ ok: this._valid, errors: this._errors, settings: this.settings });
-        return this._valid;
+    public static getErrors(): SettingsError[] {
+        return this._errors;
     }
 
     public static upToDate(): boolean {
@@ -208,9 +207,9 @@ export class Settings {
 
     //tries to restart backend, 
     public static async initiateBackendRestartIfNeeded(oldSettings?: ViperSettings, selectedBackend?: string, viperToolsUpdated: boolean = false): Promise<void> {
-        await Settings.checkSettings(viperToolsUpdated);
-        if (Settings.valid()) {
-            let newBackend = Settings.selectBackend(Settings.settings, selectedBackend);
+        const valid = await Settings.checkSettings(viperToolsUpdated);
+        if (valid) {
+            const newBackend = Settings.selectBackend(Settings.settings, selectedBackend);
 
             if (newBackend) {
                 //only restart the backend after settings changed if the active backend was affected
@@ -239,7 +238,7 @@ export class Settings {
                 Log.error("No backend, even though the setting check succeeded.");
             }
         } else {
-            Server.backendService.stop();
+            await Server.backendService.stop();
         }
     }
 
@@ -328,10 +327,10 @@ export class Settings {
             if (!resolvedPath.exists) {
                 if (!viperToolsUpdated) {
                     //Automatically install the Viper tools
-                    Server.ensureViperTools(false);
+                    await Server.ensureViperTools(false);
                     // in this case we do not want to continue restarting the backend,
-                    //the backend will be restarted after the update
-                    return Promise.reject();
+                    // the backend will be restarted after the update
+                    return true;
                 } else {
                     // we have just updated Viper tools but the resolved path still does not exist
                     return false;
@@ -409,6 +408,11 @@ export class Settings {
         }
     }
 
+    /** requires that `checkSettings` has recently been executed */
+    public static sendErrorsToClient(): void {
+        Server.sendSettingsCheckedNotification({ ok: this._valid, errors: this._errors, settings: this.settings });
+    }
+
     private static mergeBackend(custom: Backend, def: Backend) {
         if (!custom || !def || custom.name != def.name) return;
         if (!custom.paths) custom.paths = def.paths;

server/src/ViperServerService.ts

@@ -335,7 +335,7 @@ export class ViperServerService extends BackendService {
             }
 
             if ( message.msg_type.includes('warning') && message.msg_body.length > 0 ) {
-                Log.error(`ViperServer reports the following warning: ${message.msg_body.message}`, LogLevel.Default)
+                Log.log(`ViperServer reports the following warning: ${JSON.stringify(message.msg_body)}`, LogLevel.Default)
                 let label = message.msg_type.includes('internal') 
                     ? 'internal' 
                     : message.msg_type.includes('parser')