Make proof step details look nicer.

Signed-off-by: Karolis Petrauskas <k.petrauskas@gmail.com>
tlaplus · Jan 28, 2024 · 3308eb4 · 3308eb4
1 parent 1ca8a75
commit 3308eb4
Show file tree

Hide file tree

Showing 16 changed files with 109 additions and 165 deletions.
diff --git a/resources/images/icons-adhoc/tlaps-proof-state-failed.svg b/resources/images/icons-adhoc/tlaps-proof-state-failed.svg
diff --git a/resources/images/icons-adhoc/tlaps-proof-state-missing.svg b/resources/images/icons-adhoc/tlaps-proof-state-missing.svg
diff --git a/resources/images/icons-adhoc/tlaps-proof-state-omitted.svg b/resources/images/icons-adhoc/tlaps-proof-state-omitted.svg
diff --git a/resources/images/icons-adhoc/tlaps-proof-state-pending.svg b/resources/images/icons-adhoc/tlaps-proof-state-pending.svg
diff --git a/resources/images/icons-adhoc/tlaps-proof-state-progress.svg b/resources/images/icons-adhoc/tlaps-proof-state-progress.svg
diff --git a/resources/images/icons-adhoc/tlaps-proof-state-proved.svg b/resources/images/icons-adhoc/tlaps-proof-state-proved.svg
diff --git a/src/model/tlaps.ts b/src/model/tlaps.ts
@@ -20,6 +20,7 @@ export interface TlapsProofObligationResult {
 export interface TlapsProofObligationState {
     role: string;
     range: Range;
+    status: string;
     normalized: string;
     results: TlapsProofObligationResult[];
 }

diff --git a/src/panels/currentProofStepWebviewViewProvider.ts b/src/panels/currentProofStepWebviewViewProvider.ts
@@ -4,21 +4,24 @@ import { getNonce } from './utilities/getNonce';
 import { getUri } from './utilities/getUri';
 import { revealFile } from './utilities/workspace';
 import { Location } from 'vscode-languageclient';
+import { ProofStateIcons, proofStateIcons, proofStateNames } from '../tlaps';
 
 export class CurrentProofStepWebviewViewProvider implements vscode.WebviewViewProvider {
     public static readonly viewType = 'tlaplus.current-proof-step';
     private view: vscode.WebviewView | null = null;
+    private context: vscode.WebviewViewResolveContext | null = null;
 
     constructor(
         private readonly extensionUri: vscode.Uri
     ) { }
 
     public resolveWebviewView(
-        webviewView: vscode.WebviewView,
-        _context: vscode.WebviewViewResolveContext,
+        view: vscode.WebviewView,
+        context: vscode.WebviewViewResolveContext,
         _token: vscode.CancellationToken,
     ) {
-        this.view = webviewView;
+        this.context = context;
+        this.view = view;
         this.view.webview.options = { enableScripts: true };
         this.view.webview.html = this.makeHtml(this.view.webview);
         this.view.webview.onDidReceiveMessage(message => this.onMessage(message));
@@ -52,6 +55,15 @@ export class CurrentProofStepWebviewViewProvider implements vscode.WebviewViewPr
         const styleUri = getUri(webview, this.extensionUri, ['out', 'current-proof-step.css']);
         const nonce = getNonce();
 
+        const webviewProofStateNames = Object.values(proofStateNames);
+        const webviewProofStateIcons: ProofStateIcons = {};
+        Object.values(proofStateNames).forEach(stateName => {
+            const localPath = proofStateIcons[stateName];
+            const onDiskPath = vscode.Uri.joinPath(this.extensionUri, localPath);
+            const onViewPath = webview.asWebviewUri(onDiskPath);
+            webviewProofStateIcons[stateName] = onViewPath.toString();
+        });
+
         // Tip: Install the es6-string-html VS Code extension to enable code highlighting below
         /* eslint-disable max-len */
         return /*html*/ `
@@ -60,9 +72,13 @@ export class CurrentProofStepWebviewViewProvider implements vscode.WebviewViewPr
             <head>
                 <meta charset="UTF-8">
                 <meta name="viewport" content="width=device-width, initial-scale=1.0">
-                <meta http-equiv="Content-Security-Policy" content="default-src 'none'; style-src ${webview.cspSource}; font-src ${webview.cspSource}; script-src 'nonce-${nonce}';">
+                <meta http-equiv="Content-Security-Policy" content="default-src ${webview.cspSource}; style-src ${webview.cspSource}; font-src ${webview.cspSource}; script-src 'nonce-${nonce}';">
                 <link rel="stylesheet" href="${styleUri}">
                 <title>Current proof step</title>
+                <script nonce="${nonce}">
+                    const webviewProofStateNames = ${JSON.stringify(webviewProofStateNames)};
+                    const webviewProofStateIcons = ${JSON.stringify(webviewProofStateIcons)};
+                </script>
             </head>
             <body>
                 <div id="root"></div>

diff --git a/src/tlaps.ts b/src/tlaps.ts
@@ -3,14 +3,11 @@
 //  - 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.
+//  - https://code.visualstudio.com/api/extension-guides/tree-view
+//  - https://github.com/microsoft/vscode/issues/103403
 //
 // TODO: Links to the proof steps: DocumentLinkProvider<T>
 //
-// TODO: Links from the side pane: TextEditor.revealRange(range: Range, revealType?: TextEditorRevealType): void
-//
 import * as vscode from 'vscode';
 import {
     DocumentUri,
@@ -24,6 +21,28 @@ import {
 import { TlapsProofStepDetails } from './model/tlaps';
 import { DelayedFn } from './common';
 
+export enum proofStateNames {
+    proved = 'proved',
+    failed = 'failed',
+    omitted = 'omitted',
+    missing = 'missing',
+    pending = 'pending',
+    progress = 'progress',
+}
+
+export type ProofStateIcons = {
+    [key : string]: string;
+}
+
+export const proofStateIcons = {
+    proved: 'resources/images/icons-material/check_circle_FILL0_wght400_GRAD0_opsz24-color.svg',
+    failed: 'resources/images/icons-material/close_FILL0_wght400_GRAD0_opsz24-color.svg',
+    omitted: 'resources/images/icons-material/editor_choice_FILL0_wght400_GRAD0_opsz24-color.svg',
+    missing: 'resources/images/icons-material/check_box_outline_blank_FILL0_wght400_GRAD0_opsz24-color.svg',
+    pending: 'resources/images/icons-material/help_FILL0_wght400_GRAD0_opsz24-color.svg',
+    progress: 'resources/images/icons-material/more_horiz_FILL0_wght400_GRAD0_opsz24-color.svg',
+} as ProofStateIcons;
+
 interface ProofStepMarker {
     status: string;
     range: vscode.Range;
@@ -35,32 +54,7 @@ export class TlapsClient {
     private configEnabled = false;
     private configCommand = [] as string[];
     private configWholeLine = true;
-    private proofStateNames = [
-        'proved',
-        'failed',
-        'omitted',
-        'missing',
-        'pending',
-        'progress',
-    ];
     private proofStateDecorationTypes = new Map<string, vscode.TextEditorDecorationType>();
-    private iconsAdhoc = new Map<string, string>(Object.entries({
-        proved: 'icons-adhoc/tlaps-proof-state-proved.svg',
-        failed: 'icons-adhoc/tlaps-proof-state-failed.svg',
-        omitted: 'icons-adhoc/tlaps-proof-state-omitted.svg',
-        missing: 'icons-adhoc/tlaps-proof-state-missing.svg',
-        pending: 'icons-adhoc/tlaps-proof-state-pending.svg',
-        progress: 'icons-adhoc/tlaps-proof-state-progress.svg',
-    }));
-    private iconsMaterial = new Map<string, string>(Object.entries({
-        proved: 'icons-material/check_circle_FILL0_wght400_GRAD0_opsz24-color.svg',
-        failed: 'icons-material/close_FILL0_wght400_GRAD0_opsz24-color.svg',
-        omitted: 'icons-material/editor_choice_FILL0_wght400_GRAD0_opsz24-color.svg',
-        missing: 'icons-material/check_box_outline_blank_FILL0_wght400_GRAD0_opsz24-color.svg',
-        pending: 'icons-material/help_FILL0_wght400_GRAD0_opsz24-color.svg',
-        progress: 'icons-material/more_horiz_FILL0_wght400_GRAD0_opsz24-color.svg',
-    }));
-    private icons = this.iconsMaterial;
 
     constructor(
         private context: vscode.ExtensionContext,
@@ -126,7 +120,7 @@ export class TlapsClient {
 
     private makeDecoratorTypes() {
         this.proofStateDecorationTypes.clear();
-        this.proofStateNames.forEach(name => {
+        Object.values(proofStateNames).forEach(name => {
             const color = { 'id': 'tlaplus.tlaps.proofState.' + name };
             const bgColor = name === 'failed' ? { backgroundColor: color } : undefined;
             const decTypeFirst = vscode.window.createTextEditorDecorationType({
@@ -136,7 +130,7 @@ export class TlapsClient {
                 dark: bgColor,
                 isWholeLine: this.configWholeLine,
                 rangeBehavior: vscode.DecorationRangeBehavior.ClosedOpen,
-                gutterIconPath: this.context.asAbsolutePath(`resources/images/${this.icons.get(name)}`),
+                gutterIconPath: this.context.asAbsolutePath(proofStateIcons[name]),
                 gutterIconSize: '100%',
             });
             const decTypeNext = vscode.window.createTextEditorDecorationType({

diff --git a/src/webview/current-proof-step/main.tsx b/src/webview/current-proof-step/main.tsx
@@ -5,6 +5,7 @@ import { Obligation } from './obligation/index.tsx';
 import { StepCounts } from './stepCounts/index.tsx';
 import { VSCodeLink } from '@vscode/webview-ui-toolkit/react/index';
 import { vscodeClient } from './vscode_client.ts';
+import { ProofStatusIcon } from './proofStatusIcon/index.tsx';
 import '@vscode/codicons/dist/codicon.css';
 
 interface CurrentProofStepViewAppI { details: TlapsProofStepDetails | null }
@@ -26,13 +27,14 @@ const CurrentProofStepViewApp = React.memo(({ details }: CurrentProofStepViewApp
             <React.StrictMode>
                 <section>
                     <div>
-                        <b>{stepKind(details.kind)}</b>&nbsp;at&nbsp;
+                        <b>{stepKind(details.kind)}</b>&nbsp;
+                        <ProofStatusIcon proofStatus={details.status}></ProofStatusIcon>
+                        &nbsp;at&nbsp;
                         <VSCodeLink onClick={() => vscodeClient.showLocation(details.location)}>
                             {details.location.uri.split(/\/|\\/).pop()}&nbsp;
                             {details.location.range.start.line + 1}:
                             {details.location.range.start.character + 1}
                         </VSCodeLink>
-                        &nbsp;-&nbsp;<b>{details.status}</b>
                     </div>
                     <StepCounts label={subLabel} counts={details.sub_count}></StepCounts>
                 </section>

diff --git a/src/webview/current-proof-step/obligation/index.css b/src/webview/current-proof-step/obligation/index.css
@@ -5,3 +5,15 @@
 .role-other {
     color: #8b9eaa;
 }
+
+.prover-list {
+    list-style-type: none;
+    list-style-position: outside;
+    padding-left: 10px;
+}
+
+.obl-text {
+    margin-left: 10px;
+    padding-left: 2px;
+    border-left: 1px solid #ffffff10;
+}
diff --git a/src/webview/current-proof-step/obligation/index.tsx b/src/webview/current-proof-step/obligation/index.tsx
@@ -3,30 +3,40 @@ import { TlapsProofObligationState, TlapsProofStepDetails } from '../../../model
 import { VSCodeLink } from '@vscode/webview-ui-toolkit/react/index';
 import { vscodeClient } from '../vscode_client.ts';
 import { Location } from 'vscode-languageclient';
+import { ProofStatusIcon } from '../proofStatusIcon/index.tsx';
 import './index.css';
 
 interface ObligationI { details: TlapsProofStepDetails; obligation: TlapsProofObligationState }
 export const Obligation = React.memo(({ details, obligation }: ObligationI) => {
     const location = { uri: details.location.uri, range: obligation.range } as Location;
     const showLocation = () => vscodeClient.showLocation(location);
     const results = obligation.results && obligation.results.length > 0
-        ? <ul>{obligation.results.map(r => {
-            const reason = r.reason ? <span className='comment'>({r.reason})</span> : null;
+        ? <ul className='prover-list'>{obligation.results.map(r => {
+            const reason = r.reason ? (<>:<br /><span className='comment'>({r.reason})</span></>) : null;
             const meth = r.meth ? <span className='comment'>[{r.meth}]</span> : null;
-            return (<li>{r.prover}{meth}:<br />{r.status}{reason}</li>);
+            return (
+                <li>
+                    <ProofStatusIcon proofStatus={r.status}></ProofStatusIcon>&nbsp;
+                    {r.prover}{meth}{reason}
+                </li>
+            );
         })}</ul>
-        : <p>Not checked yet.</p>;
+        : null;
     return (
-        <section className={ obligation.role === 'main' ? 'role-main' : 'role-other'}>
+        <section className={obligation.role === 'main' ? 'role-main' : 'role-other'}>
             <div>
                 <div>
-                    <b>Obligation {obligation.role === 'main' ? null : <span>[{obligation.role}]</span>} at</b>&nbsp;
+                    <b>
+                        Obligation
+                        {obligation.role === 'main' ? null : <span>[{obligation.role}]</span>}&nbsp;
+                        <ProofStatusIcon proofStatus={obligation.status}></ProofStatusIcon>
+                    </b>&nbsp;at&nbsp;
                     <VSCodeLink onClick={showLocation}>
                         {obligation.range.start.line + 1}:{obligation.range.start.character + 1}
                     </VSCodeLink>
                 </div>
                 {results}
-                <pre>{obligation.normalized}</pre>
+                <pre className='obl-text'>{obligation.normalized}</pre>
             </div>
         </section>
     );

diff --git a/src/webview/current-proof-step/proofStatusIcon/index.css b/src/webview/current-proof-step/proofStatusIcon/index.css
diff --git a/src/webview/current-proof-step/proofStatusIcon/index.tsx b/src/webview/current-proof-step/proofStatusIcon/index.tsx
@@ -0,0 +1,20 @@
+import * as React from 'react';
+import './index.css';
+import { proofStateIcons } from '../vscode_client';
+
+interface ProofStatusIconI { proofStatus: string }
+export const ProofStatusIcon = React.memo(({ proofStatus }: ProofStatusIconI) => {
+    const style = {
+        height: '14px',
+        width: '14px',
+        'vertical-align': '-15%',
+    };
+    return (
+        <img
+            style={style}
+            src={proofStateIcons[proofStatus]}
+            alt={proofStatus}
+            title={proofStatus}>
+        </img>
+    );
+});