Merge pull request #322 from tlaplus/tlaps-proof-state-v2

Adapt to changes in the lsp server.

Author: kape1395

esbuild.js

@@ -50,6 +50,19 @@ const webviewConfig = {
     }
 };
 
+/** @type BuildOptions */
+const webviewCurrentProofStepConfig = {
+    ...baseConfig,
+    target: 'es2020',
+    format: 'esm',
+    tsconfig: 'tsconfig.webview.json',
+    entryPoints: ['./src/webview/current-proof-step/main.tsx'],
+    outfile: './out/current-proof-step.js',
+    loader: {
+        '.ttf': 'copy', // use the file loader to handle .ttf files
+    }
+};
+
 const watchPlugin = (name) => [{
     name: 'watch-plugin',
     setup(build) {
@@ -66,11 +79,16 @@ const watchPlugin = (name) => [{
             (await context({...extensionConfig, plugins: watchPlugin('extensionConfig')})).watch();
             (await context({...extensionBrowserConfig, plugins: watchPlugin('extensionBrowserConfig')})).watch();
             (await context({...webviewConfig, plugins: watchPlugin('webviewConfig')})).watch();
+            (await context({
+                ...webviewCurrentProofStepConfig,
+                plugins: watchPlugin('webviewCurrentProofStepConfig')
+            })).watch();
         } else {
             // Build extension
             await build(extensionConfig);
             await build(extensionBrowserConfig);
             await build(webviewConfig);
+            await build(webviewCurrentProofStepConfig);
             console.log('build complete');
         }
     } catch (err) {

package.json

@@ -486,8 +486,8 @@
         "views": {
             "tlaplus": [
                 {
-                    "id": "tlaplus.tlaps-current-proof-obligation",
-                    "name": "Current Proof Obligation",
+                    "id": "tlaplus.current-proof-step",
+                    "name": "Current Proof Step",
                     "type": "webview"
                 }
             ]

resources/images/icons-material/README.md

@@ -0,0 +1,3 @@
+Icons for the TLAPS proof steps:
+  - These icons are downloaded from <https://fonts.google.com/icons>.
+  - The files with the suffix `-color` are manually edited to add the fill color.

resources/images/icons-material/check_box_outline_blank_FILL0_wght400_GRAD0_opsz24-color.svg

@@ -175,3 +175,24 @@ export async function exists(filePath: string): Promise<boolean> {
         fs.exists(filePath, (ex) => resolve(ex));
     });
 }
+
+// This calls only the latest of the supplied functions per specified period.
+// Used to avoid overloading the environment with too frequent events.
+export class DelayedFn {
+    private latest : (() => void) | null = null;
+    constructor(private period: number) {}
+
+    public do(f : () => void) {
+        const wasScheduled = !!this.latest;
+        this.latest = f;
+        if (!wasScheduled) {
+            setTimeout(() => {
+                const f = this.latest;
+                this.latest = null;
+                if (f) {
+                    f();
+                }
+            }, this.period);
+        }
+    }
+}

resources/images/icons-material/check_box_outline_blank_FILL0_wght400_GRAD0_opsz24.svg

@@ -27,7 +27,7 @@ import { TlaDeclarationsProvider, TlaDefinitionsProvider } from './declarations/
 import { TlaDocumentInfos } from './model/documentInfo';
 import { syncTlcStatisticsSetting, listenTlcStatConfigurationChanges } from './commands/tlcStatisticsCfg';
 import { TlapsClient } from './tlaps';
-import { TlapsProofObligationView } from './webview/tlapsCurrentProofObligationView';
+import { CurrentProofStepWebviewViewProvider } from './panels/currentProofStepWebviewViewProvider';
 
 const TLAPLUS_FILE_SELECTOR: vscode.DocumentSelector = { scheme: 'file', language: LANG_TLAPLUS };
 const TLAPLUS_CFG_FILE_SELECTOR: vscode.DocumentSelector = { scheme: 'file', language: LANG_TLAPLUS_CFG };
@@ -44,7 +44,7 @@ let tlapsClient: TlapsClient | undefined;
  * Extension entry point.
  */
 export function activate(context: vscode.ExtensionContext): void {
-    const tlapsProofObligationView = new TlapsProofObligationView();
+    const currentProofStepWebviewViewProvider = new CurrentProofStepWebviewViewProvider(context.extensionUri);
     diagnostic = vscode.languages.createDiagnosticCollection(LANG_TLAPLUS);
     context.subscriptions.push(
         vscode.commands.registerCommand(
@@ -92,7 +92,7 @@ export function activate(context: vscode.ExtensionContext): void {
         vscode.languages.registerCodeActionsProvider(
             TLAPLUS_FILE_SELECTOR,
             new TlaCodeActionProvider(),
-            { providedCodeActionKinds: [ vscode.CodeActionKind.Source ] }),
+            { providedCodeActionKinds: [vscode.CodeActionKind.Source] }),
         vscode.debug.registerDebugAdapterDescriptorFactory(
             LANG_TLAPLUS,
             new TLADebugAdapterServerDescriptorFactory()),
@@ -165,11 +165,13 @@ export function activate(context: vscode.ExtensionContext): void {
             }
         ),
         vscode.window.registerWebviewViewProvider(
-            TlapsProofObligationView.viewType,
-            tlapsProofObligationView,
+            CurrentProofStepWebviewViewProvider.viewType,
+            currentProofStepWebviewViewProvider,
         )
     );
-    tlapsClient = new TlapsClient(context, tlapsProofObligationView);
+    tlapsClient = new TlapsClient(context, details => {
+        currentProofStepWebviewViewProvider.showProofStepDetails(details);
+    });
     syncTlcStatisticsSetting()
         .catch((err) => console.error(err))
         .then(() => listenTlcStatConfigurationChanges(context.subscriptions));

resources/images/icons-material/check_circle_FILL0_wght400_GRAD0_opsz24-color.svg

@@ -1,4 +1,13 @@
-import { Location } from 'vscode-languageclient/node';
+import { Location, Range } from 'vscode-languageclient/node';
+
+export interface CountByStepStatus {
+    proved: number;
+    failed: number;
+    omitted: number;
+    missing: number;
+    pending: number;
+    progress: number;
+}
 
 export interface TlapsProofObligationResult {
     prover: string;
@@ -9,7 +18,17 @@ export interface TlapsProofObligationResult {
 }
 
 export interface TlapsProofObligationState {
-    location: Location;
-    obligation: string;
+    role: string;
+    range: Range;
+    status: string;
+    normalized: string;
     results: TlapsProofObligationResult[];
 }
+
+export interface TlapsProofStepDetails {
+    kind: string;
+    status: string;
+    location: Location;
+    obligations: TlapsProofObligationState[];
+    sub_count: CountByStepStatus;
+}