diff --git a/client/src/services/hover.ts b/client/src/services/hover.ts
index cd96ea9..d0ac596 100644
--- a/client/src/services/hover.ts
+++ b/client/src/services/hover.ts
@@ -5,6 +5,8 @@ import { getSelectionContextVariables } from './context';
 import { getOriginalVariableName, normalizeFilePath } from '../utils/utils';
 import { definitionMatchesClass, getDefinitions } from './definition';
 import { isExtensionRunning } from '../extension';
+import type { SourcePosition } from '../types/diagnostics';
+import { formatDiagnosticMarkdown } from '../utils/message-markdown';
 
 /**
  * Initializes hover provider for LiquidJava diagnostics
@@ -29,12 +31,30 @@ export function registerHover() {
                 }
             }
 
-            if (hoverContent.value.length === 0) return null;
-            return new vscode.Hover(hoverContent);
+            const contents = [hoverContent, ...getHoveredDiagnostics(document, position)].filter(content => content.value.length > 0);
+            if (contents.length === 0) return null;
+            return new vscode.Hover(contents);
         }
     });
 }
 
+/**
+ * What the LiquidJava diagnostics at a position say under their headline, in markdown: the notes that explain them,
+ * the counterexample and the hints. VS Code shows the headline in its own hover, which is plain text
+ */
+function getHoveredDiagnostics(document: vscode.TextDocument, position: vscode.Position): vscode.MarkdownString[] {
+    const file = normalizeFilePath(document.uri.fsPath);
+    return (extension.diagnostics ?? [])
+        .filter(diagnostic => diagnostic.position && diagnostic.file && normalizeFilePath(diagnostic.file) === file)
+        .filter(diagnostic => {
+            const { lineStart, colStart, lineEnd, colEnd } = diagnostic.position!;
+            return new vscode.Range(lineStart, colStart, lineEnd, colEnd).contains(position);
+        })
+        .map(diagnostic => formatDiagnosticMarkdown(diagnostic, toLocationLink))
+        .filter((markdown): markdown is string => markdown !== null)
+        .map(markdown => new vscode.MarkdownString(markdown));
+}
+
 function getHoveredVariable(document: vscode.TextDocument, position: vscode.Position): LJVariable | null {
     if (!extension.context) return null;
 
@@ -120,9 +140,12 @@ function formatMethodHover(method: LJMethod): string {
 }
 
 function formatMethodLocationLink(method: LJMethod): string | null {
-    if (!method.position?.file) return null;
-    const uri = vscode.Uri.file(method.position.file).with({
-        fragment: `L${method.position.lineStart + 1},${method.position.colStart + 1}`
-    });
-    return `[Go to Refinements Definition](${uri.toString()})`;
+    const link = method.position && toLocationLink(method.position);
+    return link ? `[Go to Refinements Definition](${link})` : null;
+}
+
+// a link that opens the file at the position
+function toLocationLink(position: SourcePosition): string | null {
+    if (!position.file) return null;
+    return vscode.Uri.file(position.file).with({ fragment: `L${position.lineStart + 1},${position.colStart + 1}` }).toString();
 }
diff --git a/client/src/utils/message-markdown.spec.ts b/client/src/utils/message-markdown.spec.ts
new file mode 100644
index 0000000..d81bdf2
--- /dev/null
+++ b/client/src/utils/message-markdown.spec.ts
@@ -0,0 +1,54 @@
+import { describe, expect, it } from 'vitest';
+import { formatDiagnosticMarkdown, formatHintsMarkdown } from './message-markdown';
+
+describe('hints in markdown', () => {
+    it('keeps the code and links the lines, and escapes the rest', () => {
+        const hint = '`preview.setTilingMode(int mode)` on line 51 decides the state of `preview`: with `mode == 2`, this call would be allowed';
+        const position = { file: '/workspace/Stage.java', lineStart: 50, colStart: 8, lineEnd: 50, colEnd: 8 };
+        const markdown = formatHintsMarkdown([
+            { kind: 'deciding-argument', message: hint },
+            { kind: 'general', message: "Call `` b.f('`') `` or `` `q `` when a*b < c_d | #e" },
+        ], [{ message: hint, text: 'line 51', start: 37, position }], p => `file://${p.file}#L${p.lineStart + 1}`);
+
+        expect(markdown).toBe([
+            '**Hints**',
+            '`preview.setTilingMode(int mode)` on [line 51](file:///workspace/Stage.java#L51) decides the state of `preview`\\: with `mode == 2`\\, this call would be allowed',
+            "Call ``b.f('`')`` or `` `q `` when a\\*b \\< c\\_d \\| \\#e",
+        ].join('\n\n'));
+    });
+
+    it('lists several call sequences as options', () => {
+        const markdown = formatHintsMarkdown([
+            { kind: 'call-sequence', message: 'Call `host.dispose()` before this call' },
+            { kind: 'call-sequence', message: 'Call `host.removeNotify()` before this call' },
+        ], [], () => null);
+
+        expect(markdown).toBe('**Hints**\n\nAny one of these:\n\n- Call `host.dispose()` before this call\n- Call `host.removeNotify()` before this call');
+    });
+});
+
+describe('a diagnostic in markdown', () => {
+    it('shows the headline, then the notes, then the counterexample, then the hints', () => {
+        const note = 'Origin: line 134, `new BufferedInputStream(stream)` makes `markState(buffered) == unmarked`';
+        const position = { file: '/workspace/M.java', lineStart: 133, colStart: 43, lineEnd: 133, colEnd: 43 };
+        const diagnostic = {
+            category: 'error', type: 'refinement-error', title: 'Refinement Error', message: 'found `x` but expected `y`',
+            hints: [{ kind: 'general', message: 'Call `buffered.mark(int)` before this call' }],
+            file: '/workspace/M.java', position, messageNotes: [note],
+            references: [{ message: note, text: 'line 134', start: 8, position }],
+            expected: 'y', found: null, customMessage: '', declarationPosition: null, declarationPositions: [], declarationNotes: [],
+            counterexample: { assignments: [{ variable: 'x', value: '0' }, { variable: 'size(s)', value: '2' }] },
+        } as unknown as import('../types/diagnostics').LJDiagnostic;
+        expect(formatDiagnosticMarkdown(diagnostic, p => `file://${p.file}#L${p.lineStart + 1}`)).toBe([
+            'found `x` but expected `y`',
+            'Origin\\: [line 134](file:///workspace/M.java#L134)\\, `new BufferedInputStream(stream)` makes `markState(buffered) == unmarked`',
+            'Counterexample: `x == 0 && size(s) == 2`',
+            '**Hint**\n\nCall `buffered.mark(int)` before this call',
+        ].join('\n\n'));
+    });
+
+    it('is the headline alone when the diagnostic has no notes, counterexample or hints', () => {
+        const diagnostic = { category: 'error', type: 'custom-error', title: 'Error', message: 'a < b', hints: [], file: '', position: null, messageNotes: [], references: [] } as unknown as import('../types/diagnostics').LJDiagnostic;
+        expect(formatDiagnosticMarkdown(diagnostic, () => null)).toBe('a \\< b');
+    });
+});
diff --git a/client/src/utils/message-markdown.ts b/client/src/utils/message-markdown.ts
new file mode 100644
index 0000000..e148824
--- /dev/null
+++ b/client/src/utils/message-markdown.ts
@@ -0,0 +1,74 @@
+import type { LJDiagnostic, LJHint, LJSourceReference, SourcePosition } from "../types/diagnostics";
+import { groupHints, splitMessageText } from "./message-text";
+
+// the link that opens a place in the source, or null if it has no file
+export type LinkTarget = (position: SourcePosition) => string | null;
+
+/**
+ * Formats what the editor hover shows of a diagnostic, in markdown: its headline, the notes that explain it (such as
+ * where a value comes from), the counterexample and the hints, with their code as inline code and the places they
+ * name as links. VS Code's own part of the hover, which is plain text, shows only the diagnostic's title
+ * @param linkTo the link that opens a place
+ * @returns the markdown, or null if the diagnostic has no headline
+ */
+export function formatDiagnosticMarkdown(diagnostic: LJDiagnostic, linkTo: LinkTarget): string | null {
+    const parts = [
+        formatMessageMarkdown(diagnostic.message, diagnostic.references, linkTo),
+        ...diagnostic.messageNotes.map(note => formatMessageMarkdown(note, diagnostic.references, linkTo)),
+        formatCounterexampleMarkdown(diagnostic),
+        formatHintsMarkdown(diagnostic.hints, diagnostic.references, linkTo),
+    ].filter((part): part is string => part !== null && part.length > 0);
+    return parts.length > 0 ? parts.join("\n\n") : null;
+}
+
+/**
+ * Formats the hints of a diagnostic in markdown, as the panel shows them: their code as inline code and the places
+ * they name as links, with everything else escaped, since hints hold expressions with `*`, `_`, `<` or `|`
+ * @param references the places the hints name
+ * @param linkTo the link that opens a place
+ * @returns the markdown, or null if there are no hints
+ */
+export function formatHintsMarkdown(hints: LJHint[] | undefined, references: LJSourceReference[], linkTo: LinkTarget): string | null {
+    const { shown, options, notes } = groupHints(hints);
+    if (shown.length === 0) return null;
+    const format = (hint: LJHint) => formatMessageMarkdown(hint.message, references, linkTo);
+    return [
+        shown.length === 1 ? "**Hint**" : "**Hints**",
+        ...options.length > 0 ? ["Any one of these:", options.map(hint => `- ${format(hint)}`).join("\n")] : [],
+        ...notes.map(format),
+    ].join("\n\n");
+}
+
+// Counterexample: `x == 1 && y == 0`, as the verifier prints it, or null if the diagnostic has none
+function formatCounterexampleMarkdown(diagnostic: LJDiagnostic): string | null {
+    if (diagnostic.type !== "refinement-error" || diagnostic.counterexample.assignments.length === 0) return null;
+    const assignments = diagnostic.counterexample.assignments.map(a => `${a.variable} == ${a.value}`).join(" && ");
+    return `Counterexample: ${formatInlineCode(assignments)}`;
+}
+
+function formatMessageMarkdown(message: string, references: LJSourceReference[], linkTo: LinkTarget): string {
+    return splitMessageText(message, references).map(segment => {
+        switch (segment.kind) {
+            case "reference": {
+                const target = linkTo(segment.reference.position);
+                const text = escapeMarkdown(segment.reference.text);
+                return target ? `[${text}](${target})` : text;
+            }
+            case "code": return formatInlineCode(segment.code);
+            case "text": return escapeMarkdown(segment.text);
+        }
+    }).join("");
+}
+
+// a fence longer than any run of backticks in the code, and a space on each side, which markdown strips, if the code
+// starts or ends with a backtick or a space
+function formatInlineCode(code: string): string {
+    const fence = "`".repeat(Math.max(0, ...(code.match(/`+/g) ?? []).map(run => run.length)) + 1);
+    const pad = /^[`\s]|[`\s]$/.test(code) ? " " : "";
+    return `${fence}${pad}${code}${pad}${fence}`;
+}
+
+// every ASCII punctuation character can be escaped in markdown, so all are, rather than those that start a construct
+function escapeMarkdown(text: string): string {
+    return text.replace(/[!-/:-@[-`{-~]/g, "\\$&");
+}
diff --git a/client/src/utils/message-text.ts b/client/src/utils/message-text.ts
new file mode 100644
index 0000000..451c975
--- /dev/null
+++ b/client/src/utils/message-text.ts
@@ -0,0 +1,65 @@
+import type { LJHint, LJSourceReference } from "../types/diagnostics";
+
+// a part of a line of a diagnostic: plain text, code the verifier marks with backticks, or a place in the source it names
+export type MessageSegment =
+    | { kind: "text"; text: string }
+    | { kind: "code"; code: string }
+    | { kind: "reference"; reference: LJSourceReference };
+
+// a run of backticks, the code, and a run of the same length, as the verifier marks code in its messages
+const CODE_SPAN = /(`+)([\s\S]+?)(?<!`)\1(?!`)/y;
+
+/**
+ * Splits a line of a diagnostic, such as a note or a hint, into its text, the code it marks with backticks,
+ * without the backticks, and the places in the source it names
+ * @param references the places the diagnostic names, of which only those of this line are used
+ */
+export function splitMessageText(message: string, references: LJSourceReference[] = []): MessageSegment[] {
+    const links = references.filter(reference =>
+        reference.message === message && message.startsWith(reference.text, reference.start));
+    const segments: MessageSegment[] = [];
+    let text = "";
+    const flushText = () => {
+        if (text) segments.push({ kind: "text", text });
+        text = "";
+    };
+    let index = 0;
+    while (index < message.length) {
+        const link = links.find(reference => reference.start === index);
+        if (link) {
+            flushText();
+            segments.push({ kind: "reference", reference: link });
+            index += link.text.length;
+            continue;
+        }
+        CODE_SPAN.lastIndex = index;
+        const span = message[index] === "`" ? CODE_SPAN.exec(message) : null;
+        if (span) {
+            flushText();
+            segments.push({ kind: "code", code: unpad(span[2]) });
+            index += span[0].length;
+            continue;
+        }
+        text += message[index];
+        index++;
+    }
+    flushText();
+    return segments;
+}
+
+// the code without the space on each side that the verifier adds to code that holds a backtick or a space at an end
+function unpad(code: string): string {
+    return code.length >= 2 && code.startsWith(" ") && code.endsWith(" ") ? code.slice(1, -1) : code;
+}
+
+/**
+ * The hints of a diagnostic as they are shown: several call sequences are alternatives, so they are listed as options
+ * apart from the hints that explain the error
+ */
+export function groupHints(hints: LJHint[] | undefined): { shown: LJHint[]; options: LJHint[]; notes: LJHint[] } {
+    const shown = (hints ?? []).filter(hint => hint.message.trim());
+    const sequences = shown.filter(hint => hint.kind === "call-sequence");
+    const options = sequences.length > 1 ? sequences : [];
+    const notes = options.length > 0 ? shown.filter(hint => hint.kind !== "call-sequence") : shown;
+    return { shown, options, notes };
+}
diff --git a/client/src/webview/message-text.ts b/client/src/webview/message-text.ts
index 595915f..bc69283 100644
--- a/client/src/webview/message-text.ts
+++ b/client/src/webview/message-text.ts
@@ -1,43 +1,21 @@
 import type { LJSourceReference } from "../types/diagnostics";
+import { splitMessageText } from "../utils/message-text";
 import { renderLineTags } from "./highlighting";
 import { escapeHtml } from "./utils";
 
-// a run of backticks, the code, and a run of the same length, as the verifier marks code in its messages
-const CODE_SPAN = /(`+)([\s\S]+?)(?<!`)\1(?!`)/y;
-
 /**
  * Renders a line of a diagnostic, such as a note or a hint: the code it marks with backticks in the editor font,
  * without the backticks, and each place in the source it names as a link that opens that place
  * @param references the places the diagnostic names, of which only those of this line are used
  */
 export function renderMessageText(message: string, references: LJSourceReference[] = []): string {
-    const links = references.filter(reference =>
-        reference.message === message && message.startsWith(reference.text, reference.start));
-    let html = "";
-    let index = 0;
-    while (index < message.length) {
-        const link = links.find(reference => reference.start === index);
-        if (link) {
-            html += renderReferenceLink(link);
-            index += link.text.length;
-            continue;
-        }
-        CODE_SPAN.lastIndex = index;
-        const span = message[index] === "`" ? CODE_SPAN.exec(message) : null;
-        if (span) {
-            html += `<code class="lj-code">${renderLineTags(unpad(span[2]))}</code>`;
-            index += span[0].length;
-            continue;
+    return splitMessageText(message, references).map(segment => {
+        switch (segment.kind) {
+            case "reference": return renderReferenceLink(segment.reference);
+            case "code": return `<code class="lj-code">${renderLineTags(segment.code)}</code>`;
+            case "text": return escapeHtml(segment.text);
         }
-        html += escapeHtml(message[index]);
-        index++;
-    }
-    return html;
-}
-
-// the code without the space on each side that the verifier adds to code that holds a backtick or a space at an end
-function unpad(code: string): string {
-    return code.length >= 2 && code.startsWith(" ") && code.endsWith(" ") ? code.slice(1, -1) : code;
+    }).join("");
 }
 
 function renderReferenceLink(reference: LJSourceReference): string {
diff --git a/client/src/webview/styles.ts b/client/src/webview/styles.ts
index c85bdc1..5c1e47d 100644
--- a/client/src/webview/styles.ts
+++ b/client/src/webview/styles.ts
@@ -233,14 +233,13 @@ export function getStyles(): string {
             background-color: var(--vscode-editor-background);
             border-radius: 4px;
         }
-        /* code that a message marks with backticks, set apart from its prose */
+        /* code that a message marks with backticks, as VS Code renders inline code in a markdown hover */
         .lj-code {
-            padding: 0 0.2em;
+            padding: 0 0.1em;
             border-radius: 3px;
             font-family: var(--vscode-editor-font-family, monospace);
             font-size: var(--vscode-editor-font-size, inherit);
-            color: var(--vscode-textPreformat-foreground);
-            background-color: var(--vscode-textPreformat-background);
+            background-color: var(--vscode-textCodeBlock-background);
             overflow-wrap: break-word;
         }
         .message-note {
diff --git a/client/src/webview/views/sections.ts b/client/src/webview/views/sections.ts
index a571d57..da35aa4 100644
--- a/client/src/webview/views/sections.ts
+++ b/client/src/webview/views/sections.ts
@@ -4,6 +4,7 @@ import { renderHighlightedExpression, renderHighlightedInlineExpression } from "
 import { getDiagnosticRevealTarget, getDiagnosticRevealTargetKey } from "../diagnostic-reveal";
 import { renderCodicon, renderCodiconButton } from "../icons";
 import { renderMessageText } from "../message-text";
+import { groupHints } from "../../utils/message-text";
 import { LJVariable } from "../../types/context";
 
 export const renderMainHeader = (title: string, selectedTab: NavTab, badges = NO_NAV_BADGES): string => /*html*/`
@@ -32,23 +33,19 @@ export function setHintOpen(key: string, open: boolean) {
 
 /**
  * Renders the hints of a diagnostic, closed until the user opens them
- * Several call sequences are alternatives, so they are listed as options apart from the hints that explain the error
  * @param hints The hints of the diagnostic
  * @param key Identifies the diagnostic, so opened hints stay open after a new verification
  * @param references The places in the source the hints name
  */
 export function renderHints(hints: LJHint[] | undefined, key?: string, references: LJSourceReference[] = []): string {
-    const shown = (hints ?? []).filter(hint => hint.message.trim());
+    const { shown, options, notes } = groupHints(hints);
     if (shown.length === 0) return '';
-    const options = shown.filter(hint => hint.kind === 'call-sequence');
-    const listsOptions = options.length > 1;
-    const notes = listsOptions ? shown.filter(hint => hint.kind !== 'call-sequence') : shown;
     const open = key !== undefined && openHints.has(key);
     return /*html*/`
         <details class="section hint-section"${key !== undefined ? ` data-hint-key="${escapeHtml(key)}"` : ''}${open ? ' open' : ''}>
             <summary class="hint-summary">${shown.length === 1 ? 'Hint' : 'Hints'}</summary>
             <div class="hint-body">
-                ${listsOptions ? /*html*/`
+                ${options.length > 0 ? /*html*/`
                     <div class="hint-options">
                         <p class="hint-options-title">Any one of these:</p>
                         <ul>${options.map(hint => `<li>${renderHintMessage(hint, references)}</li>`).join('')}</ul>
diff --git a/server/src/main/java/LJDiagnosticsHandler.java b/server/src/main/java/LJDiagnosticsHandler.java
index b638a2f..4f3fac7 100644
--- a/server/src/main/java/LJDiagnosticsHandler.java
+++ b/server/src/main/java/LJDiagnosticsHandler.java
@@ -72,7 +72,7 @@ public static List<PublishDiagnosticsParams> getDiagnostics(List<LJDiagnostic> d
                 d -> PathUtils.toFileUri(d.getFile()),
                 Collectors.mapping(d -> {
                     Range range = getRangeFromPosition(d.getPosition());
-                    return new Diagnostic(range, getHoverMessage(d), severity, SOURCE);
+                    return new Diagnostic(range, diagnosticMessage(d), severity, SOURCE);
                 }, Collectors.toList())
             ));
         
@@ -83,19 +83,14 @@ public static List<PublishDiagnosticsParams> getDiagnostics(List<LJDiagnostic> d
     }
 
     /**
-     * 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
+     * The message of a diagnostic in the editor: its title alone. VS Code shows that message as plain text in the
+     * hover, the Problems tab and the problem view; the headline, the notes, the counterexample and the hints are
+     * rendered by the extension's own part of the hover, in markdown, and by 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);
+    static String diagnosticMessage(LJDiagnostic diagnostic) {
+        return diagnostic.getTitle();
     }
 
     /**
diff --git a/server/src/test/java/LJDiagnosticsHandlerTest.java b/server/src/test/java/LJDiagnosticsHandlerTest.java
index 18f0b20..c585785 100644
--- a/server/src/test/java/LJDiagnosticsHandlerTest.java
+++ b/server/src/test/java/LJDiagnosticsHandlerTest.java
@@ -10,9 +10,9 @@
 class LJDiagnosticsHandlerTest {
 
     @Test
-    void hoverShowsTheHeadlineThenTheNotesThenTheCounterexampleButNoHints() {
-        LJDiagnostic diagnostic = new LJDiagnostic("Refinement Error", "expected timeout >= 0 but could not prove it",
-                null, "", null) {
+    void messageIsTheTitleAlone() {
+        LJDiagnostic diagnostic = new LJDiagnostic("Refinement Error", "found `x > 0` but expected `y == 1`", null, "",
+                null) {
             @Override
             public List<String> getMessageNotes() {
                 return List.of("where Positive(x) means x > 0");
@@ -20,10 +20,6 @@ public List<String> getMessageNotes() {
         };
         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));
+        assertEquals("Refinement Error", LJDiagnosticsHandler.diagnosticMessage(diagnostic));
     }
 }