lsp server: fix response sending order

src/servers/lsp.rs

@@ -249,6 +249,17 @@ impl LspServer {
         Ok(())
     }
 
+    fn handle_timeout_for_results(&mut self) -> Result<(), ServerError> {
+        self.statuses.iter_mut().for_each(|(_, status)| {
+            // If status is Todo convert it to Timeout
+            if let VerifyResult::Todo = status {
+                *status = VerifyResult::Timeout;
+            }
+        });
+        self.publish_verify_statuses()?;
+        Ok(())
+    }
+
     fn clear_file_information(&mut self, file_id: &FileId) -> Result<(), ServerError> {
         if let Some(diag) = self.diagnostics.get_mut(file_id) {
             diag.clear();
@@ -317,6 +328,8 @@ impl Server for LspServer {
 
     fn register_source_unit(&mut self, span: Span) -> Result<(), VerifyError> {
         self.statuses.insert(span, VerifyResult::Todo);
+        self.publish_verify_statuses()
+            .map_err(VerifyError::ServerError)?;
         Ok(())
     }
 
@@ -440,29 +453,35 @@ async fn handle_verify_request(
     };
 
     let result = verify(&[file_id]).await;
-    let res = match &result {
-        Ok(_) => Response::new_ok(id, Value::Null),
-        Err(err) => Response::new_err(id, 0, format!("{}", err)),
-    };
-    sender
-        .send(Message::Response(res))
-        .map_err(|e| VerifyError::ServerError(e.into()))?;
+
     match result {
-        Ok(()) => {}
-        Err(VerifyError::Diagnostic(diagnostic)) => {
-            server.lock().unwrap().add_diagnostic(diagnostic)?;
+        Ok(()) => {
+            let response = Message::Response(Response::new_ok(id, Value::Null));
+            sender
+                .send(response)
+                .map_err(|e| VerifyError::ServerError(e.into()))?;
         }
-        Err(VerifyError::Interrupted) | Err(VerifyError::LimitError(_)) => {
-            // If the verification is interrupted or a limit is reached before the verification starts, no verification statuses are published yet.
-            // In this case, the client needs to be notified about the registered source units that are not checked yet (marked with VerifyResult::Todo).
-            // This acts as a fallback mechanism for this case.
-            server
-                .lock()
-                .unwrap()
-                .publish_verify_statuses()
-                .map_err(VerifyError::ServerError)?;
+
+        Err(err) => {
+            let response = Response::new_err(id, 0, format!("{}", err));
+            match err {
+                VerifyError::Diagnostic(diagnostic) => {
+                    server.lock().unwrap().add_diagnostic(diagnostic)?;
+                }
+                VerifyError::Interrupted | VerifyError::LimitError(_) => {
+                    server
+                        .lock()
+                        .unwrap()
+                        .handle_timeout_for_results()
+                        .map_err(VerifyError::ServerError)?;
+                }
+                _ => {}
+            }
+
+            sender
+                .send(Message::Response(response))
+                .map_err(|e| VerifyError::ServerError(e.into()))?;
         }
-        Err(err) => Err(err)?,
     }
     Ok(())
 }

src/servers/mod.rs

@@ -35,6 +35,7 @@ pub enum VerifyResult {
     Verified,
     Failed,
     Unknown,
+    Timeout,
 }
 
 impl VerifyResult {

vscode-ext/src/CaesarClient.ts

@@ -25,7 +25,8 @@ export enum VerifyResult {
     Todo = "todo",
     Verified = "verified",
     Failed = "failed",
-    Unknown = "unknown"
+    Unknown = "unknown",
+    Timeout = "timeout"
 }
 
 export interface VerifyStatusNotification {

vscode-ext/src/GutterStatusComponent.ts

@@ -11,22 +11,38 @@ export class GutterStatusComponent {
     private enabled: boolean;
     private status: DocumentMap<[Range, VerifyResult][]>;
     private serverStatus: ServerStatus = ServerStatus.NotStarted;
+    private gutterAnimator: GutterAnimator;
 
     private verifyDecType: vscode.TextEditorDecorationType;
     private failedDecType: vscode.TextEditorDecorationType;
     private unknownDecType: vscode.TextEditorDecorationType;
+    private timeoutDecType: vscode.TextEditorDecorationType;
 
     constructor(verifier: Verifier) {
-        // create decorations
+
+        // Load the fixed decoration types
         this.verifyDecType = vscode.window.createTextEditorDecorationType({ gutterIconSize: "contain", gutterIconPath: verifier.context.asAbsolutePath('images/verified.png') });
         this.failedDecType = vscode.window.createTextEditorDecorationType({ gutterIconSize: "contain", gutterIconPath: verifier.context.asAbsolutePath('images/failed.png') });
         this.unknownDecType = vscode.window.createTextEditorDecorationType({ gutterIconSize: "contain", gutterIconPath: verifier.context.asAbsolutePath('images/unknown.png') });
+        this.timeoutDecType = vscode.window.createTextEditorDecorationType({ gutterIconSize: "contain", gutterIconPath: verifier.context.asAbsolutePath('images/timeout.png') });
+
+        // Load the animation frames
+        let frameDecorationMap: Map<number, vscode.TextEditorDecorationType> = new Map();
+        for (let i = 0; i < 8; i++) {
+            let decType = vscode.window.createTextEditorDecorationType({ gutterIconSize: "contain", gutterIconPath: verifier.context.asAbsolutePath(`images/gutterAnimation/${i}.png`) });
+            frameDecorationMap.set(i, decType);
+        }
 
         // render if enabled
         this.enabled = GutterInformationViewConfig.get(ConfigurationConstants.showGutterIcons);
 
         this.status = new DocumentMap();
 
+        this.gutterAnimator = new GutterAnimator(frameDecorationMap);
+
+        // Editor context subscriptions:
+        // ----------------------------
+
         // subscribe to config changes
         verifier.context.subscriptions.push(vscode.workspace.onDidChangeConfiguration((e: vscode.ConfigurationChangeEvent) => {
             if (GutterInformationViewConfig.isAffected(e)) {
@@ -40,6 +56,16 @@ export class GutterStatusComponent {
             this.render();
         }));
 
+
+        verifier.context.subscriptions.push(vscode.workspace.onDidCloseTextDocument((document) => {
+            const documentIdentifier: TextDocumentIdentifier = { uri: document.uri.toString() };
+            this.status.remove(documentIdentifier);
+            this.render();
+        }));
+
+        // Server context subscriptions:
+        // ----------------------------
+
         // listen to status and verify updates
         verifier.client.onStatusUpdate((status) => {
             this.serverStatus = status;
@@ -56,14 +82,11 @@ export class GutterStatusComponent {
             this.render();
         });
 
-        verifier.context.subscriptions.push(vscode.workspace.onDidCloseTextDocument((document) => {
-            const documentIdentifier: TextDocumentIdentifier = { uri: document.uri.toString() };
-            this.status.remove(documentIdentifier);
-            this.render();
-        }));
     }
 
     render() {
+        let loadingEditorRangeMap: Map<vscode.TextEditor, vscode.Range[]> = new Map();
+
         for (const editor of vscode.window.visibleTextEditors) {
             for (const [document_id, results] of this.status.entries()) {
 
@@ -74,6 +97,9 @@ export class GutterStatusComponent {
                 const verifiedProcs: vscode.DecorationOptions[] = [];
                 const failedProcs: vscode.DecorationOptions[] = [];
                 const unknownProcs: vscode.DecorationOptions[] = [];
+                const timeoutProcs: vscode.DecorationOptions[] = [];
+
+                const todoProcs: Range[] = [];
 
                 if (this.enabled) {
                     for (const [range, result] of results) {
@@ -82,10 +108,14 @@ export class GutterStatusComponent {
 
                         switch (result) {
                             case VerifyResult.Todo:
-                                // Only show unknown icon if the verification process is ended but this is still a Todo.
                                 if (this.serverStatus === ServerStatus.Ready) {
+                                    // If the server stopped verfying, but this is still todo, mark as unknown
+                                    // This should not happen since the server converts todos to timeouts when it stops verifying
                                     unknownProcs.push({ range: gutterRange, hoverMessage: 'Unknown' });
                                 }
+
+                                // Add to the todo list to be animated
+                                todoProcs.push(range);
                                 break;
                             case VerifyResult.Verified:
                                 verifiedProcs.push({ range: gutterRange, hoverMessage: 'Verified' });
@@ -96,13 +126,79 @@ export class GutterStatusComponent {
                             case VerifyResult.Unknown:
                                 unknownProcs.push({ range: gutterRange, hoverMessage: 'Unknown' });
                                 break;
+                            case VerifyResult.Timeout:
+                                timeoutProcs.push({ range: gutterRange, hoverMessage: 'Timeout' });
                         }
                     }
                 }
+                loadingEditorRangeMap.set(editor, todoProcs);
+
                 editor.setDecorations(this.verifyDecType, verifiedProcs);
                 editor.setDecorations(this.failedDecType, failedProcs);
                 editor.setDecorations(this.unknownDecType, unknownProcs);
+                editor.setDecorations(this.timeoutDecType, timeoutProcs);
             }
         }
+        this.gutterAnimator.setEditorRangemap(loadingEditorRangeMap);
+
+    }
+}
+
+class GutterAnimator {
+    private frame = 0;
+    private interval: NodeJS.Timeout | undefined;
+
+    private editorRangeMap: Map<vscode.TextEditor, vscode.Range[]> = new Map();
+
+    constructor(private readonly frameDecorationMap: Map<number, vscode.TextEditorDecorationType>, private readonly intervalSpeed: number = 75) {
+    }
+
+    startAnimation() {
+        if (this.interval === undefined) {
+            this.interval = setInterval(() => {
+                this.frame = (this.frame + 1) % this.frameDecorationMap.size;
+                this.render();
+            }, this.intervalSpeed);
+        }
+    }
+
+    stopAnimation() {
+        if (this.interval !== undefined) {
+            clearInterval(this.interval);
+            this.interval = undefined;
+        }
+    }
+
+    setEditorRangemap(editorRangeMap: Map<vscode.TextEditor, vscode.Range[]>) {
+        this.editorRangeMap = editorRangeMap;
+        if (Array.from(editorRangeMap.values()).every(ranges => ranges.length == 0)) {
+            // Animation is not needed if there are no ranges to animate
+            this.stopAnimation();
+            // Render to clear the decorations
+            this.render();
+        } else {
+            // If the animation is still running, it won't be restarted internally 
+            // so it is safe to call startAnimation multiple times
+            this.startAnimation();
+        }
+
+    }
+
+    render() {
+        // const decorations = this.frameDecorationMap.get(this.frame) ?? [];
+        // for each decoration type in the map
+        for (const [frame, decType] of this.frameDecorationMap) {
+            for (const [editor, ranges] of this.editorRangeMap) {
+                // if the frame is the current frame
+                if (frame === this.frame) {
+                    // set the decorations
+                    editor.setDecorations(decType, ranges.map(range => ({ range: range, hoverMessage: 'Pending' })));
+                } else {
+                    // clear the decorations for other frames
+                    editor.setDecorations(decType, []);
+                }
+            }
+
+        }
     }
 }

vscode-ext/src/StatusBarComponent.ts

@@ -174,6 +174,10 @@ export class StatusBarComponent {
                     case VerifyResult.Unknown:
                         unknown++;
                         break;
+                    case VerifyResult.Timeout:
+                        // For now we treat timeouts as unknowns in the status bar.
+                        unknown++;
+                        break;
                 }
             }
             if (failed > 0 || unknown > 0) {