Set the current proof step via explicit LSP command.

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

src/common.ts

@@ -175,3 +175,24 @@ export async function exists(filePath: string): Promise<boolean> {
         fs.exists(filePath, (ex) => resolve(ex));
     });
 }
+
+// This calls only the latest of the supplied functions per specified period.
+// Used to avoid overloading the environment with too frequent events.
+export class DelayedFn {
+    private latest : (() => void) | null = null;
+    constructor(private period: number) {}
+
+    public do(f : () => void) {
+        const wasScheduled = !!this.latest;
+        this.latest = f;
+        if (!wasScheduled) {
+            setTimeout(() => {
+                const f = this.latest;
+                this.latest = null;
+                if (f) {
+                    f();
+                }
+            }, this.period);
+        }
+    }
+}

src/tlaps.ts

@@ -27,6 +27,7 @@ import {
 } from 'vscode-languageclient/node';
 import { TlapsProofObligationView } from './webview/tlapsCurrentProofObligationView';
 import { TlapsProofStepDetails } from './model/tlaps';
+import { DelayedFn } from './common';
 
 interface ProofStepMarker {
     status: string;
@@ -70,10 +71,22 @@ export class TlapsClient {
         private context: vscode.ExtensionContext,
         private tlapsProofObligationView: TlapsProofObligationView,
     ) {
-        // TODO: Here.
-        // context.subscriptions.push(vscode.window.onDidChangeTextEditorSelection(function(e) {
-        //     console.log(e);
-        // }, this));
+        const delayedCurrentProofStepSet = new DelayedFn(500);
+        context.subscriptions.push(vscode.window.onDidChangeTextEditorSelection(event => {
+            // We track the cursor here to show the current proof step based on the
+            // cursor position.
+            delayedCurrentProofStepSet.do(() => {
+                vscode.commands.executeCommand('tlaplus.tlaps.currentProofStep.set.lsp',
+                    {
+                        uri: event.textEditor.document.uri.toString()
+                    } as TextDocumentIdentifier,
+                    {
+                        start: event.textEditor.selection.start,
+                        end: event.textEditor.selection.end
+                    } as vscode.Range,
+                );
+            });
+        }));
         context.subscriptions.push(vscode.window.onDidChangeActiveTextEditor(textEditor => {
             // A document clears all its decorators when it becomes invisible (e.g. user opens another
             // document in other tab). Here we notify the LSP server to resend the markers.