Retain decorators after tabs are switched.

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

src/model/tlaps.ts

@@ -1,5 +1,14 @@
 import { Location, Range } from 'vscode-languageclient/node';
 
+export interface CountByStepStatus {
+    proved: number;
+    failed: number;
+    omitted: number;
+    missing: number;
+    pending: number;
+    progress: number;
+}
+
 export interface TlapsProofObligationResult {
     prover: string;
     meth: string;
@@ -19,4 +28,5 @@ export interface TlapsProofStepDetails {
     status: string;
     location: Location;
     obligations: TlapsProofObligationState[];
+    sub_count: CountByStepStatus;
 }

src/tlaps.ts

@@ -11,12 +11,6 @@
 //  - Visible range: https://stackoverflow.com/questions/40339229/vscode-extension-api-how-to-get-only-visible-lines-of-editor
 //  - Cursor change event: https://stackoverflow.com/questions/44782075/vscode-extension-ondidchangecursorposition
 //
-// TODO: Icons: https://code.visualstudio.com/api/references/icons-in-labels
-//  - testing-passed-icon
-//  - testing-failed-icon
-//  - settings-sync-view-icon   $(sync~spin)
-//  - testing-run-icon
-//
 // TODO: Links to the proof steps: DocumentLinkProvider<T>
 //
 // TODO: Links from the side pane: TextEditor.revealRange(range: Range, revealType?: TextEditorRevealType): void
@@ -27,6 +21,7 @@ import {
     Executable,
     LanguageClient,
     LanguageClientOptions,
+    TextDocumentIdentifier,
     TransportKind,
     VersionedTextDocumentIdentifier
 } from 'vscode-languageclient/node';
@@ -79,6 +74,18 @@ export class TlapsClient {
         // context.subscriptions.push(vscode.window.onDidChangeTextEditorSelection(function(e) {
         //     console.log(e);
         // }, this));
+        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.
+            if (!this.client || !textEditor) {
+                return;
+            }
+            vscode.commands.executeCommand('tlaplus.tlaps.proofStepMarkers.fetch.lsp',
+                {
+                    uri: textEditor.document.uri.toString()
+                } as TextDocumentIdentifier
+            );
+        }));
         context.subscriptions.push(vscode.commands.registerTextEditorCommand(
             'tlaplus.tlaps.check-step',
             (te, ed, args) => {

src/webview/tlapsCurrentProofObligationView.ts

@@ -44,14 +44,17 @@ export class TlapsProofObligationView implements vscode.WebviewViewProvider {
         if (this.tlapsProofStepDetails) {
             const loc = this.tlapsProofStepDetails.location;
             const uri = URI.parse(loc.uri);
+            const details = this.tlapsProofStepDetails;
+            const sub_count = details.sub_count;
             content = `<p>${uri.path.split(/\/|\\/).pop()}</p>`;
             if (loc.range.start.line === loc.range.end.line) {
                 content += `<p>Line: ${loc.range.start.line + 1}</p>`;
             } else {
                 content += `<p>Lines: ${loc.range.start.line + 1}-${loc.range.end.line + 1}</p>`;
             }
-            content += `<p>Status: ${this.tlapsProofStepDetails.kind} / ${this.tlapsProofStepDetails.status}</p>`;
-            this.tlapsProofStepDetails.obligations.forEach(obl => {
+            content += `<p>Status: ${details.kind} / ${details.status}</p>`;
+            content += `<p>Sub: ${sub_count.proved}/${sub_count.failed}/${sub_count.omitted}/${sub_count.missing}/${sub_count.pending}/${sub_count.progress}</p>`;
+            details.obligations.forEach(obl => {
                 content += `<div> Obligation on ${obl.range.start.line + 1}:${obl.range.start.character + 1}--${obl.range.end.line + 1}:${obl.range.end.character + 1}`;
                 if (obl.results) {
                     content += '<ul>';