${escapeHtml(c)}`.replace(/&(lt|gt|amp);/g, "&$1;"));
text = text.replace(/\*\*([^*]+)\*\*/g, "$1");
text = text.replace(/\*([^*\n]+)\*/g, "$1");
const paragraphs = text
.split(/\n{2,}/)
.map((p) => `${p.replace(/\n/g, "
")}
${escapeHtml(b.body)}${escapeHtml(result.error || "unknown error")}`;
activeRun.bodyEl.appendChild(err);
return;
}
completePhase("report");
activeRun.phaseEls.forEach((e) => e.classList.remove("active"));
activeRun.phaseLineEls.forEach((e) => {
e.classList.remove("flowing");
e.classList.add("done");
});
stopRunTimer("done");
activeRun.nowLineEl.classList.add("done");
setNowLine(
!result.bugs || result.bugs.length === 0
? "no bugs confirmed"
: `${result.bugs.length} bug${result.bugs.length === 1 ? "" : "s"} confirmed`
);
// Auto-collapse the verbose log once the result is in view.
if (activeRun.logDiscEl) activeRun.logDiscEl.open = false;
const wrap = document.createElement("div");
wrap.className = "bug-summary";
if (!result.bugs || result.bugs.length === 0) {
wrap.innerHTML = `${escapeHtml(url)}`, { label: "tool" });
setStatus("working", "fetching");
} else if (evt.data.name === "run_aprover") {
appendRunCard();
setStatus("working", "verifying");
}
break;
case "tool_progress": {
const d = evt.data || {};
if (d.type === "fetch_result") {
const note = d.ok
? `← fetched ${d.bytes} bytes`
: `× fetch failed: ${escapeHtml(d.error || "")}`;
appendMsg("system", note, { label: "tool" });
} else if (d.type === "started") {
if (activeRun) logRunLine("info", "pipeline started");
} else if (d.type === "log") {
logRunLine(d.level, d.message);
} else if (d.type === "error") {
logRunLine("error", d.message);
} else if (d.type === "result") {
renderResult(d.result || {});
setStatus("thinking", "summarizing");
}
break;
}
case "error":
appendMsg("system", `server error: ${escapeHtml(evt.data.message || "unknown")}`);
setStatus("error", "error");
break;
case "done":
break;
}
}
// ---- Composer wiring ----
function autoGrow() {
input.style.height = "auto";
input.style.height = Math.min(input.scrollHeight, 220) + "px";
}
input.addEventListener("input", autoGrow);
input.addEventListener("keydown", (e) => {
if (e.key === "Enter" && !e.shiftKey) {
e.preventDefault();
form.requestSubmit();
}
});
form.addEventListener("submit", (e) => {
e.preventDefault();
if (busy) return;
const text = input.value.trim();
if (!text) return;
if (!getApiKey()) {
appendMsg("system", "Add your Anthropic API key below to run AProver — it stays in your browser.");
if (apiKeyInput) {
apiKeyInput.focus();
apiKeyInput.classList.add("key-needed");
setTimeout(() => apiKeyInput.classList.remove("key-needed"), 1500);
}
return;
}
appendMsg("user", renderMarkdown(text), { label: "you" });
history.push({ role: "user", content: text });
input.value = "";
autoGrow();
streamChat().catch((err) => {
appendMsg("system", `client error: ${escapeHtml(String(err))}`);
setBusy(false);
});
});
// Quick-action chips: prefill the composer (or send immediately if the prompt
// is a self-contained command).
document.querySelectorAll(".chip").forEach((chip) => {
chip.addEventListener("click", () => {
const prompt = chip.getAttribute("data-prompt") || "";
input.value = prompt;
autoGrow();
input.focus();
// If the prompt ends with ": " (i.e. expects user completion), don't auto-send.
if (!/[:?\s]$/.test(prompt)) {
form.requestSubmit();
}
});
});
// ---- Hero live-preview demo ----
// Drives a looping fake run on the hero so visitors see the agent in motion
// before they ever type anything. Hover pauses; click loads the snippet into
// the composer so they can run it for real.
const DEMO_SOURCE = `#include