Use decorators to present proof states.

Signed-off-by: Karolis Petrauskas <k.petrauskas@gmail.com>

.vscode/cspell.json

@@ -1,9 +1,12 @@
 {
     "words": [
         "tlaplus",
+        "pluscal",
         "tlaps",
         "tlapm",
         "sany",
+        "opam",
+        "pdflatex",
         "checkndebug",
         "evaluatable"
     ]

package.json

@@ -411,7 +411,63 @@
                 "editor.formatOnType": true,
                 "editor.detectIndentation": false
             }
-        }
+        },
+        "colors": [
+            {
+                "id": "tlaplus.tlaps.proofState.proved",
+                "description": "Background for a proved sequent.",
+                "defaults": {
+                    "dark": "#00ff0020",
+                    "light": "#00ff0020",
+                    "highContrast": "#00ff0050"
+                }
+            },
+            {
+                "id": "tlaplus.tlaps.proofState.failed",
+                "description": "Background for a failed to prove sequent.",
+                "defaults": {
+                    "dark": "#ff000030",
+                    "light": "#ff000030",
+                    "highContrast": "#ff000060"
+                }
+            },
+            {
+                "id": "tlaplus.tlaps.proofState.omitted",
+                "description": "Background for a sequent with omitted proof.",
+                "defaults": {
+                    "dark": "#c8ff0020",
+                    "light": "#c8ff0020",
+                    "highContrast": "#c8ff0050"
+                }
+            },
+            {
+                "id": "tlaplus.tlaps.proofState.missing",
+                "description": "Background for a sequent with no proof.",
+                "defaults": {
+                    "dark": "#c8ff0020",
+                    "light": "#c8ff0020",
+                    "highContrast": "#c8ff0050"
+                }
+            },
+            {
+                "id": "tlaplus.tlaps.proofState.pending",
+                "description": "Background for a sequent whose proof was not checked yet.",
+                "defaults": {
+                    "dark": "#c8c8c820",
+                    "light": "#c8c8c820",
+                    "highContrast": "#c8c8c850"
+                }
+            },
+            {
+                "id": "tlaplus.tlaps.proofState.progress",
+                "description": "Background for a sequent which is currently being checked.",
+                "defaults": {
+                    "dark": "#d8d8d820",
+                    "light": "#d8d8d820",
+                    "highContrast": "#d8d8d850"
+                }
+            }
+        ]
     },
     "scripts": {
         "vscode:prepublish": "npm run compile -- --production",

src/tlaps.ts

@@ -1,18 +1,47 @@
 import * as vscode from 'vscode';
 import {
+    DocumentUri,
     Executable,
     LanguageClient,
     LanguageClientOptions,
     TransportKind,
     VersionedTextDocumentIdentifier
 } from 'vscode-languageclient/node';
 
+interface ProofStateMarker {
+    range: vscode.Range;
+    state: string;
+    hover: string;
+}
+
 export class TlapsClient {
     private client: LanguageClient | undefined;
     private configEnabled = false;
     private configCommand = [] as string[];
+    private proofStateNames = [
+        'proved',
+        'failed',
+        'omitted',
+        'missing',
+        'pending',
+        'progress',
+    ];
+    private proofStateDecorationTypes = new Map<string, vscode.TextEditorDecorationType>(
+        this.proofStateNames.map(name => {
+            const color = { 'id': 'tlaplus.tlaps.proofState.' + name };
+            const decType = vscode.window.createTextEditorDecorationType({
+                overviewRulerColor: color,
+                overviewRulerLane: vscode.OverviewRulerLane.Right,
+                light: { backgroundColor: color },
+                dark: { backgroundColor: color },
+                isWholeLine: true,
+                rangeBehavior: vscode.DecorationRangeBehavior.ClosedClosed,
+            });
+            return [name, decType];
+        })
+    );
 
-    constructor(context: vscode.ExtensionContext) {
+    constructor(private context: vscode.ExtensionContext) {
         context.subscriptions.push(vscode.commands.registerTextEditorCommand(
             'tlaplus.tlaps.check-step',
             (te, ed, args) => {
@@ -85,6 +114,10 @@ export class TlapsClient {
             clientOptions,
             true,
         );
+        this.context.subscriptions.push(this.client.onNotification(
+            'tlaplus/tlaps/proofStates',
+            this.proofStateNotifHandler.bind(this)
+        ));
         this.client.start();
     }
 
@@ -96,4 +129,24 @@ export class TlapsClient {
         }
         return client.stop();
     }
+
+    private proofStateNotifHandler(uri: DocumentUri, markers: ProofStateMarker[]) {
+        vscode.window.visibleTextEditors.forEach(editor => {
+            if (editor.document.uri.toString() === uri) {
+                const decorations = new Map(this.proofStateNames.map(name => [name, [] as vscode.DecorationOptions[]]));
+                markers.forEach(marker => {
+                    decorations.get(marker.state)?.push(
+                        {
+                            range: marker.range,
+                            hoverMessage: marker.hover,
+                        }
+                    );
+                });
+                this.proofStateDecorationTypes.forEach((decoratorType, proofStateName) => {
+                    const decs = decorations.get(proofStateName);
+                    editor.setDecorations(decoratorType, decs ? decs : []);
+                });
+            }
+        });
+    }
 }