Fade dimmed diagram parts less in light themes and count errors on Verification

client/src/webview/script.spec.ts

@@ -329,6 +329,31 @@ describe('webview script', () => {
         expect(root.querySelector('.mermaid')?.textContent).toContain('ljStateDimmed');
     });
 
+    it('counts the errors of the current file on Verification, and its state errors in a quieter badge', () => {
+        showDiagnostics([
+            diagnostic(currentFile, 'Refinement error'),
+            stateError('State refinement error', errorMachine('Counter', 'close'), 4),
+            diagnostic(otherFile, 'Other file error'),
+        ]);
+        const badge = (tab: string) => root.querySelector(`[data-tab="${tab}"] .nav-badge`);
+
+        expect(badge('diagnostics')?.textContent).toBe('2');
+        expect(badge('diagnostics')?.getAttribute('title')).toBe('2 errors');
+        expect(badge('diagnostics')?.classList.contains('nav-badge-error')).toBe(true);
+        expect(badge('fsm')?.textContent).toBe('1');
+        expect(badge('fsm')?.classList.contains('nav-badge-state-error')).toBe(true);
+        expect(badge('context')).toBeNull();
+
+        // the badges stay up to date on the State Machine tab
+        click('[data-tab="fsm"]');
+        receive({ type: 'diagnostics', diagnostics: [stateError('State refinement error', errorMachine('Counter', 'close'), 4)] });
+        expect(badge('diagnostics')?.textContent).toBe('1');
+
+        receive({ type: 'diagnostics', diagnostics: [] });
+        expect(badge('diagnostics')).toBeNull();
+        expect(badge('fsm')).toBeNull();
+    });
+
     it('counts only the state errors of the current file, as listed in the Verification tab', () => {
         showDiagnostics([
             stateError('State refinement error', errorMachine('Counter', 'close'), 4),

client/src/webview/script.ts

@@ -9,7 +9,7 @@ import type { Range } from "../types/context";
 import type { LJStateMachine } from "../types/fsm";
 import type { ExtensionStatus } from "../state";
 import { setHintOpen, type NavTab } from "./views/sections";
-import { copyDiagnosticToClipboard, getDisplayDiagnostics, renderDiagnosticsView } from "./views/diagnostics/diagnostics";
+import { copyDiagnosticToClipboard, getCurrentFileErrorCount, getDisplayDiagnostics, renderDiagnosticsView } from "./views/diagnostics/diagnostics";
 import type { LJContext } from "../types/context";
 import { ContextSectionState, renderContextView } from "./views/context/context";
 import type { DiagnosticRevealTarget } from "../types/diagnostics";
@@ -421,11 +421,12 @@ export function getScript(vscode: VSCodeApi, document: Document, window: Window)
         }
 
         const stateErrors = getCurrentStateErrors();
+        const badges = { errors: getCurrentFileErrorCount(diagnostics, currentFile), stateErrors: stateErrors.length };
         renderedStateMachineView = undefined;
         switch (selectedTab) {
             case 'diagnostics':
                 root.innerHTML = diagnostics
-                    ? renderDiagnosticsView(diagnostics, showAllDiagnostics, currentFile, stateErrors.length)
+                    ? renderDiagnosticsView(diagnostics, showAllDiagnostics, currentFile, badges)
                     : renderLoading();
                 break;
             case 'fsm': {
@@ -439,13 +440,13 @@ export function getScript(vscode: VSCodeApi, document: Document, window: Window)
                     .map(sm => createMermaidDiagram({ ...sm, errorContext: null }, diagramOrientation, showDiagramConditions))
                     .join('\n\n');
                 renderStateMachineView(root, displayedStateMachines, diagrams, diagramOrientation, showDiagramConditions, focusOnError,
-                    { index: shownIndex, count: stateErrors.length, line: getStateErrorLine(shownError) });
+                    { index: shownIndex, count: stateErrors.length, line: getStateErrorLine(shownError) }, badges);
                 renderedStateMachineView = getStateMachineViewKey();
                 if (displayedStateMachines.length > 0) renderMermaidDiagram(document, window);
                 break;
             }
             case 'context':
-                root.innerHTML = renderContextView(context, currentFile, contextSectionState, errorAtCursor, stateErrors.length);
+                root.innerHTML = renderContextView(context, currentFile, contextSectionState, errorAtCursor, badges);
                 break;
         }
     }
@@ -511,7 +512,8 @@ export function getScript(vscode: VSCodeApi, document: Document, window: Window)
     function getStateMachineViewKey(): string {
         const stateErrors = getCurrentStateErrors();
         const { error: shownError } = getShownStateError(stateErrors);
-        return JSON.stringify([shownError?.stateMachines ?? stateMachines, shownError ? getStateErrorKey(shownError) : null, stateErrors.length]);
+        return JSON.stringify([shownError?.stateMachines ?? stateMachines, shownError ? getStateErrorKey(shownError) : null, stateErrors.length,
+            getCurrentFileErrorCount(diagnostics, currentFile)]);
     }
 
     function revealDiagnostic(target: DiagnosticRevealTarget) {

client/src/webview/styles.spec.ts

@@ -74,17 +74,27 @@ describe('state error styles', () => {
         render(state('ljStateDimmed') + '<path class="transition lj-dimmed"></path><g class="label lj-dimmed"></g>');
 
         for (const selector of ['.ljStateDimmed', 'path.lj-dimmed', 'g.lj-dimmed']) {
-            expect(style(selector).opacity).toBe('0.25');
+            expect(style(selector).opacity).toBe('var(--lj-dimmed-opacity)');
         }
     });
 
+    it('fades dimmed parts less in light themes, where they would be hard to read', () => {
+        render('');
+        const dimmedOpacity = (selector: string) => Array.from(document.styleSheets[0].cssRules)
+            .map(rule => rule as CSSStyleRule)
+            .find(rule => rule.selectorText === selector)?.style.getPropertyValue('--lj-dimmed-opacity');
+
+        expect(dimmedOpacity('body')).toBe('0.25');
+        expect(dimmedOpacity('body.vscode-light')).toBe('0.5');
+    });
+
     it('dims single methods of a label without dimming a dimmed transition twice', () => {
         const label = (className: string, method: string) => `<g class="edgeLabel"><g class="${className}"><foreignObject>`
             + `<div><span class="edgeLabel"><p><span class="lj-dimmed-method">${method}</span></p></span></div></foreignObject></g></g>`;
         render(label('label', 'send') + label('label lj-dimmed', 'bind'));
 
         const [method, inDimmedTransition] = document.querySelectorAll('.lj-dimmed-method');
-        expect(getComputedStyle(method).opacity).toBe('0.25');
+        expect(getComputedStyle(method).opacity).toBe('var(--lj-dimmed-opacity)');
         expect(getComputedStyle(inDimmedTransition).opacity).toBe('1');
 
         // only the background of a fully dimmed label is cleared

client/src/webview/styles.ts

@@ -45,8 +45,11 @@ export function getStyles(): string {
             --lj-state-valid: var(--vscode-testing-iconPassed, var(--vscode-charts-green, #388a34));
             --lj-state-invalid: var(--vscode-errorForeground);
             --lj-state-accepted: var(--vscode-editorWarning-foreground, #cca700);
+            --lj-dimmed-opacity: 0.25;
         }
         body.vscode-light {
+            /* dark text faded on white is barely readable, so light themes fade it less */
+            --lj-dimmed-opacity: 0.5;
             /* the light warning colour is too faint for a thin dashed outline on white */
             --lj-state-accepted: color-mix(in srgb, var(--vscode-editorWarning-foreground, #bf8803) 75%, black);
             --lj-token-keyword: #0000FF;
@@ -150,14 +153,21 @@ export function getStyles(): string {
             margin-left: 0.2rem;
             padding: 0 0.25rem;
             box-sizing: border-box;
-            color: var(--vscode-editor-background);
-            background: var(--vscode-errorForeground);
             border-radius: 0.5rem;
             font-size: 10px;
             font-weight: 600;
             line-height: 1rem;
             text-align: center;
         }
+        .nav-badge-error {
+            color: var(--vscode-editor-background);
+            background: var(--vscode-errorForeground);
+        }
+        /* Verification already counts these errors in red */
+        .nav-badge-state-error {
+            color: var(--vscode-badge-foreground);
+            background: var(--vscode-badge-background);
+        }
         .container {
             margin: 0;
             padding: 0.5rem;
@@ -1128,7 +1138,7 @@ export function getStyles(): string {
         .diagram-container .mermaid svg .ljStateDimmed,
         .diagram-container .mermaid svg .lj-dimmed,
         .diagram-container .mermaid .edgeLabel .lj-dimmed-method {
-            opacity: 0.25;
+            opacity: var(--lj-dimmed-opacity);
         }
         .diagram-container .mermaid svg .lj-dimmed .lj-dimmed-method {
             opacity: 1;

client/src/webview/views/context/context.ts

@@ -1,6 +1,6 @@
 import type { LJContext } from "../../../types/context";
 import type { RefinementMismatchError } from "../../../types/diagnostics";
-import { renderMainHeader } from "../sections";
+import { NO_NAV_BADGES, renderMainHeader } from "../sections";
 import { renderContextAliases } from "./aliases";
 import { renderContextGhosts } from "./ghosts";
 import { renderContextVariables } from "./variables";
@@ -11,14 +11,14 @@ export type ContextSectionState = {
     vars: boolean;
 }
 
-export function renderContextView(context: LJContext | undefined, currentFile: string | undefined, sectionState: ContextSectionState, errorAtCursor?: RefinementMismatchError, stateErrorCount = 0): string {
+export function renderContextView(context: LJContext | undefined, currentFile: string | undefined, sectionState: ContextSectionState, errorAtCursor?: RefinementMismatchError, badges = NO_NAV_BADGES): string {
     const allVars = context?.allVars || [];
     const ghosts = context?.ghosts?.filter(ghost => ghost.file === currentFile) || [];
     const aliases = context?.aliases || [];
     const total = allVars.length + ghosts.length + aliases.length;
     return /*html*/`
         <div>
-            ${renderMainHeader("", 'context', stateErrorCount)}
+            ${renderMainHeader("", 'context', badges)}
             ${total === 0
                 ? 'No context information available at the cursor position'
                 : `${renderContextAliases(aliases, sectionState.aliases)}

client/src/webview/views/diagnostics/diagnostics.ts

@@ -4,14 +4,14 @@ import { copyToClipboard } from "../../clipboard";
 import { renderCodiconButton } from "../../icons";
 import { getFileName } from "../../utils";
 import { renderErrors } from "./errors";
-import { renderMainHeader } from "../sections";
+import { NO_NAV_BADGES, renderMainHeader } from "../sections";
 import { renderWarnings } from "./warnings";
 
 export function renderDiagnosticsView(
     diagnostics: LJDiagnostic[],
     showAll: boolean,
     currentFile: string | undefined,
-    stateErrorCount = 0,
+    badges = NO_NAV_BADGES,
 ): string {
     const fileDiagnostics = diagnostics.filter(diagnostic => diagnostic.file?.toLowerCase() === currentFile?.toLowerCase() || !diagnostic.file);
     const displayDiagnostics = showAll ? diagnostics : fileDiagnostics;
@@ -33,7 +33,7 @@ export function renderDiagnosticsView(
 
     return /*html*/`
         <div>
-            ${renderMainHeader(hasErrors ? "" : "Passed Verification", 'diagnostics', stateErrorCount)}
+            ${renderMainHeader(hasErrors ? "" : "Passed Verification", 'diagnostics', badges)}
             ${scopeSelector}
             ${!hasErrors ? '<p class="info">No errors were found by the LiquidJava verifier.</p>' : ''}
             ${
@@ -64,6 +64,12 @@ function renderScopeButton(scope: 'file' | 'workspace', label: string, count: nu
     `;
 }
 
+// the errors of the current file, as counted by the Current file scope, or of the workspace without a current file
+export function getCurrentFileErrorCount(diagnostics: LJDiagnostic[] | undefined, currentFile: string | undefined): number {
+    const errors = (diagnostics ?? []).filter(d => d.category === 'error');
+    return currentFile ? errors.filter(d => d.file?.toLowerCase() === currentFile.toLowerCase() || !d.file).length : errors.length;
+}
+
 export function getDisplayDiagnostics(diagnostics: LJDiagnostic[], showAll: boolean, currentFile: string | undefined): LJDiagnostic[] {
     if (showAll) return diagnostics;
     return diagnostics.filter(diagnostic => diagnostic.file?.toLowerCase() === currentFile?.toLowerCase() || !diagnostic.file);

client/src/webview/views/fsm/fsm.ts

@@ -2,7 +2,7 @@ import type { LJStateMachine } from "../../../types/fsm";
 import { INVALID_STATE_ICON, VALID_STATE_ICON, getRejectedCallText, getStateErrorFocuses, type StateErrorFocus } from "../../diagram-focus";
 import { renderCodiconButton } from "../../icons";
 import { escapeHtml } from "../../utils";
-import { renderMainHeader } from "../sections";
+import { renderMainHeader, type NavBadges } from "../sections";
 
 /**
  * The position of the shown state error among the state errors of the current file
@@ -22,13 +22,13 @@ const NO_STATE_ERROR_NAVIGATION: StateErrorNavigation = { index: -1, count: 0 };
  * @param sms the state machines, one per state set
  * @param diagrams the Mermaid diagram of each state machine
  */
-export function renderStateMachineView(root: HTMLElement, sms: LJStateMachine[], diagrams: string[], orientation: "LR" | "TB", showConditions: boolean, focusOnError = false, stateErrors = NO_STATE_ERROR_NAVIGATION) {
+export function renderStateMachineView(root: HTMLElement, sms: LJStateMachine[], diagrams: string[], orientation: "LR" | "TB", showConditions: boolean, focusOnError = false, stateErrors = NO_STATE_ERROR_NAVIGATION, badges: NavBadges = { errors: 0, stateErrors: stateErrors.count }) {
     const previousDiagramContainer = root.querySelector('.diagram-container') as HTMLElement | null;
     const diagramHeight = previousDiagramContainer?.offsetHeight;
-    root.innerHTML = renderStateMachineViewHtml(sms, diagrams, orientation, showConditions, focusOnError, stateErrors, diagramHeight);
+    root.innerHTML = renderStateMachineViewHtml(sms, diagrams, orientation, showConditions, focusOnError, stateErrors, badges, diagramHeight);
 }
 
-function renderStateMachineViewHtml(sms: LJStateMachine[], diagrams: string[], orientation: "LR" | "TB", showConditions: boolean, focusOnError: boolean, stateErrors: StateErrorNavigation, diagramHeight?: number): string {
+function renderStateMachineViewHtml(sms: LJStateMachine[], diagrams: string[], orientation: "LR" | "TB", showConditions: boolean, focusOnError: boolean, stateErrors: StateErrorNavigation, badges: NavBadges, diagramHeight?: number): string {
     const className = sms[0]?.className;
     const errorFocuses = getStateErrorFocuses(sms);
     const hasConditionExpansions = sms.some(sm =>
@@ -40,7 +40,7 @@ function renderStateMachineViewHtml(sms: LJStateMachine[], diagrams: string[], o
 
     return /*html*/`
         <div>
-            ${renderMainHeader("", 'fsm', stateErrors.count)}
+            ${renderMainHeader("", 'fsm', badges)}
             ${className !== undefined ? /*html*/`
                 <div class="diagram-section">
                     <div class="diagram-container"${diagramHeight ? ` style="min-height: ${diagramHeight}px"` : ''}>

client/src/webview/views/sections.ts

@@ -5,9 +5,9 @@ import { getDiagnosticRevealTarget, getDiagnosticRevealTargetKey } from "../diag
 import { renderCodicon, renderCodiconButton } from "../icons";
 import { LJVariable } from "../../types/context";
 
-export const renderMainHeader = (title: string, selectedTab: NavTab, stateErrorCount = 0): string => /*html*/`
+export const renderMainHeader = (title: string, selectedTab: NavTab, badges = NO_NAV_BADGES): string => /*html*/`
     <div class="header">
-        ${renderNav(selectedTab, stateErrorCount)}
+        ${renderNav(selectedTab, badges)}
         <h2>${title}</h2>
     </div>
 `;
@@ -176,14 +176,29 @@ function getFile(position: SourcePosition): string {
 
 export type NavTab = 'diagnostics' | 'fsm' | 'context';
 
-export function renderNav(selectedTab: NavTab, stateErrorCount = 0): string {
-    const stateErrorBadge = stateErrorCount > 0
-        ? ` <span class="nav-badge" title="${stateErrorCount} state error${stateErrorCount === 1 ? '' : 's'}">${stateErrorCount}</span>`
-        : '';
+function renderNavBadge(count: number, noun: string, className: string): string {
+    if (count <= 0) return '';
+    return ` <span class="nav-badge ${className}" title="${count} ${noun}${count === 1 ? '' : 's'}">${count}</span>`;
+}
+
+/**
+ * The counts shown on the tabs: the errors of the current file on Verification, and those of them that are state
+ * errors on State Machine, in a quieter colour since Verification already counts them
+ */
+export type NavBadges = {
+    errors: number;
+    stateErrors: number;
+};
+
+export const NO_NAV_BADGES: NavBadges = { errors: 0, stateErrors: 0 };
+
+export function renderNav(selectedTab: NavTab, badges = NO_NAV_BADGES): string {
+    const errorBadge = renderNavBadge(badges.errors, 'error', 'nav-badge-error');
+    const stateErrorBadge = renderNavBadge(badges.stateErrors, 'state error', 'nav-badge-state-error');
     return /*html*/`
         <nav>
             <ul>
-                <li><button class="nav-tab ${selectedTab === 'diagnostics' ? 'selected' : ''}" data-tab="diagnostics">Verification</button></li>
+                <li><button class="nav-tab ${selectedTab === 'diagnostics' ? 'selected' : ''}" data-tab="diagnostics">Verification${errorBadge}</button></li>
                 <li><button class="nav-tab ${selectedTab === 'fsm' ? 'selected' : ''}" data-tab="fsm">State Machine${stateErrorBadge}</button></li>
                 <li><button class="nav-tab ${selectedTab === 'context' ? 'selected' : ''}" data-tab="context">Context</button></li>
             </ul>