From a554fc6ef9377e05355eb60e04f2b6d71e030337 Mon Sep 17 00:00:00 2001
From: Catarina Gamboa <catarina.vg@hotmail.com>
Date: Tue, 10 Nov 2026 15:23:44 +0000
Subject: [PATCH] Show the message notes and the counterexample in the hover

The editor diagnostic, and so the hover and the Problems view, now carries
the headline, then the verifier's message notes, then its counterexample,
each on its own line. The hints stay in the LiquidJava view.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
---
 .../src/main/java/LJDiagnosticsHandler.java   | 19 ++++++++++--
 .../test/java/LJDiagnosticsHandlerTest.java   | 29 +++++++++++++++++++
 2 files changed, 46 insertions(+), 2 deletions(-)
 create mode 100644 server/src/test/java/LJDiagnosticsHandlerTest.java

diff --git a/server/src/main/java/LJDiagnosticsHandler.java b/server/src/main/java/LJDiagnosticsHandler.java
index d4617fd..b638a2f 100644
--- a/server/src/main/java/LJDiagnosticsHandler.java
+++ b/server/src/main/java/LJDiagnosticsHandler.java
@@ -72,8 +72,7 @@ public static List<PublishDiagnosticsParams> getDiagnostics(List<LJDiagnostic> d
                 d -> PathUtils.toFileUri(d.getFile()),
                 Collectors.mapping(d -> {
                     Range range = getRangeFromPosition(d.getPosition());
-                    String message = String.format("%s: %s", d.getTitle(), d.getMessage());
-                    return new Diagnostic(range, message, severity, SOURCE);
+                    return new Diagnostic(range, getHoverMessage(d), severity, SOURCE);
                 }, Collectors.toList())
             ));
         
@@ -83,6 +82,22 @@ public static List<PublishDiagnosticsParams> getDiagnostics(List<LJDiagnostic> d
             .toList();
     }
 
+    /**
+     * The message the editor shows for a diagnostic: the headline, then the notes that explain it and the
+     * counterexample, each on its own line. The hints are left to the LiquidJava view
+     * @param diagnostic the diagnostic
+     * @return the message
+     */
+    static String getHoverMessage(LJDiagnostic diagnostic) {
+        List<String> lines = new ArrayList<>();
+        lines.add(String.format("%s: %s", diagnostic.getTitle(), diagnostic.getMessage()));
+        lines.addAll(diagnostic.getMessageNotes());
+        String counterexample = diagnostic.getCounterexampleStr();
+        if (counterexample != null && !counterexample.isBlank())
+            lines.add(counterexample);
+        return String.join("\n", lines);
+    }
+
     /**
      * Generates empty diagnostics for the given URI
      * @param uri the uri used for the verification
diff --git a/server/src/test/java/LJDiagnosticsHandlerTest.java b/server/src/test/java/LJDiagnosticsHandlerTest.java
new file mode 100644
index 0000000..18f0b20
--- /dev/null
+++ b/server/src/test/java/LJDiagnosticsHandlerTest.java
@@ -0,0 +1,29 @@
+import static org.junit.jupiter.api.Assertions.assertEquals;
+
+import java.util.List;
+
+import org.junit.jupiter.api.Test;
+
+import liquidjava.diagnostics.LJDiagnostic;
+import liquidjava.diagnostics.hints.Hint;
+
+class LJDiagnosticsHandlerTest {
+
+    @Test
+    void hoverShowsTheHeadlineThenTheNotesThenTheCounterexampleButNoHints() {
+        LJDiagnostic diagnostic = new LJDiagnostic("Refinement Error", "expected timeout >= 0 but could not prove it",
+                null, "", null) {
+            @Override
+            public List<String> getMessageNotes() {
+                return List.of("where Positive(x) means x > 0");
+            }
+        };
+        diagnostic.setCounterexampleStr("Counterexample: timeout == -1");
+        diagnostic.addHint(Hint.general("Add a refinement"));
+
+        assertEquals("""
+                Refinement Error: expected timeout >= 0 but could not prove it
+                where Positive(x) means x > 0
+                Counterexample: timeout == -1""", LJDiagnosticsHandler.getHoverMessage(diagnostic));
+    }
+}