Merge pull request #319 from kape1395/tlaps-proof-state

Initial version for the proof state view.

package.json

@@ -473,7 +473,25 @@
                     "highContrast": "#d8d8d850"
                 }
             }
-        ]
+        ],
+        "viewsContainers": {
+            "activitybar": [
+                {
+                    "id": "tlaplus",
+                    "title": "TLA+",
+                    "icon": "resources/images/tlaplus.svg"
+                }
+            ]
+        },
+        "views": {
+            "tlaplus": [
+                {
+                    "id": "tlaplus.tlaps-current-proof-obligation",
+                    "name": "Current Proof Obligation",
+                    "type": "webview"
+                }
+            ]
+        }
     },
     "scripts": {
         "vscode:prepublish": "npm run compile -- --production",

src/main.ts

@@ -27,6 +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';
 
 const TLAPLUS_FILE_SELECTOR: vscode.DocumentSelector = { scheme: 'file', language: LANG_TLAPLUS };
 const TLAPLUS_CFG_FILE_SELECTOR: vscode.DocumentSelector = { scheme: 'file', language: LANG_TLAPLUS_CFG };
@@ -43,6 +44,7 @@ let tlapsClient: TlapsClient | undefined;
  * Extension entry point.
  */
 export function activate(context: vscode.ExtensionContext): void {
+    const tlapsProofObligationView = new TlapsProofObligationView();
     diagnostic = vscode.languages.createDiagnosticCollection(LANG_TLAPLUS);
     context.subscriptions.push(
         vscode.commands.registerCommand(
@@ -160,9 +162,14 @@ export function activate(context: vscode.ExtensionContext): void {
                             //   1 1 1 2
                             (wordRange.end.character /** + 1 */))) : undefined;
                 }
-            })
+            }
+        ),
+        vscode.window.registerWebviewViewProvider(
+            TlapsProofObligationView.viewType,
+            tlapsProofObligationView,
+        )
     );
-    tlapsClient = new TlapsClient(context);
+    tlapsClient = new TlapsClient(context, tlapsProofObligationView);
     syncTlcStatisticsSetting()
         .catch((err) => console.error(err))
         .then(() => listenTlcStatConfigurationChanges(context.subscriptions));

src/model/tlaps.ts

@@ -0,0 +1,15 @@
+import { Location } from 'vscode-languageclient/node';
+
+export interface TlapsProofObligationResult {
+    prover: string;
+    meth: string;
+    status: string;
+    reason: string | null;
+    obligation: string | null; // Non-null, if prover failed.
+}
+
+export interface TlapsProofObligationState {
+    location: Location;
+    obligation: string;
+    results: TlapsProofObligationResult[];
+}

src/tlaps.ts

@@ -1,3 +1,12 @@
+// TODO: Click on the proof gutter icons.
+//  - https://github.com/microsoft/vscode/issues/5455
+//  - https://github.com/microsoft/vscode/issues/175945#issuecomment-1466438453
+//
+// TODO: Tree View to show the proof.
+//  https://code.visualstudio.com/api/extension-guides/tree-view
+//  https://github.com/microsoft/vscode/issues/103403
+//  Also show WebviewView to show a custom content in a sidebar.
+//
 import * as vscode from 'vscode';
 import {
     DocumentUri,
@@ -7,6 +16,8 @@ import {
     TransportKind,
     VersionedTextDocumentIdentifier
 } from 'vscode-languageclient/node';
+import { TlapsProofObligationView } from './webview/tlapsCurrentProofObligationView';
+import { TlapsProofObligationState } from './model/tlaps';
 
 interface ProofStateMarker {
     range: vscode.Range;
@@ -29,7 +40,10 @@ export class TlapsClient {
     ];
     private proofStateDecorationTypes = new Map<string, vscode.TextEditorDecorationType>();
 
-    constructor(private context: vscode.ExtensionContext) {
+    constructor(
+        private context: vscode.ExtensionContext,
+        private tlapsProofObligationView: TlapsProofObligationView,
+    ) {
         context.subscriptions.push(vscode.commands.registerTextEditorCommand(
             'tlaplus.tlaps.check-step',
             (te, ed, args) => {
@@ -130,6 +144,12 @@ export class TlapsClient {
             'tlaplus/tlaps/proofStates',
             this.proofStateNotifHandler.bind(this)
         ));
+        this.context.subscriptions.push(this.client.onNotification(
+            'tlaplus/tlaps/currentProofObligation',
+            (oblState: TlapsProofObligationState) => {
+                this.tlapsProofObligationView.showProofObligation(oblState);
+            }
+        ));
         this.client.start();
     }
 

src/webview/tlapsCurrentProofObligationView.ts

@@ -0,0 +1,68 @@
+import * as vscode from 'vscode';
+import { TlapsProofObligationState } from '../model/tlaps';
+import { URI } from 'vscode-uri';
+
+export class TlapsProofObligationView implements vscode.WebviewViewProvider {
+    public static readonly viewType = 'tlaplus.tlaps-current-proof-obligation';
+    private view?: vscode.WebviewView;
+    private oblState: TlapsProofObligationState | null = null;
+
+    public resolveWebviewView(
+        webviewView: vscode.WebviewView,
+        _context: vscode.WebviewViewResolveContext,
+        _token: vscode.CancellationToken,
+    ) {
+        this.view = webviewView;
+        this.show();
+    }
+
+    public showProofObligation(oblState: TlapsProofObligationState | null) {
+        this.oblState = oblState;
+        this.show();
+    }
+
+    private show() {
+        if (this.view) {
+            this.view.webview.html = this.makeHtml();
+        }
+    }
+
+    private makeHtml() {
+        const header =
+            `<!DOCTYPE html>
+            <html lang="en">
+            <head>
+                <meta charset="UTF-8">
+                <meta name="viewport" content="width=device-width, initial-scale=1.0">
+                <title>Cat Coding</title>
+            </head>
+            <body>`;
+        const footer =
+            `</body>
+            </html>`;
+        let content = '<p>No obligation selected.</p>';
+        if (this.oblState) {
+            const loc = this.oblState.location;
+            const uri = URI.parse(loc.uri);
+            content = `<p>${uri.path.split(/\/|\\/).pop()}</p>`;
+            if (loc.range.start.line === loc.range.end.line) {
+                content += `<p>Line: ${loc.range.start.line}</p>`;
+            } else {
+                content += `<p>Lines: ${loc.range.start.line}-${loc.range.end.line}</p>`;
+            }
+            if (this.oblState.results) {
+                content += '<ul>';
+                this.oblState.results.forEach(r => {
+                    const reason = r.reason ? ` <span style='opacity: 0.7'>(${r.reason})</span>` : '';
+                    const meth = r.meth ? ` <span style='opacity: 0.7'>[${r.meth}]</span>` : '';
+                    content += `<li>${r.prover}${meth}: ${r.status}${reason}</li>`;
+                });
+                content += '</ul>';
+            } else {
+                content += '<p>Not checked yet.</p>';
+            }
+            content += `<pre>${this.oblState.obligation}</pre>`;
+        }
+        return header + content + footer;
+    }
+}