Fix bug: POG view lock-up

Remove 5s default QuickCheck timeout and allow 0 timeout

package.json

@@ -845,7 +845,7 @@
                         "items": {
                             "type": "string"
                         },
-                        "scope": "resource",
+                        "scope": "window",
                         "markdownDescription": "Specifies additional paths to search for VDMJ extensions, i.e. plugins, libraries and annotations. Other types of extensions are not natively supported by the extension, and will need to be added to the class path through the 'Server > Class Path Additions' configuration. The paths can either point directly to an extension jar or a directory containing multiple extension jars. [Add directories to the search path](command:vdm-vscode.addExtensionJarFolders), [Add jars to the search path](command:vdm-vscode.addExtensionJars), or type a path manually."
                     },
                     "vdm-vscode.server.plugins.enabled": {

resources/schemas/schema.quickcheck.json

@@ -1 +1 @@
-{"type":"object","properties":{"config":{"type":"object","properties":{"timeout":{"type":"integer","minimum":1,"description":"The timeout of a QuickCheck execution in seconds."},"obligations":{"type":"array","items":{"type":"integer","minimum":1},"description":"A list of proof obligation indexes to run QuickCheck on. When left undefined or as an empty list, the default behavior is to check all proof obligations left after search filtering."}},"required":["timeout"],"additionalProperties":false,"description":"General configuration."},"strategies":{"type":"array","items":{"type":"object","properties":{},"additionalProperties":true,"description":"A single strategy configuration."},"description":"Configuration of QuickCheck strategies."}},"required":["config"],"additionalProperties":false,"description":"Configuration of the QuickCheck plugin.","$schema":"http://json-schema.org/draft-07/schema#"}
+{"type":"object","properties":{"config":{"type":"object","properties":{"timeout":{"type":"integer","minimum":0,"description":"The timeout of a QuickCheck execution in milliseconds."},"obligations":{"type":"array","items":{"type":"integer","minimum":1},"description":"A list of proof obligation indexes to run QuickCheck on. When left undefined or as an empty list, the default behavior is to check all proof obligations left after search filtering."}},"additionalProperties":false,"description":"General configuration."},"strategies":{"type":"array","items":{"type":"object","properties":{},"additionalProperties":true,"description":"A single strategy configuration."},"description":"Configuration of QuickCheck strategies."}},"required":["config"],"additionalProperties":false,"description":"Configuration of the QuickCheck plugin.","$schema":"http://json-schema.org/draft-07/schema#"}

src/handlers/ManagementBase.ts

@@ -0,0 +1,20 @@
+// SPDX-License-Identifier: GPL-3.0-or-later
+
+// import { Uri, WorkspaceFolder, commands, workspace } from "vscode";
+// import { ClientManager } from "../ClientManager";
+// import AutoDisposable from "../helper/AutoDisposable";
+
+// import * as Util from "../util/Util";
+
+// // TODO: Write base class with shared logic for annotations and plugins.
+// export abstract class ManagementBase extends AutoDisposable {
+//     constructor(protected readonly clientManager: ClientManager, contextKey: string, command: string) {
+//         super();
+//         commands.executeCommand("setContext", contextKey, true);
+//         Util.registerCommand(this._disposables, command, (inputUri: Uri) => this.handleManage(workspace.getWorkspaceFolder(inputUri)));
+//     }
+
+//     protected handleManage(wsFolder: WorkspaceFolder): Promise<void> {
+//         return;
+//     }
+// }

src/handlers/RTLogViewHandler.ts

@@ -160,7 +160,9 @@ export class RTLogViewHandler extends AutoDisposable {
 
     dispose() {
         // Figure out how to close the editor that showed the log view
-        this._panel.dispose();
+        if (this._panel) {
+            this._panel.dispose();
+        }
         while (this._disposables.length) {
             this._disposables.pop().dispose();
         }

src/server/ServerFactory.ts

@@ -190,7 +190,6 @@ export class ServerFactory implements Disposable {
         args.push(...["-cp", classPath, "lsp.LSPServerSocket", "-" + dialect, "-lsp", lspPort.toString(), "-dap", "0"]);
 
         // Start the LSP server
-        console.log("server args", args);
         let server = child_process.spawn(this._javaPath, args, { cwd: wsFolder.uri.fsPath });
 
         // Create output channel for server stdout

src/slsp/features/ProofObligationGenerationFeature.ts

@@ -126,7 +126,6 @@ export default class ProofObligationGenerationFeature implements StaticFeature {
             readOptionalConfiguration(wsFolder, "quickcheck.json", quickcheckConfigSchema, (config: RunQuickCheckRequestParams) => {
                 const calculatedConfig: QuickCheckConfig & { workDoneToken: string } = {
                     config: {
-                        timeout: 5,
                         obligations: poIds,
                     },
                     workDoneToken: workDoneToken,

src/slsp/views/ProofObligationPanel.ts

@@ -17,6 +17,7 @@ import {
     debug,
     ProgressLocation,
     Progress,
+    TabInputWebview,
 } from "vscode";
 import { ClientManager } from "../../ClientManager";
 import * as util from "../../util/Util";
@@ -97,6 +98,21 @@ export class ProofObligationPanel implements Disposable {
             this._onReadyCallbacks = new OnReady(resolve, reject);
         });
 
+        // Workaround to bug: https://github.com/microsoft/vscode/issues/188257
+        // disposing of the WebviewPanel on extension deactivation does not close the panel,
+        // leaving it orphaned and unresponsive when the extension activates again.
+        const orphanedTabs = window.tabGroups.all
+            .flatMap((tabGroup) => tabGroup.tabs)
+            .filter((tab) => {
+                if (tab.input instanceof TabInputWebview) {
+                    return tab.input.viewType.includes(this.viewType);
+                }
+
+                return false;
+            });
+
+        window.tabGroups.close(orphanedTabs);
+
         this._disposables.push(
             commands.registerCommand(
                 `vdm-vscode.pog.run`,
@@ -403,7 +419,9 @@ export class ProofObligationPanel implements Disposable {
         commands.executeCommand("setContext", `vdm-vscode.pog.run`, false);
 
         // Clean up our resources
-        this._panel.dispose();
+        if (this._panel) {
+            this._panel.dispose();
+        }
 
         while (this._disposables.length) {
             this._disposables.pop().dispose();

src/util/Schemas.ts

@@ -16,8 +16,9 @@ export const quickcheckConfigSchema = z
                 timeout: z
                     .number()
                     .int()
-                    .gte(1, "The timeout has to be at least 1 second.")
-                    .describe("The timeout of a QuickCheck execution in seconds."),
+                    .gte(0, "The timeout has to be at least 0 second.")
+                    .optional()
+                    .describe("The timeout of a QuickCheck execution in milliseconds."),
                 obligations: z
                     .array(z.number().int().gte(1))
                     .optional()

src/webviews/proof_obligations/ProofObligationsTable.tsx

@@ -112,8 +112,6 @@ export const ProofObligationsTable = ({
     const sortedPOs = sortPOs(pos, sortingState);
     const shouldRenderTable = !((pos.length === 0) && posInvalid)
 
-    console.log("Should render", shouldRenderTable, "because", pos.length, posInvalid)
-
     return (
         <>
             {shouldRenderTable ? (