--- a/src/Tools/VSCode/extension/media/sledgehammer.js Sun Oct 26 14:20:56 2025 +0100
+++ b/src/Tools/VSCode/extension/media/sledgehammer.js Sun Oct 26 14:33:16 2025 +0100
@@ -1,191 +1,193 @@
(function () {
const vscode = acquireVsCodeApi();
- let wasCancelled = false;
- let kannbeCancelled = false;
+ let was_cancelled = false;
+ let can_be_cancelled = false;
let history = [];
const container = document.createElement('div');
container.id = 'sledgehammer-container';
- const topRow = document.createElement('div');
- topRow.classList.add('top-row');
+ const top_row = document.createElement('div');
+ top_row.classList.add('top-row');
- const proversLabel = document.createElement('label');
- proversLabel.textContent = 'Provers: ';
+ const provers_label = document.createElement('label');
+ provers_label.textContent = 'Provers: ';
- const proversInputWrapper = document.createElement('div');
- proversInputWrapper.className = 'provers-input-wrapper';
+ const provers_input_wrapper = document.createElement('div');
+ provers_input_wrapper.className = 'provers-input-wrapper';
- const proversInput = document.createElement('input');
- proversInput.type = 'text';
- proversInput.id = 'provers';
- proversInput.size = 30;
- proversInput.value = '';
- proversInput.autocomplete = 'off';
+ 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';
- proversInputWrapper.appendChild(proversInput);
+ provers_input_wrapper.appendChild(provers_input);
- const chevronBtn = document.createElement('button');
- chevronBtn.type = 'button';
- chevronBtn.className = 'provers-dropdown-toggle';
- chevronBtn.setAttribute('aria-label', 'Show provers history');
- chevronBtn.tabIndex = -1;
- chevronBtn.innerHTML = '\u25bc';
- proversInputWrapper.appendChild(chevronBtn);
+ 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';
+ provers_input_wrapper.appendChild(chevron_button);
- proversLabel.appendChild(proversInputWrapper);
+ provers_label.appendChild(provers_input_wrapper);
const dropdown = document.createElement('div');
dropdown.className = 'provers-dropdown';
- proversInputWrapper.appendChild(dropdown);
+ provers_input_wrapper.appendChild(dropdown);
- function showDropdown() {
+ function show_dropdown() {
dropdown.classList.add('visible');
}
- function hideDropdown() {
+ function hide_dropdown() {
dropdown.classList.remove('visible');
}
- function renderDropdown(open = false) {
+ function render_dropdown(open = false) {
dropdown.innerHTML = '';
const header = document.createElement('div');
header.textContent = 'Previously entered strings:';
header.className = 'history-header';
dropdown.appendChild(header);
if (history.length === 0) {
- const noEntry = document.createElement('div');
- noEntry.className = 'history-header';
- } else {
+ const no_entry = document.createElement('div');
+ no_entry.className = 'history-header';
+ }
+ else {
history.forEach(item => {
const row = document.createElement('div');
row.tabIndex = 0;
row.textContent = item;
- const delBtn = document.createElement('span');
- delBtn.textContent = '\u2716';
- delBtn.className = 'delete-btn';
- delBtn.title = 'Delete entry';
- delBtn.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);
- renderDropdown(false);
- showDropdown();
+ render_dropdown(false);
+ show_dropdown();
vscode.postMessage({ command: 'delete_prover_history', entry: item });
});
- row.appendChild(delBtn);
+ row.appendChild(delete_button);
row.addEventListener('mousedown', function (e) {
e.preventDefault();
- proversInput.value = item;
- hideDropdown();
- proversInput.focus();
+ provers_input.value = item;
+ hide_dropdown();
+ provers_input.focus();
});
dropdown.appendChild(row);
});
}
- if (open) showDropdown(); else hideDropdown();
+ if (open) show_dropdown(); else hide_dropdown();
}
- chevronBtn.addEventListener('mousedown', function (e) {
+ chevron_button.addEventListener('mousedown', function (e) {
e.preventDefault();
if (dropdown.classList.contains('visible')) {
- hideDropdown();
- } else {
- renderDropdown(true);
- showDropdown();
- proversInput.focus();
+ hide_dropdown();
+ }
+ else {
+ render_dropdown(true);
+ show_dropdown();
+ provers_input.focus();
}
});
- proversInput.addEventListener('input', () => { });
+ provers_input.addEventListener('input', () => { });
- proversInput.addEventListener('focus', function () {
- renderDropdown(true);
- showDropdown();
+ provers_input.addEventListener('focus', function () {
+ render_dropdown(true);
+ show_dropdown();
});
- proversInput.addEventListener('blur', () => {
+ provers_input.addEventListener('blur', () => {
setTimeout(() => {
- if (!dropdown.contains(document.activeElement)) hideDropdown();
+ if (!dropdown.contains(document.activeElement)) hide_dropdown();
}, 150);
});
- proversInput.addEventListener('keydown', (e) => {
+ provers_input.addEventListener('keydown', (e) => {
if (e.key === 'ArrowDown' && dropdown.childNodes.length) {
dropdown.firstChild && dropdown.firstChild.focus && dropdown.firstChild.focus();
}
});
- function setHistory(newHistory) {
+ function set_history(newHistory) {
history = Array.isArray(newHistory) ? newHistory : [];
- saveState();
- renderDropdown(false);
+ save_state();
+ render_dropdown(false);
}
- function saveState() {
+ function save_state() {
vscode.setState({
history,
- provers: proversInput.value,
- isar: isarCheckbox.checked,
- try0: try0Checkbox.checked
+ provers: provers_input.value,
+ isar: isar_checkbox.checked,
+ try0: try0_checkbox.checked
});
}
- function addToHistory(entry) {
+ function add_to_history(entry) {
if (!entry.trim()) return;
history = [entry, ...history.filter((h) => h !== entry)].slice(0, 10);
- saveState();
- renderDropdown();
+ save_state();
+ render_dropdown();
}
- const isarLabel = document.createElement('label');
- const isarCheckbox = document.createElement('input');
- isarCheckbox.type = 'checkbox';
- isarCheckbox.id = 'isar';
- isarLabel.appendChild(isarCheckbox);
- isarLabel.appendChild(document.createTextNode(' Isar proofs'));
+ 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'));
- const try0Label = document.createElement('label');
- const try0Checkbox = document.createElement('input');
- try0Checkbox.type = 'checkbox';
- try0Checkbox.id = 'try0';
- try0Checkbox.checked = true;
- try0Label.appendChild(try0Checkbox);
- try0Label.appendChild(document.createTextNode(' Try methods'));
+ 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'));
- proversInput.addEventListener('input', saveState);
- isarCheckbox.addEventListener('change', saveState);
- try0Checkbox.addEventListener('change', saveState);
+ 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 applyBtn = document.createElement('button');
- applyBtn.textContent = 'Apply';
- applyBtn.id = 'apply-btn';
- applyBtn.addEventListener('click', () => {
- wasCancelled = false;
- kannbeCancelled = true;
+ 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 = '';
- addToHistory(proversInput.value);
- hideDropdown();
+ add_to_history(provers_input.value);
+ hide_dropdown();
vscode.postMessage({
command: 'apply',
- provers: proversInput.value,
- isar: isarCheckbox.checked,
- try0: try0Checkbox.checked
+ provers: provers_input.value,
+ isar: isar_checkbox.checked,
+ try0: try0_checkbox.checked
});
});
- const cancelBtn = document.createElement('button');
- cancelBtn.textContent = 'Cancel';
- cancelBtn.addEventListener('click', () => {
+ const cancel_button = document.createElement('button');
+ cancel_button.textContent = 'Cancel';
+ cancel_button.addEventListener('click', () => {
vscode.postMessage({ command: 'cancel' });
- if (wasCancelled) return;
- if (!kannbeCancelled) return;
- wasCancelled = true;
+ if (was_cancelled) return;
+ if (!can_be_cancelled) return;
+ was_cancelled = true;
spinner.classList.remove('loading');
const div = document.createElement("div");
div.classList.add("interrupt");
@@ -193,25 +195,25 @@
result.appendChild(div);
});
- const locateBtn = document.createElement('button');
- locateBtn.textContent = 'Locate';
- locateBtn.addEventListener('click', () => {
+ const locate_button = document.createElement('button');
+ locate_button.textContent = 'Locate';
+ locate_button.addEventListener('click', () => {
vscode.postMessage({
command: 'locate',
- provers: proversInput.value,
- isar: isarCheckbox.checked,
- try0: try0Checkbox.checked
+ provers: provers_input.value,
+ isar: isar_checkbox.checked,
+ try0: try0_checkbox.checked
});
});
- topRow.appendChild(proversLabel);
- topRow.appendChild(isarLabel);
- topRow.appendChild(try0Label);
- topRow.appendChild(spinner);
- topRow.appendChild(applyBtn);
- topRow.appendChild(cancelBtn);
- topRow.appendChild(locateBtn);
- container.appendChild(topRow);
+ top_row.appendChild(provers_label);
+ top_row.appendChild(isar_label);
+ top_row.appendChild(try0_label);
+ top_row.appendChild(spinner);
+ top_row.appendChild(apply_button);
+ top_row.appendChild(cancel_button);
+ top_row.appendChild(locate_button);
+ container.appendChild(top_row);
const result = document.createElement('div');
result.id = 'result';
@@ -219,7 +221,7 @@
document.body.appendChild(container);
- renderDropdown();
+ render_dropdown();
window.addEventListener('message', event => {
const message = event.data;
@@ -227,14 +229,13 @@
spinner.classList.toggle('loading', message.message !== "Beendet");
}
else if (message.command === 'provers') {
- setHistory(message.history);
+ set_history(message.history);
if (message.provers) {
- proversInput.value = message.provers;
+ provers_input.value = message.provers;
} else if (message.history && message.history.length > 0) {
- proversInput.value = message.history[0];
+ provers_input.value = message.history[0];
}
}
-
else if (message.command === 'no_proof_context') {
const div = document.createElement("div");
div.classList.add("interrupt");
@@ -248,18 +249,18 @@
result.appendChild(div);
}
else if (message.command === 'result') {
- if (wasCancelled) return;
+ if (was_cancelled) return;
result.innerHTML = '';
const parser = new DOMParser();
- const xmlDoc = parser.parseFromString(`<root>${message.content}</root>`, 'application/xml');
- const messages = xmlDoc.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 inner = msg.innerHTML;
if (inner.includes('<sendback')) {
- const tempContainer = document.createElement('div');
- tempContainer.innerHTML = inner;
- tempContainer.childNodes.forEach(node => {
+ 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) {
@@ -273,20 +274,22 @@
button.addEventListener('click', () => {
vscode.postMessage({
command: 'insert_text',
- provers: proversInput.value,
- isar: isarCheckbox.checked,
- try0: try0Checkbox.checked,
+ provers: provers_input.value,
+ isar: isar_checkbox.checked,
+ try0: try0_checkbox.checked,
text: node.textContent.trim()
});
});
div.appendChild(button);
- } else {
+ }
+ else {
const span = document.createElement('span');
span.textContent = node.textContent.trim();
div.appendChild(span);
}
});
- } else {
+ }
+ else {
div.textContent = msg.textContent.trim();
}
result.appendChild(div);
@@ -296,7 +299,7 @@
} else {
result.classList.remove('error');
}
- kannbeCancelled = false;
+ can_be_cancelled = false;
}
});
@@ -304,10 +307,10 @@
const saved = vscode.getState();
if (saved) {
history = Array.isArray(saved.history) ? saved.history : [];
- proversInput.value = saved.provers || '';
- isarCheckbox.checked = !!saved.isar;
- try0Checkbox.checked = saved.try0 !== undefined ? saved.try0 : true;
- renderDropdown(false);
+ provers_input.value = saved.provers || '';
+ isar_checkbox.checked = !!saved.isar;
+ try0_checkbox.checked = saved.try0 !== undefined ? saved.try0 : true;
+ render_dropdown(false);
}
};
})();