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

The server sends the verifier's declaration positions and declaration notes
(the "where ... means ..." lines) of refinement and state errors, and the
Locations section shows a link to every position, with the notes under them.

Needs liquidjava-verifier 0.0.38: getDeclarationNotes() comes from
liquid-java/liquidjava#517 and getDeclarationPositions() from
liquid-java/liquidjava#525.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

Author: CatarinaGamboa

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,5 +1,6 @@
 import { afterEach, describe, expect, it } from 'vitest';
-import type { CustomError, CustomWarning } from '../../../types/diagnostics';
+import type { CustomError, CustomWarning, StateRefinementError } from '../../../types/diagnostics';
+import { renderLocation } from '../sections';
 import { renderDiagnosticsView } from './diagnostics';
 
 const currentFile = 'file:///workspace/Current.java';
@@ -86,6 +87,22 @@ 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 });
+        document.body.innerHTML = renderLocation({
+            ...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);
+
+        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');
+    });
+
     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/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);
     }