Show every declared-here position and its gloss in the IDE panel

client/src/types/diagnostics.ts

@@ -73,6 +73,10 @@ export type RefinementError = BaseDiagnostic & {
     customMessage: string;
     counterexample: Counterexample;
     declarationPosition: SourcePosition | null;
+    // where each part of the refinement is declared, the first being declarationPosition
+    declarationPositions: SourcePosition[];
+    // lines that explain the declaration, shown under its locations
+    declarationNotes: string[];
 }
 
 export type Counterexample = {
@@ -99,6 +103,10 @@ export type StateRefinementError = BaseDiagnostic & {
     found: VCSimplificationResult;
     customMessage: string;
     declarationPosition: SourcePosition | null;
+    // where each entry state that makes up expected is declared, the first being declarationPosition
+    declarationPositions: SourcePosition[];
+    // lines that explain the declaration, shown under its locations
+    declarationNotes: string[];
     // one state machine per state set of the receiver's class
     stateMachines: LJStateMachine[];
 }

client/src/webview/script.spec.ts

@@ -63,7 +63,7 @@ function stateError(title: string, sm: LJStateMachine, line = position.lineStart
         title, message: `${title} message`, hints: [], file, position: errorPosition,
         category: 'error', type: 'state-refinement-error', translationTable: {}, expected: 'Open(counter)',
         found: { implication: null as never, origin: null, simplification: 'Closed(counter)' },
-        customMessage: '', declarationPosition: null, stateMachines: [sm],
+        customMessage: '', declarationPosition: null, declarationPositions: [], declarationNotes: [], stateMachines: [sm],
     };
 }
 

client/src/webview/state-errors.spec.ts

@@ -26,6 +26,8 @@ function stateError(line: number, overrides: Partial<StateRefinementError> = {})
         found: { implication: null as never, origin: null, simplification: null },
         customMessage: '',
         declarationPosition: { file: refinementsFile, lineStart: 21, colStart: 29, lineEnd: 21, colEnd: 51 },
+        declarationPositions: [{ file: refinementsFile, lineStart: 21, colStart: 29, lineEnd: 21, colEnd: 51 }],
+        declarationNotes: [],
         stateMachines: [machine()],
         ...overrides,
     };

client/src/webview/styles.ts

