# HG changeset patch
# User wenzelm
# Date 1761485596 -3600
# Node ID d2a9248792cf8c51db09adcd2a1cbdee8da3bc76
# Parent  8026f3a3146dcd229436ee1c1e6d85d8a1c7ee6b
tuned names: avoid camel-case;

diff -r 8026f3a3146d -r d2a9248792cf src/Tools/VSCode/extension/media/sledgehammer.js
--- 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);
     }
   };
 })();