--- a/src/Tools/VSCode/extension/media/sledgehammer.js Sun Oct 26 18:24:39 2025 +0100
+++ b/src/Tools/VSCode/extension/media/sledgehammer.js Sun Oct 26 18:26:49 2025 +0100
@@ -5,79 +5,79 @@
let history = [];
- const container = document.createElement('div');
- container.id = 'sledgehammer-container';
+ const container = document.createElement("div");
+ container.id = "sledgehammer-container";
- const top_row = document.createElement('div');
- top_row.classList.add('top-row');
+ const top_row = document.createElement("div");
+ top_row.classList.add("top-row");
- const provers_label = document.createElement('label');
- provers_label.textContent = 'Provers: ';
+ const provers_label = document.createElement("label");
+ provers_label.textContent = "Provers: ";
- const provers_input_wrapper = document.createElement('div');
- provers_input_wrapper.className = 'provers-input-wrapper';
+ const provers_input_wrapper = document.createElement("div");
+ provers_input_wrapper.className = "provers-input-wrapper";
- const provers_input = document.createElement('input');
- provers_input.type = 'text';
- provers_input.id = 'provers';
+ const provers_input = document.createElement("input");
+ provers_input.type = "text";
+ provers_input.id = "provers";
provers_input.size = 30;
- provers_input.value = '';
- provers_input.autocomplete = 'off';
+ provers_input.value = "";
+ provers_input.autocomplete = "off";
provers_input_wrapper.appendChild(provers_input);
- const chevron_button = document.createElement('button');
- chevron_button.type = 'button';
- chevron_button.className = 'provers-dropdown-toggle';
- chevron_button.setAttribute('aria-label', 'Show provers history');
+ const chevron_button = document.createElement("button");
+ chevron_button.type = "button";
+ chevron_button.className = "provers-dropdown-toggle";
+ chevron_button.setAttribute("aria-label", "Show provers history");
chevron_button.tabIndex = -1;
- chevron_button.innerHTML = '\u25bc';
+ chevron_button.innerHTML = "\u25bc";
provers_input_wrapper.appendChild(chevron_button);
provers_label.appendChild(provers_input_wrapper);
- const dropdown = document.createElement('div');
- dropdown.className = 'provers-dropdown';
+ const dropdown = document.createElement("div");
+ dropdown.className = "provers-dropdown";
provers_input_wrapper.appendChild(dropdown);
function show_dropdown() {
- dropdown.classList.add('visible');
+ dropdown.classList.add("visible");
}
function hide_dropdown() {
- dropdown.classList.remove('visible');
+ dropdown.classList.remove("visible");
}
function render_dropdown(open = false) {
- dropdown.innerHTML = '';
- const header = document.createElement('div');
- header.textContent = 'Previously entered strings:';
- header.className = 'history-header';
+ dropdown.innerHTML = "";
+ const header = document.createElement("div");
+ header.textContent = "Previously entered strings:";
+ header.className = "history-header";
dropdown.appendChild(header);
if (history.length === 0) {
- const no_entry = document.createElement('div');
- no_entry.className = 'history-header';
+ const no_entry = document.createElement("div");
+ no_entry.className = "history-header";
}
else {
history.forEach(item => {
- const row = document.createElement('div');
+ const row = document.createElement("div");
row.tabIndex = 0;
row.textContent = item;
- const delete_button = document.createElement('span');
- delete_button.textContent = '\u2716';
- delete_button.className = 'delete-btn';
- delete_button.title = 'Delete entry';
- delete_button.addEventListener('mousedown', function (ev) {
+ const delete_button = document.createElement("span");
+ delete_button.textContent = "\u2716";
+ delete_button.className = "delete-btn";
+ delete_button.title = "Delete entry";
+ delete_button.addEventListener("mousedown", function (ev) {
ev.preventDefault();
ev.stopPropagation();
history = history.filter(h => h !== item);
render_dropdown(false);
show_dropdown();
- vscode.postMessage({ command: 'delete_prover_history', entry: item });
+ vscode.postMessage({ command: "delete_prover_history", entry: item });
});
row.appendChild(delete_button);
- row.addEventListener('mousedown', function (e) {
+ row.addEventListener("mousedown", function (e) {
e.preventDefault();
provers_input.value = item;
hide_dropdown();
@@ -90,9 +90,9 @@
}
- chevron_button.addEventListener('mousedown', function (e) {
+ chevron_button.addEventListener("mousedown", function (e) {
e.preventDefault();
- if (dropdown.classList.contains('visible')) {
+ if (dropdown.classList.contains("visible")) {
hide_dropdown();
}
else {
@@ -102,20 +102,20 @@
}
});
- provers_input.addEventListener('input', () => { });
+ provers_input.addEventListener("input", () => { });
- provers_input.addEventListener('focus', function () {
+ provers_input.addEventListener("focus", function () {
render_dropdown(true);
show_dropdown();
});
- provers_input.addEventListener('blur', () => {
+ provers_input.addEventListener("blur", () => {
setTimeout(() => {
if (!dropdown.contains(document.activeElement)) hide_dropdown();
}, 150);
});
- provers_input.addEventListener('keydown', (e) => {
- if (e.key === 'ArrowDown' && dropdown.childNodes.length) {
+ provers_input.addEventListener("keydown", (e) => {
+ if (e.key === "ArrowDown" && dropdown.childNodes.length) {
dropdown.firstChild && dropdown.firstChild.focus && dropdown.firstChild.focus();
}
});
@@ -142,64 +142,64 @@
render_dropdown();
}
- const isar_label = document.createElement('label');
- const isar_checkbox = document.createElement('input');
- isar_checkbox.type = 'checkbox';
- isar_checkbox.id = 'isar';
+ const isar_label = document.createElement("label");
+ const isar_checkbox = document.createElement("input");
+ isar_checkbox.type = "checkbox";
+ isar_checkbox.id = "isar";
isar_label.appendChild(isar_checkbox);
- isar_label.appendChild(document.createTextNode(' Isar proofs'));
+ isar_label.appendChild(document.createTextNode(" Isar proofs"));
- const try0_label = document.createElement('label');
- const try0_checkbox = document.createElement('input');
- try0_checkbox.type = 'checkbox';
- try0_checkbox.id = 'try0';
+ const try0_label = document.createElement("label");
+ const try0_checkbox = document.createElement("input");
+ try0_checkbox.type = "checkbox";
+ try0_checkbox.id = "try0";
try0_checkbox.checked = true;
try0_label.appendChild(try0_checkbox);
- try0_label.appendChild(document.createTextNode(' Try methods'));
+ try0_label.appendChild(document.createTextNode(" Try methods"));
- provers_input.addEventListener('input', save_state);
- isar_checkbox.addEventListener('change', save_state);
- try0_checkbox.addEventListener('change', save_state);
- const spinner = document.createElement('div');
- spinner.id = 'sledgehammer-spinner';
+ provers_input.addEventListener("input", save_state);
+ isar_checkbox.addEventListener("change", save_state);
+ try0_checkbox.addEventListener("change", save_state);
+ const spinner = document.createElement("div");
+ spinner.id = "sledgehammer-spinner";
- const apply_button = document.createElement('button');
- apply_button.textContent = 'Apply';
- apply_button.id = 'apply-btn';
- apply_button.addEventListener('click', () => {
+ const apply_button = document.createElement("button");
+ apply_button.textContent = "Apply";
+ apply_button.id = "apply-btn";
+ apply_button.addEventListener("click", () => {
was_cancelled = false;
can_be_cancelled = true;
- result.innerHTML = '';
+ result.innerHTML = "";
add_to_history(provers_input.value);
hide_dropdown();
vscode.postMessage({
- command: 'apply',
+ command: "apply",
provers: provers_input.value,
isar: isar_checkbox.checked,
try0: try0_checkbox.checked
});
});
- const cancel_button = document.createElement('button');
- cancel_button.textContent = 'Cancel';
- cancel_button.addEventListener('click', () => {
- vscode.postMessage({ command: 'cancel' });
+ const cancel_button = document.createElement("button");
+ cancel_button.textContent = "Cancel";
+ cancel_button.addEventListener("click", () => {
+ vscode.postMessage({ command: "cancel" });
if (was_cancelled) return;
if (!can_be_cancelled) return;
was_cancelled = true;
- spinner.classList.remove('loading');
+ spinner.classList.remove("loading");
const div = document.createElement("div");
div.classList.add("interrupt");
div.textContent = "Interrupt";
result.appendChild(div);
});
- const locate_button = document.createElement('button');
- locate_button.textContent = 'Locate';
- locate_button.addEventListener('click', () => {
+ const locate_button = document.createElement("button");
+ locate_button.textContent = "Locate";
+ locate_button.addEventListener("click", () => {
vscode.postMessage({
- command: 'locate',
+ command: "locate",
provers: provers_input.value,
isar: isar_checkbox.checked,
try0: try0_checkbox.checked
@@ -215,20 +215,20 @@
top_row.appendChild(locate_button);
container.appendChild(top_row);
- const result = document.createElement('div');
- result.id = 'result';
+ const result = document.createElement("div");
+ result.id = "result";
container.appendChild(result);
document.body.appendChild(container);
render_dropdown();
- window.addEventListener('message', event => {
+ window.addEventListener("message", event => {
const message = event.data;
- if (message.command === 'status') {
- spinner.classList.toggle('loading', message.message !== "Finished");
+ if (message.command === "status") {
+ spinner.classList.toggle("loading", message.message !== "Finished");
}
- else if (message.command === 'provers') {
+ else if (message.command === "provers") {
set_history(message.history);
if (message.provers) {
provers_input.value = message.provers;
@@ -237,45 +237,45 @@
provers_input.value = message.history[0];
}
}
- else if (message.command === 'no_proof_context') {
+ else if (message.command === "no_proof_context") {
const div = document.createElement("div");
div.classList.add("interrupt");
div.textContent = "Unknown proof context";
result.appendChild(div);
}
- else if (message.command === 'no_provers') {
+ else if (message.command === "no_provers") {
const div = document.createElement("div");
div.classList.add("interrupt");
div.textContent = "No such provers";
result.appendChild(div);
}
- else if (message.command === 'result') {
+ else if (message.command === "result") {
if (was_cancelled) return;
- result.innerHTML = '';
+ result.innerHTML = "";
const parser = new DOMParser();
- const xml_doc = parser.parseFromString(`<root>${message.content}</root>`, 'application/xml');
- const messages = xml_doc.getElementsByTagName('writeln_message');
+ const xml_doc = parser.parseFromString(`<root>${message.content}</root>`, "application/xml");
+ const messages = xml_doc.getElementsByTagName("writeln_message");
for (const msg of messages) {
- const div = document.createElement('div');
+ const div = document.createElement("div");
const inner = msg.innerHTML;
- if (inner.includes('<sendback')) {
- const temp_container = document.createElement('div');
+ if (inner.includes("<sendback")) {
+ const temp_container = document.createElement("div");
temp_container.innerHTML = inner;
temp_container.childNodes.forEach(node => {
if (node.nodeType === Node.TEXT_NODE) {
const text = node.textContent.trim();
if (text) {
- const span = document.createElement('span');
+ const span = document.createElement("span");
span.textContent = text;
div.appendChild(span);
}
}
- else if (node.nodeName.toLowerCase() === 'sendback') {
- const button = document.createElement('button');
+ else if (node.nodeName.toLowerCase() === "sendback") {
+ const button = document.createElement("button");
button.textContent = node.textContent.trim();
- button.addEventListener('click', () => {
+ button.addEventListener("click", () => {
vscode.postMessage({
- command: 'insert_text',
+ command: "insert_text",
provers: provers_input.value,
isar: isar_checkbox.checked,
try0: try0_checkbox.checked,
@@ -285,7 +285,7 @@
div.appendChild(button);
}
else {
- const span = document.createElement('span');
+ const span = document.createElement("span");
span.textContent = node.textContent.trim();
div.appendChild(span);
}
@@ -297,10 +297,10 @@
result.appendChild(div);
}
if (/Unknown proof context/i.test(message.content)) {
- result.classList.add('error');
+ result.classList.add("error");
}
else {
- result.classList.remove('error');
+ result.classList.remove("error");
}
can_be_cancelled = false;
}
@@ -310,7 +310,7 @@
const saved = vscode.getState();
if (saved) {
history = Array.isArray(saved.history) ? saved.history : [];
- provers_input.value = saved.provers || '';
+ provers_input.value = saved.provers || "";
isar_checkbox.checked = !!saved.isar;
try0_checkbox.checked = saved.try0 !== undefined ? saved.try0 : true;
render_dropdown(false);