Mark code in every message with backticks, and name the lines they refer to

liquidjava-verifier/src/main/java/liquidjava/diagnostics/Code.java

@@ -0,0 +1,50 @@
+package liquidjava.diagnostics;
+
+import java.util.regex.Matcher;
+import java.util.regex.Pattern;
+
+/**
+ * Code inside a message, marked with backticks as in {@code found `x > 0`}. Clients that show plain text get the
+ * backticks; the terminal shows the code in colour instead, or keeps the backticks when colour is off
+ */
+public final class Code {
+
+    // a run of backticks, the code, and a run of the same length
+    private static final Pattern SPAN = Pattern.compile("(`+)(.+?)(?<!`)\\1(?!`)", Pattern.DOTALL);
+
+    private Code() {
+    }
+
+    /**
+     * {@code code} marked as code, fenced by more backticks than any run it holds, and padded with a space on each side
+     * if it holds a backtick or starts or ends with a space, so {@link #render} can tell the padding from the code
+     */
+    public static String of(String code) {
+        String fence = "`";
+        while (code.contains(fence))
+            fence += "`";
+        String pad = code.contains("`") || code.startsWith(" ") || code.endsWith(" ") ? " " : "";
+        return fence + pad + code + pad + fence;
+    }
+
+    /** {@code message} with each code span in colour and without its backticks, or as it is when colour is off */
+    public static String render(String message) {
+        return render(message, Colors.enabled());
+    }
+
+    static String render(String message, boolean colour) {
+        if (message == null || !colour)
+            return message;
+        Matcher span = SPAN.matcher(message);
+        StringBuilder rendered = new StringBuilder();
+        while (span.find()) {
+            String code = span.group(2);
+            // the padding of() adds: code with a space at both ends is always padded
+            if (code.length() >= 2 && code.startsWith(" ") && code.endsWith(" "))
+                code = code.substring(1, code.length() - 1);
+            span.appendReplacement(rendered, Matcher.quoteReplacement(Colors.BLUE + code + Colors.RESET));
+        }
+        span.appendTail(rendered);
+        return rendered.toString();
+    }
+}

liquidjava-verifier/src/main/java/liquidjava/diagnostics/Colors.java

