Show the message notes and the counterexample in the hover

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

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));
+    }
+}