@@ -377,6 +377,12 @@ export function getStyles(): string {
         .link:hover {
             text-decoration: underline;
         }
+        .location-note {
+            display: block;
+            padding-left: 2ch;
+            text-indent: -2ch;
+            color: var(--vscode-descriptionForeground);
+        }
         .lj-expression,
         .lj-expression-code {
             font-family: var(--vscode-editor-font-family);

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

@@ -1,6 +1,7 @@
 import { afterEach, describe, expect, it } from 'vitest';
-import type { CustomError, CustomWarning } from '../../../types/diagnostics';
-import { renderDiagnosticsView } from './diagnostics';
+import type { CustomError, CustomWarning, StateRefinementError } from '../../../types/diagnostics';
+import { renderLocation } from '../sections';
+import { formatDiagnosticForClipboard, renderDiagnosticsView } from './diagnostics';
 
 const currentFile = 'file:///workspace/Current.java';
 const otherFile = 'file:///workspace/Other.java';
@@ -86,6 +87,26 @@ describe('diagnostics view', () => {
         expect(document.querySelector('#show-all-button')).toBeNull();
     });
 
+    it('shows every declaration of a refinement with their notes under them', () => {
+        const declaredAt = (lineStart: number) =>
+            ({ file: '/workspace/DoorRefinements.java', lineStart, colStart: 29, lineEnd: lineStart, colEnd: 58 });
+        const stateError = {
+            ...error(), type: 'state-refinement-error', declarationPosition: declaredAt(12),
+            declarationPositions: [declaredAt(12), declaredAt(13)],
+            declarationNotes: ['where closed(this) means doorState(this) == closed', 'where ajar(this) means doorState(this) == ajar'],
+        } as unknown as StateRefinementError;
+        document.body.innerHTML = renderLocation(stateError);
+
+        expect(Array.from(document.querySelectorAll('pre > *')).map(element => element.textContent)).toEqual([
+            'DoorRefinements.java:13', 'DoorRefinements.java:14',
+            'where closed(this) means doorState(this) == closed', 'where ajar(this) means doorState(this) == ajar',
+        ]);
+        expect(document.querySelector('pre > :last-child')?.className).toBe('location-note');
+        // the copied error keeps the notes but not the raw positions
+        expect(formatDiagnosticForClipboard(stateError)).toContain('Declaration Notes: where closed(this) means');
+        expect(formatDiagnosticForClipboard(stateError)).not.toContain('Declaration Positions');
+    });
+
     it.each([false, true])('keeps warnings in the passed state (showAll=%s)', showAll => {
         document.body.innerHTML = renderDiagnosticsView([warning(), warning(otherFile)], showAll, currentFile);
 

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

@@ -96,7 +96,7 @@ export async function copyDiagnosticToClipboard(button: any, displayDiagnostics:
 }
 
 export function formatDiagnosticForClipboard(diagnostic: LJDiagnostic): string {
-    const skippedFields = new Set(['category', 'type', 'translationTable', 'position', 'file', 'declarationPosition', 'stateMachines']);
+    const skippedFields = new Set(['category', 'type', 'translationTable', 'position', 'file', 'declarationPosition', 'declarationPositions', 'stateMachines']);
     const lines: string[] = [];
 
     Object.entries(diagnostic).forEach(([key, value]) => {

client/src/webview/views/sections.ts

@@ -86,15 +86,19 @@ export const renderLocation = (diagnostic: LJDiagnostic): string => {
     const positions: SourcePosition[] = [];
     if (diagnostic.position && diagnostic.file) positions.push(diagnostic.position);
 
-    const declarationPosition = diagnostic.type === 'refinement-error' || diagnostic.type === 'state-refinement-error'
-        ? diagnostic.declarationPosition
+    const declaration = diagnostic.type === 'refinement-error' || diagnostic.type === 'state-refinement-error'
+        ? diagnostic
         : null;
-    if (declarationPosition?.file) positions.push(declarationPosition);
+    const declarationPositions = declaration?.declarationPositions.filter(position => position.file) ?? [];
+    positions.push(...declarationPositions);
 
     if (positions.length === 0) return "";
     const title = positions.length === 1 ? "Location" : "Locations";
     const links = positions.map(renderLocationLink).join("\n");
-    return renderCustomSection(title, /*html*/`<pre>${links}</pre>`);
+    // the notes explain the declarations, so they are shown only under their links
+    const notes = declarationPositions.length > 0 ? declaration?.declarationNotes ?? [] : [];
+    const noteLines = notes.map(note => `<span class="location-note">${escapeHtml(note)}</span>`).join("");
+    return renderCustomSection(title, /*html*/`<pre>${links}${noteLines}</pre>`);
 };
 
 export function renderVariableHighlightButton(variable: LJVariable): string {

server/pom.xml

@@ -167,7 +167,7 @@
 		<dependency>
 			<groupId>io.github.liquid-java</groupId>
 			<artifactId>liquidjava-verifier</artifactId>
-			<version>0.0.37</version>
+			<version>0.0.38</version>
 		</dependency>
 		<dependency>
 		  <groupId>io.github.liquid-java</groupId>

server/src/main/java/dtos/errors/RefinementErrorDTO.java

@@ -1,5 +1,7 @@
 package dtos.errors;
 
+import java.util.List;
+
 import dtos.diagnostics.CounterexampleDTO;
 import dtos.diagnostics.SourcePositionDTO;
 import dtos.diagnostics.VCSimplificationResultDTO;
@@ -16,6 +18,10 @@ public class RefinementErrorDTO extends LJErrorDTO {
     public final String customMessage;
     public final CounterexampleDTO counterexample;
     public final SourcePositionDTO declarationPosition;
+    /** Where each part of the refinement is declared, the first being declarationPosition */
+    public final List<SourcePositionDTO> declarationPositions;
+    /** Lines that explain the declaration, such as what the states it names mean */
+    public final List<String> declarationNotes;
 
     public RefinementErrorDTO(RefinementError error) {
         super("refinement-error", error);
@@ -24,6 +30,8 @@ public RefinementErrorDTO(RefinementError error) {
         this.customMessage = error.getCustomMessage();
         this.counterexample = CounterexampleDTO.from(error.getCounterexample());
         this.declarationPosition = SourcePositionDTO.from(error.getDeclarationPosition());
+        this.declarationPositions = error.getDeclarationPositions().stream().map(SourcePositionDTO::from).toList();
+        this.declarationNotes = error.getDeclarationNotes();
     }
 
     public static RefinementErrorDTO from(RefinementError error) {

server/src/main/java/dtos/errors/StateRefinementErrorDTO.java

@@ -27,6 +27,10 @@ public class StateRefinementErrorDTO extends LJErrorDTO {
     public final VCSimplificationResultDTO found;
     public final String customMessage;
     public final SourcePositionDTO declarationPosition;
+    /** Where each part of the refinement is declared, the first being declarationPosition */
+    public final List<SourcePositionDTO> declarationPositions;
+    /** Lines that explain the declaration, such as what the states it names mean */
+    public final List<String> declarationNotes;
     public final List<StateMachineDTO> stateMachines;
 
     public StateRefinementErrorDTO(StateRefinementError error) {
@@ -35,6 +39,8 @@ public StateRefinementErrorDTO(StateRefinementError error) {
         this.found = VCSimplificationResultDTO.from(error.getFoundSimplification());
         this.customMessage = error.getCustomMessage();
         this.declarationPosition = SourcePositionDTO.from(error.getDeclarationPosition());
+        this.declarationPositions = error.getDeclarationPositions().stream().map(SourcePositionDTO::from).toList();
+        this.declarationNotes = error.getDeclarationNotes();
         this.stateMachines = declarationPosition == null || declarationPosition.file() == null ? List.of()
                 : stateMachines(declarationPosition.file(), specFiles(), error.getContext());
     }

server/src/test/java/utils/DiagnosticConverterTest.java

@@ -159,6 +159,7 @@ void preservesRefinementDetailsAndSimplificationHistory() {
         assertEquals("true", dto.expected);
         assertEquals("expected true", dto.customMessage);
         assertEquals(dto.position, dto.declarationPosition);
+        assertEquals(List.of(dto.position), dto.declarationPositions);
         assertEquals("false", dto.found.implication().predicate());
         assertEquals("constant folding", dto.found.simplification());
         assertEquals("true", dto.found.origin().implication().predicate());
@@ -170,15 +171,18 @@ void preservesRefinementDetailsAndSimplificationHistory() {
     @Test
     void preservesStateRefinementDetailsWithoutDeclarationFile() {
         StateRefinementErrorDTO dto = (StateRefinementErrorDTO) DiagnosticConverter.convertToDTO(
-                new StateRefinementError(position, null, new Predicate(new LiteralBoolean(false)),
+                new StateRefinementError(position, List.of(), new Predicate(new LiteralBoolean(false)),
                         new VCSimplificationResult(new VCImplication(new Predicate())), null, "expected closed",
-                        List.of(), null, null, UnaryOperator.identity()));
+                        List.of(), null, null, UnaryOperator.identity(),
+                        List.of("where closed(this) means doorState(this) == closed")));
         assertEquals("error", dto.category);
         assertEquals("state-refinement-error", dto.type);
         assertEquals("false", dto.expected);
         assertEquals("true", dto.found.implication().predicate());
         assertEquals("expected closed", dto.customMessage);
         assertNull(dto.declarationPosition);
+        assertEquals(List.of(), dto.declarationPositions);
+        assertEquals(List.of("where closed(this) means doorState(this) == closed"), dto.declarationNotes);
         assertEquals(List.of(), dto.stateMachines);
     }