From 606bf3c3e83e1bf90701f3beb0a36f543e80cb45 Mon Sep 17 00:00:00 2001
From: Karolis Petrauskas <k.petrauskas@gmail.com>
Date: Sun, 15 Oct 2023 10:55:26 +0300
Subject: [PATCH] Use decorators to present proof states.

Signed-off-by: Karolis Petrauskas <k.petrauskas@gmail.com>
---
 .vscode/cspell.json |  3 +++
 package.json        | 58 ++++++++++++++++++++++++++++++++++++++++++++-
 src/tlaps.ts        | 55 +++++++++++++++++++++++++++++++++++++++++-
 3 files changed, 114 insertions(+), 2 deletions(-)

diff --git a/.vscode/cspell.json b/.vscode/cspell.json
index 7901754..7665b72 100644
--- a/.vscode/cspell.json
+++ b/.vscode/cspell.json
@@ -1,9 +1,12 @@
 {
     "words": [
         "tlaplus",
+        "pluscal",
         "tlaps",
         "tlapm",
         "sany",
+        "opam",
+        "pdflatex",
         "checkndebug",
         "evaluatable"
     ]
diff --git a/package.json b/package.json
index f07ea41..c997037 100644
--- a/package.json
+++ b/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",
diff --git a/src/tlaps.ts b/src/tlaps.ts
index 49d598c..2b5dde9 100644
--- a/src/tlaps.ts
+++ b/src/tlaps.ts
@@ -1,5 +1,6 @@
 import * as vscode from 'vscode';
 import {
+    DocumentUri,
     Executable,
     LanguageClient,
     LanguageClientOptions,
@@ -7,12 +8,40 @@ import {
     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 : []);
+                });
+            }
+        });
+    }
 }