vscode-ext: improve "Copy Command" command and other minor stuff

moves-rwth · Dec 22, 2024 · 1438e65 · 1438e65
1 parent 7010978
commit 1438e65
Show file tree

Hide file tree

Showing 4 changed files with 9 additions and 8 deletions.
diff --git a/vscode-ext/src/CaesarClient.ts b/vscode-ext/src/CaesarClient.ts
@@ -416,11 +416,12 @@ export class CaesarClient {
             return;
         }
         const command = '"' + executable.command.replace(/(["'$`\\])/g, '\\$1') + '"';
-        let line = `${command} ${executable.args!.join(" ")}`;
+        const args = executable.args!.filter(arg => !["--language-server", "--debug"].includes(arg));
+        let line = `${command} ${args.join(" ")}`;
         let cwd = executable.options && executable.options.cwd;
         if (cwd !== undefined) {
             cwd = '"' + cwd.replace(/(["'$`\\])/g, '\\$1') + '"';
-            line = `pushd ${cwd}; ${line}; popd`;
+            line = `cd ${cwd}; ${line}`;
         }
         await vscode.env.clipboard.writeText(line);
     }

diff --git a/vscode-ext/src/ComputedPreComponent.ts b/vscode-ext/src/ComputedPreComponent.ts
@@ -70,7 +70,7 @@ export class ComputedPreComponent {
 
         // clear all information when a new verification task is started
         verifier.client.onStatusUpdate((status) => {
-            if (status == ServerStatus.Verifying) {
+            if (status === ServerStatus.Verifying) {
                 for (const [_document, results] of this.computedPres.entries()) {
                     results.length = 0;
                 }

diff --git a/vscode-ext/src/GutterStatusComponent.ts b/vscode-ext/src/GutterStatusComponent.ts
@@ -41,7 +41,7 @@ export class GutterStatusComponent {
 
         // listen to status and verify updates
         verifier.client.onStatusUpdate((status) => {
-            if (status == ServerStatus.Verifying) {
+            if (status === ServerStatus.Verifying) {
                 for (const [_document, results] of this.status.entries()) {
                     results.length = 0;
                 }

diff --git a/vscode-ext/src/StatusBarComponent.ts b/vscode-ext/src/StatusBarComponent.ts
@@ -20,7 +20,7 @@ const stoppedTooltipMenu =
 export class StatusBarComponent {
 
     private enabled: boolean;
-    private verifyStatus: DocumentMap<[Range, VerifyResult][]> = new DocumentMap();
+    private verifyStatus = new DocumentMap<[Range, VerifyResult][]>();
     private serverStatus: ServerStatus = ServerStatus.NotStarted;
     private view: StatusBarItem;
 
@@ -95,7 +95,7 @@ export class StatusBarComponent {
                     break;
                 case ServerStatus.Starting:
                     viewText = "$(loading~spin) Starting Caesar...";
-                    command = "caesar.showOutput"
+                    command = "caesar.showOutput";
                     break;
                 case ServerStatus.Ready:
                     [viewText, tooltipStatusText] = this.getReadyStatusView();
@@ -104,7 +104,7 @@ export class StatusBarComponent {
                     break;
                 case ServerStatus.Verifying:
                     viewText = "$(sync~spin) Verifying...";
-                    command = "caesar.showOutput"
+                    command = "caesar.showOutput";
                     break;
             }
 
@@ -150,7 +150,7 @@ export class StatusBarComponent {
 
             const results = this.verifyStatus.get(document_id);
 
-            if (results === undefined) throw new Error("No verify results found for document: " + document_id);
+            if (results === undefined) { throw new Error("No verify results found for document: " + document_id.uri); }
 
             let verified = 0;
             let failed = 0;