@@ -2,6 +2,16 @@
 
 // ANSI color codes
 public class Colors {
+
+    /**
+     * Whether colour may mark code: not when NO_COLOR is set (https://no-color.org), nor when the output is not a
+     * terminal
+     */
+    public static boolean enabled() {
+        String noColor = System.getenv("NO_COLOR");
+        return (noColor == null || noColor.isEmpty()) && System.console() != null;
+    }
+
     public static final String RESET = "\u001B[0m";
     public static final String GREY = "\u001B[90m";
     public static final String RED = "\u001B[31m";

liquidjava-verifier/src/main/java/liquidjava/diagnostics/LJDiagnostic.java

@@ -23,6 +23,7 @@ public class LJDiagnostic extends RuntimeException {
     private SourcePosition position;
     private final List<Hint> hints = new ArrayList<>();
     private final List<String> messageNotes = new ArrayList<>();
+    private final List<SourceReference> references = new ArrayList<>();
     private String counterexample;
     private ErrorCategory category;
     private static final String PIPE = " | ";
@@ -87,6 +88,19 @@ public void addMessageNote(String note) {
         messageNotes.add(note);
     }
 
+    /** Adds a line printed under the message that names a place in the source, as {@code reference} tells */
+    public void addMessageNote(SourceReference reference) {
+        messageNotes.add(reference.message());
+        references.add(reference);
+    }
+
+    /** The places in the source that the message notes and hints name, each with the line that names it */
+    public List<SourceReference> getReferences() {
+        List<SourceReference> all = new ArrayList<>(references);
+        hints.stream().map(Hint::reference).filter(Objects::nonNull).forEach(all::add);
+        return all;
+    }
+
     /** Lines printed under the excerpt of where the refinement is declared that explain it */
     public List<String> getDeclarationNotes() {
         return List.of();
@@ -128,10 +142,10 @@ public String toString() {
         StringBuilder sb = new StringBuilder();
 
         // title
-        sb.append("\n").append(accentColor).append(title).append(": ").append(Colors.RESET).append(message)
+        sb.append("\n").append(accentColor).append(title).append(": ").append(Colors.RESET).append(Code.render(message))
                 .append("\n");
         for (String note : getMessageNotes())
-            sb.append("  ").append(note).append("\n");
+            sb.append("  ").append(Code.render(note)).append("\n");
 
         // snippet
         String snippet = getSnippet();
@@ -142,14 +156,14 @@ public String toString() {
         // counterexample
         String counterexample = getCounterexampleStr();
         if (counterexample != null && !counterexample.isBlank()) {
-            sb.append(" --> ").append(String.join("\n     ", counterexample.split("\n"))).append("\n");
+            sb.append(" --> ").append(Code.render(String.join("\n     ", counterexample.split("\n")))).append("\n");
         }
 
         // hints
         if (!hints.isEmpty()) {
             sb.append("\nHints:\n");
             for (Hint hint : hints)
-                sb.append("  - ").append(String.join("\n    ", hint.message().split("\n"))).append("\n");
+                sb.append("  - ").append(Code.render(String.join("\n    ", hint.message().split("\n")))).append("\n");
         }
 
         // location
@@ -165,7 +179,7 @@ public String toString() {
             if (declarationSnippet != null) {
                 sb.append(declarationSnippet);
                 for (String note : getDeclarationNotes())
-                    sb.append("  ").append(note).append("\n");
+                    sb.append("  ").append(Code.render(note)).append("\n");
             }
 
             sb.append("\n").append(declPos.getFile().getPath()).append(":").append(declPos.getLine())

liquidjava-verifier/src/main/java/liquidjava/diagnostics/SourceReference.java

@@ -0,0 +1,33 @@
+package liquidjava.diagnostics;
+
+import spoon.reflect.cu.SourcePosition;
+
+/**
+ * A place in the source that a line of a diagnostic names, such as {@code line 134} in an origin note, for clients that
+ * link to it
+ *
+ * @param message
+ *            the whole line, a message note or a hint, as the diagnostic gives it
+ * @param text
+ *            the words of {@code message} that name the place
+ * @param start
+ *            where {@code text} starts in {@code message}, as an index of its characters
+ * @param file
+ *            the path of the file
+ * @param line
+ *            the line, from 1
+ * @param column
+ *            the column, from 1
+ */
+public record SourceReference(String message, String text, int start, String file, int line, int column) {
+
+    /** {@code text} where it first occurs in {@code message}, naming {@code position} */
+    public static SourceReference of(String message, String text, SourcePosition position) {
+        return of(message, text, message.indexOf(text), position);
+    }
+
+    public static SourceReference of(String message, String text, int start, SourcePosition position) {
+        return new SourceReference(message, text, start, position.getFile().getPath(), position.getLine(),
+                position.getColumn());
+    }
+}

liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/ErrorMessage.java

@@ -8,6 +8,7 @@
 import java.util.function.UnaryOperator;
 
 import liquidjava.diagnostics.TranslationTable;
+import liquidjava.diagnostics.Code;
 import liquidjava.processor.context.PlacementInCode;
 import liquidjava.rj_language.ast.Expression;
 import liquidjava.rj_language.ast.formatter.DisplayNames;
@@ -36,9 +37,9 @@ static ErrorMessage of(Expression expected, VCSimplificationResult found, Transl
             PlacementInCode placement = translationTable == null ? null : translationTable.get(name);
             return placement == null ? null : placement.getLine();
         });
-        String expectedText = ExpressionFormatter.format(display.apply(expected), names);
+        String expectedText = Code.of(ExpressionFormatter.format(display.apply(expected), names));
         String text = showsFound.test(shown)
-                ? String.format(frame, ExpressionFormatter.format(display.apply(shown), names), expectedText)
+                ? String.format(frame, Code.of(ExpressionFormatter.format(display.apply(shown), names)), expectedText)
                 : String.format("expected %s but could not prove it", expectedText);
         return new ErrorMessage(text, names);
     }

liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/NotFoundError.java

@@ -3,6 +3,7 @@
 import java.util.Collection;
 import java.util.Locale;
 
+import liquidjava.diagnostics.Code;
 import liquidjava.diagnostics.NameSuggester;
 import liquidjava.diagnostics.TranslationTable;
 import liquidjava.diagnostics.hints.Hint;
@@ -29,11 +30,12 @@ public NotFoundError(SourcePosition position, String name, Kind kind, Collection
 
     public NotFoundError(SourcePosition position, String name, Kind kind, TranslationTable translationTable,
             Collection<String> availableElements) {
-        super("Not Found Error", String.format("%s '%s' could not be found", kind, name), position, translationTable);
+        super("Not Found Error", String.format("%s %s could not be found", kind, Code.of(name)), position,
+                translationTable);
         this.name = Utils.getSimpleName(name);
         this.kind = kind;
         NameSuggester.findClosest(name, availableElements)
-                .ifPresent(match -> addHint(Hint.general(String.format("Did you mean '%s'?", match))));
+                .ifPresent(match -> addHint(Hint.general(String.format("Did you mean %s?", Code.of(match)))));
     }
 
     public String getName() {

liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/RefinementError.java

@@ -11,6 +11,7 @@
 import java.util.stream.Collectors;
 
 import liquidjava.diagnostics.AliasExpansion;
+import liquidjava.diagnostics.Code;
 import liquidjava.diagnostics.TranslationTable;
 import liquidjava.diagnostics.categories.ErrorCategory;
 import liquidjava.processor.context.AliasWrapper;
@@ -68,7 +69,7 @@ public RefinementError(SourcePosition position, SourcePosition declarationPositi
             String counterexampleString = this.counterexample.assignments().stream()
                     .map(a -> getDisplayNames().get(a.first()) + " == " + a.second())
                     .collect(Collectors.joining(" && "));
-            setCounterexampleStr("Counterexample: " + counterexampleString);
+            setCounterexampleStr("Counterexample: " + Code.of(counterexampleString));
         }
         setCategory(categoryOf(expected, found));
     }
@@ -120,7 +121,7 @@ public List<AliasExpansion> getExpectedAliases() {
     @Override
     public List<String> getMessageNotes() {
         List<String> notes = new ArrayList<>(
-                aliasDeclarations.stream().map(declaration -> "where " + declaration).toList());
+                aliasDeclarations.stream().map(declaration -> "where " + Code.of(declaration)).toList());
         notes.addAll(super.getMessageNotes());
         return notes;
     }

liquidjava-verifier/src/main/java/liquidjava/diagnostics/hints/Hint.java

@@ -1,14 +1,22 @@
 package liquidjava.diagnostics.hints;
 
+import liquidjava.diagnostics.SourceReference;
+
 /**
  * A suggestion on how to fix a diagnostic
  *
  * @param kind
  *            what the suggestion is about, so clients can show or filter hints separately
  * @param message
- *            the suggestion as shown to the user
+ *            the suggestion as shown to the user, with code marked as {@link liquidjava.diagnostics.Code} marks it
+ * @param reference
+ *            the place in the source the suggestion names, or null
  */
-public record Hint(Kind kind, String message) {
+public record Hint(Kind kind, String message, SourceReference reference) {
+
+    public Hint(Kind kind, String message) {
+        this(kind, message, null);
+    }
 
     public enum Kind {
         /** A suggestion that does not come from a specific analysis */