Improve Webview Verification State

client/src/extension.ts

@@ -52,6 +52,7 @@ export async function startExtension(context: vscode.ExtensionContext) {
         return;
     }
     extension.logger!.client.info("Starting LiquidJava...");
+    updateStatusBar("loading");
 
     // find java executable path
     const javaExecutablePath = findJavaExecutable();

client/src/services/status-bar.ts

@@ -1,7 +1,7 @@
 import * as vscode from "vscode";
-import { extension } from "../state";
+import { ExtensionStatus, extension } from "../state";
 
-export type StatusBarState = "loading" | "stopped" | "passed" | "failed";
+export type StatusBarState = ExtensionStatus;
 
  const icons = {
     loading: "$(sync~spin)",
@@ -24,19 +24,24 @@ const statusText = {
 export function registerStatusBar(context: vscode.ExtensionContext) {
     extension.statusBar = vscode.window.createStatusBarItem(vscode.StatusBarAlignment.Left);
     extension.statusBar.command = "liquidjava.showCommands";
-    updateStatusBar("loading");
+    updateStatusBar("loading", true);
     extension.statusBar.show();
     context.subscriptions.push(extension.statusBar);
 }
 
 /**
  * Updates the status bar with the current state
- * @param state The current state ("loading", "stopped", "passed", "failed")
+ * @param status The current status ("loading", "stopped", "passed", "failed")
+ * @param notifyWebview Whether the webview should reflect this status update.
  */
-export function updateStatusBar(state: StatusBarState) {
-    const color = state === "stopped" ? "errorForeground" : "statusBar.foreground";
+export function updateStatusBar(status: StatusBarState, notifyWebview = status !== "loading") {
+    if (notifyWebview) {
+        extension.status = status;
+        extension.webview?.sendMessage({ type: "status", status });
+    }
+    const color = status === "stopped" ? "errorForeground" : "statusBar.foreground";
     if (!extension.statusBar) return;
     extension.statusBar.color = new vscode.ThemeColor(color);
-    extension.statusBar.text = icons[state] + " LiquidJava";
-    extension.statusBar.tooltip = statusText[state];
+    extension.statusBar.text = icons[status] + " LiquidJava";
+    extension.statusBar.tooltip = statusText[status];
 }

client/src/services/webview.ts

@@ -25,6 +25,7 @@ export function registerWebview(context: vscode.ExtensionContext) {
     context.subscriptions.push(
         extension.webview.onDidReceiveMessage(message => {
             if (message.type === "ready") {
+                if (extension.status) extension.webview?.sendMessage({ type: "status", status: extension.status });
                 if (extension.file) extension.webview?.sendMessage({ type: "file", file: extension.file });
                 if (extension.diagnostics) extension.webview?.sendMessage({ type: "diagnostics", diagnostics: extension.diagnostics });
                 if (extension.context) extension.webview?.sendMessage({ type: "context", context: extension.context , errorAtCursor: extension.errorAtCursor });

client/src/state.ts

@@ -8,6 +8,8 @@ import type { LJDiagnostic, RefinementMismatchError } from "./types/diagnostics"
 import type { LJStateMachine } from "./types/fsm";
 import { LJContext, Range } from "./types/context";
 
+export type ExtensionStatus = "loading" | "stopped" | "passed" | "failed";
+
 export class ExtensionState {
     // server/client state
     serverProcess?: child_process.ChildProcess;
@@ -18,6 +20,7 @@ export class ExtensionState {
     logger?: LiquidJavaLogger;
     statusBar?: vscode.StatusBarItem;
     webview?: LiquidJavaWebviewProvider;
+    status?: ExtensionStatus;
 
     // application state
     file?: string;
@@ -28,4 +31,4 @@ export class ExtensionState {
     errorAtCursor?: RefinementMismatchError;
 }
 
-export const extension = new ExtensionState();
+export const extension = new ExtensionState();

client/src/webview/script.ts

@@ -1,10 +1,12 @@
 import { handleDerivableNodeClick, handleDerivationResetClick } from "./views/diagnostics/derivation-nodes";
 import { renderLoading } from "./views/loading";
+import { renderStopped } from "./views/stopped";
 import { renderStateMachineView } from "./views/fsm/fsm";
 import { createMermaidDiagram, renderMermaidDiagram, resetZoom, zoomIn, zoomOut, copyDiagramToClipboard } from "./diagram";
 import type { LJDiagnostic, RefinementMismatchError } from "../types/diagnostics";
 import type { Range } from "../types/context";
 import type { LJStateMachine } from "../types/fsm";
+import type { ExtensionStatus } from "../state";
 import type { NavTab } from "./views/sections";
 import { copyDiagnosticToClipboard, getDisplayDiagnostics, renderDiagnosticsView } from "./views/diagnostics/diagnostics";
 import type { LJContext } from "../types/context";
@@ -25,14 +27,15 @@ type VSCodeApi = {
 export function getScript(vscode: VSCodeApi, document: Document, window: Window) {
     const root = document.getElementById('root')!;
     if (!root) return;
-    let diagnostics: LJDiagnostic[] = [];
+    let diagnostics: LJDiagnostic[] | undefined;
     let showAllDiagnostics = false;
     let currentFile: string;
     const expandedErrors = new Set<number>();
     let stateMachine: LJStateMachine;
     let context: LJContext;
     let errorAtCursor: RefinementMismatchError;
     let selectedTab: NavTab = 'diagnostics';
+    let status: ExtensionStatus = 'loading';
     let diagramOrientation: "LR" | "TB" = "TB";
     let currentDiagram: string = '';
     let revealTimeout: ReturnType<typeof setTimeout> | undefined;
@@ -241,7 +244,7 @@ export function getScript(vscode: VSCodeApi, document: Document, window: Window)
         if (diagnosticCopyBtn) {
             e.preventDefault();
             e.stopPropagation();
-            copyDiagnosticToClipboard(diagnosticCopyBtn, getDisplayDiagnostics(diagnostics, showAllDiagnostics, currentFile));
+            copyDiagnosticToClipboard(diagnosticCopyBtn, getDisplayDiagnostics(diagnostics || [], showAllDiagnostics, currentFile));
             return;
         }
     });
@@ -250,13 +253,17 @@ export function getScript(vscode: VSCodeApi, document: Document, window: Window)
     window.addEventListener('message', event => {
         const msg = event.data;
         switch (msg.type) {
+            case 'status':
+                status = msg.status as ExtensionStatus;
+                updateView();
+                break;
             case 'diagnostics':
                 diagnostics = msg.diagnostics as LJDiagnostic[];
                 if (selectedTab === 'diagnostics') updateView();
                 break;
             case 'file':
                 currentFile = msg.file;
-                if (!showAllDiagnostics && selectedTab === 'diagnostics') updateView();
+                if (diagnostics && !showAllDiagnostics && selectedTab === 'diagnostics') updateView();
                 break;
             case 'fsm':
                 stateMachine = msg.sm as LJStateMachine;
@@ -277,9 +284,22 @@ export function getScript(vscode: VSCodeApi, document: Document, window: Window)
      * Updates the webview content based on the current state
      */
     function updateView() {
+        if (status === 'stopped') {
+            currentDiagram = '';
+            root.innerHTML = renderStopped();
+            return;
+        }
+        if (status === 'loading') {
+            currentDiagram = '';
+            root.innerHTML = renderLoading();
+            return;
+        }
+
         switch (selectedTab) {
             case 'diagnostics':
-                root.innerHTML = renderDiagnosticsView(diagnostics, showAllDiagnostics, currentFile, expandedErrors);
+                root.innerHTML = diagnostics
+                    ? renderDiagnosticsView(diagnostics, showAllDiagnostics, currentFile, expandedErrors)
+                    : renderLoading();
                 break;
             case 'fsm': {
                 const diagram = createMermaidDiagram(stateMachine, diagramOrientation);

client/src/webview/styles.ts

@@ -423,6 +423,37 @@ export function getStyles(): string {
         .info {
             margin: 1rem 0;
         }
+        .stopped-view {
+            display: flex;
+            min-height: calc(100vh - 2rem);
+            flex-direction: column;
+            align-items: center;
+            justify-content: flex-start;
+            gap: 0.75rem;
+            padding-top: 2rem;
+            text-align: center;
+            color: var(--vscode-foreground);
+        }
+        .stopped-view h2 {
+            margin: 0;
+        }
+        .stopped-view .info {
+            max-width: 28rem;
+            color: var(--vscode-descriptionForeground);
+        }
+        .stopped-status-icon {
+            display: inline-flex;
+            align-items: center;
+            justify-content: center;
+            width: 2.25rem;
+            height: 2.25rem;
+            border: 1px solid var(--vscode-errorForeground);
+            border-radius: 50%;
+            color: var(--vscode-errorForeground);
+            font-weight: 700;
+            font-size: 1.35rem;
+            line-height: 1;
+        }
         .more-indicator {
             text-align: center;
             font-size: 0.8rem;

client/src/webview/views/loading.ts

@@ -1,9 +1,11 @@
 
+import { renderMainHeader } from "./sections";
+
 export function renderLoading(): string {
     return /*html*/`
         <div>
-            <h2>LiquidJava</h2>
-            <p>Loading extension...</p>
+            ${renderMainHeader("Verification Pending", "diagnostics")}
+            <p class="info">Running the LiquidJava verification...</p>
         </div>
     `;
 }

client/src/webview/views/stopped.ts

@@ -0,0 +1,9 @@
+export function renderStopped(): string {
+    return /*html*/`
+        <div class="stopped-view">
+            <div class="stopped-status-icon" aria-hidden="true">!</div>
+            <h2>LiquidJava Not Running</h2>
+            <p class="info">To use LiquidJava, run <code>LiquidJava: Start</code> from the command palette</p>
+        </div>
+    `;
+}