Make whole-line markers configurable.

Signed-off-by: Karolis Petrauskas <[email protected]>
tlaplus · Oct 16, 2023 · cf04d98 · cf04d98
1 parent 606bf3c
commit cf04d98
Show file tree

Hide file tree

Showing 2 changed files with 37 additions and 23 deletions.
diff --git a/package.json b/package.json
@@ -395,6 +395,11 @@
                     "items": {"type": "string"},
                     "description": "Command and arguments to start a TLAPS LSP server.",
                     "default": ["opam", "exec", "--", "tlapm_lsp", "--log-io", "--log-to=/tmp/tlapm_lsp.log"]
+                },
+                "tlaplus.tlaps.wholeLine": {
+                    "type": "boolean",
+                    "default": true,
+                    "description": "Mark proof step states using whole line."
                 }
             }
         },
@@ -435,18 +440,18 @@
                 "id": "tlaplus.tlaps.proofState.omitted",
                 "description": "Background for a sequent with omitted proof.",
                 "defaults": {
-                    "dark": "#c8ff0020",
-                    "light": "#c8ff0020",
-                    "highContrast": "#c8ff0050"
+                    "dark": "#ff660020",
+                    "light": "#ff660020",
+                    "highContrast": "#ff660050"
                 }
             },
             {
                 "id": "tlaplus.tlaps.proofState.missing",
                 "description": "Background for a sequent with no proof.",
                 "defaults": {
-                    "dark": "#c8ff0020",
-                    "light": "#c8ff0020",
-                    "highContrast": "#c8ff0050"
+                    "dark": "#ff660020",
+                    "light": "#ff660020",
+                    "highContrast": "#ff660050"
                 }
             },
             {

diff --git a/src/tlaps.ts b/src/tlaps.ts
@@ -18,6 +18,7 @@ export class TlapsClient {
     private client: LanguageClient | undefined;
     private configEnabled = false;
     private configCommand = [] as string[];
+    private configWholeLine = true;
     private proofStateNames = [
         'proved',
         'failed',
@@ -26,20 +27,7 @@ export class TlapsClient {
         '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];
-        })
-    );
+    private proofStateDecorationTypes = new Map<string, vscode.TextEditorDecorationType>();
 
     constructor(private context: vscode.ExtensionContext) {
         context.subscriptions.push(vscode.commands.registerTextEditorCommand(
@@ -63,13 +51,31 @@ export class TlapsClient {
         context.subscriptions.push(vscode.workspace.onDidChangeConfiguration(event => {
             if (this.readConfig()) {
                 this.tryStop();
+                this.makeDecoratorTypes();
                 this.tryStart();
             }
         }));
         this.readConfig();
+        this.makeDecoratorTypes();
         this.tryStart();
     }
 
+    private makeDecoratorTypes() {
+        this.proofStateDecorationTypes.clear();
+        this.proofStateNames.forEach(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: this.configWholeLine,
+                rangeBehavior: vscode.DecorationRangeBehavior.ClosedOpen,
+            });
+            this.proofStateDecorationTypes.set(name, decType);
+        });
+    }
+
     public deactivate() {
         this.tryStop();
     }
@@ -78,11 +84,14 @@ export class TlapsClient {
         const config = vscode.workspace.getConfiguration();
         const configEnabled = config.get<boolean>('tlaplus.tlaps.enabled');
         const configCommand = config.get<string[]>('tlaplus.tlaps.lspServerCommand');
-        const configChanged =
-            configEnabled !== this.configEnabled ||
-            JSON.stringify(configCommand) !== JSON.stringify(this.configCommand);
+        const configWholeLine = config.get<boolean>('tlaplus.tlaps.wholeLine');
+        const configChanged = false
+            || configEnabled !== this.configEnabled
+            || JSON.stringify(configCommand) !== JSON.stringify(this.configCommand)
+            || configWholeLine !== this.configWholeLine;
         this.configEnabled = !!configEnabled;
         this.configCommand = configCommand ? configCommand : [];
+        this.configWholeLine = !!configWholeLine;
         return configChanged;
     }