diff -r 3de18e94ac7c -r 486e094b676c src/Tools/VSCode/extension/media/sledgehammer.js
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/VSCode/extension/media/sledgehammer.js	Thu Oct 23 16:15:40 2025 +0200
@@ -0,0 +1,317 @@
+(function () {
+  const vscode = acquireVsCodeApi();
+  let wasCancelled = false;
+  let kannbeCancelled = false;
+
+  let history = []; 
+
+  const container = document.createElement('div');
+  container.id = 'sledgehammer-container';
+
+  const topRow = document.createElement('div');
+  topRow.classList.add('top-row');
+
+  const proversLabel = document.createElement('label');
+  proversLabel.textContent = 'Provers: ';
+
+  const proversInputWrapper = document.createElement('div');
+  proversInputWrapper.className = 'provers-input-wrapper';
+
+  const proversInput = document.createElement('input');
+  proversInput.type = 'text';
+  proversInput.id = 'provers';
+  proversInput.size = 30;
+  proversInput.value = '';
+  proversInput.autocomplete = 'off';
+
+  proversInputWrapper.appendChild(proversInput);
+
+  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 = '▼';
+  proversInputWrapper.appendChild(chevronBtn);
+
+  proversLabel.appendChild(proversInputWrapper);
+
+  const dropdown = document.createElement('div');
+  dropdown.className = 'provers-dropdown';
+  proversInputWrapper.appendChild(dropdown);
+
+  function showDropdown() {
+    dropdown.classList.add('visible');
+  }
+  function hideDropdown() {
+    dropdown.classList.remove('visible');
+  }
+
+  function renderDropdown(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 {
+      history.forEach(item => {
+        const row = document.createElement('div');
+        row.tabIndex = 0;
+        row.textContent = item;
+
+        const delBtn = document.createElement('span');
+        delBtn.textContent = '✖';
+        delBtn.className = 'delete-btn';
+        delBtn.title = 'Delete entry';
+        delBtn.addEventListener('mousedown', function (ev) {
+          ev.preventDefault();
+          ev.stopPropagation();
+          history = history.filter(h => h !== item);
+          renderDropdown(false);
+          showDropdown();
+
+          vscode.postMessage({
+            command: 'delete_prover_history',
+            entry: item
+          });
+        });
+
+        row.appendChild(delBtn);
+        row.addEventListener('mousedown', function (e) {
+          e.preventDefault();
+          proversInput.value = item;
+          hideDropdown();
+          proversInput.focus();
+        });
+        dropdown.appendChild(row);
+      });
+    }
+    if (open) showDropdown(); else hideDropdown();
+  }
+
+
+  chevronBtn.addEventListener('mousedown', function (e) {
+    e.preventDefault();
+    if (dropdown.classList.contains('visible')) {
+      hideDropdown();
+    } else {
+      renderDropdown(true);
+      showDropdown();
+      proversInput.focus();
+    }
+  });
+
+  proversInput.addEventListener('input', () => { });
+
+  proversInput.addEventListener('focus', function () {
+    renderDropdown(true);
+    showDropdown();
+  });
+  proversInput.addEventListener('blur', () => {
+    setTimeout(() => {
+      if (!dropdown.contains(document.activeElement)) hideDropdown();
+    }, 150);
+  });
+
+  proversInput.addEventListener('keydown', (e) => {
+    if (e.key === 'ArrowDown' && dropdown.childNodes.length) {
+      dropdown.firstChild && dropdown.firstChild.focus && dropdown.firstChild.focus();
+    }
+  });
+
+  function setHistory(newHistory) {
+    history = Array.isArray(newHistory) ? newHistory : [];
+    saveState();
+    renderDropdown(false);
+  }
+
+  function saveState() {
+    vscode.setState({
+      history,
+      provers: proversInput.value,
+      isar: isarCheckbox.checked,
+      try0: try0Checkbox.checked
+    });
+  }
+
+  function addToHistory(entry) {
+    if (!entry.trim()) return;
+    history = [entry, ...history.filter((h) => h !== entry)].slice(0, 10);
+    saveState();
+    renderDropdown();
+  }
+
+  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 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'));
+
+
+  proversInput.addEventListener('input', saveState);
+  isarCheckbox.addEventListener('change', saveState);
+  try0Checkbox.addEventListener('change', saveState);
+  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;
+    result.innerHTML = '';
+    addToHistory(proversInput.value); 
+    hideDropdown();
+    vscode.postMessage({
+      command: 'apply',
+      provers: proversInput.value,
+      isar: isarCheckbox.checked,
+      try0: try0Checkbox.checked
+    });
+  });
+
+  const cancelBtn = document.createElement('button');
+  cancelBtn.textContent = 'Cancel';
+  cancelBtn.addEventListener('click', () => {
+    vscode.postMessage({ command: 'cancel' });
+    if (wasCancelled) return;
+    if (!kannbeCancelled) return;
+    wasCancelled = true;
+    spinner.classList.remove('loading');
+    const div = document.createElement("div");
+    div.classList.add("interrupt");
+    div.textContent = "Interrupt";
+    result.appendChild(div);
+  });
+
+  const locateBtn = document.createElement('button');
+  locateBtn.textContent = 'Locate';
+  locateBtn.addEventListener('click', () => {
+    vscode.postMessage({
+      command: 'locate',
+      provers: proversInput.value,
+      isar: isarCheckbox.checked,
+      try0: try0Checkbox.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);
+
+  const result = document.createElement('div');
+  result.id = 'result';
+  container.appendChild(result);
+
+  document.body.appendChild(container);
+
+  renderDropdown();
+
+  window.addEventListener('message', event => {
+    const message = event.data;
+    if (message.command === 'status') {
+      spinner.classList.toggle('loading', message.message !== "Beendet");
+    }
+    else if (message.command === 'provers') {
+      setHistory(message.history);
+      if (message.provers) {
+        proversInput.value = message.provers;
+      } else if (message.history && message.history.length > 0) {
+        proversInput.value = message.history[0];
+      }
+    }
+
+    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') {
+      const div = document.createElement("div");
+      div.classList.add("interrupt");
+      div.textContent = "No such provers";
+      result.appendChild(div);
+    }
+    else if (message.command === 'result') {
+      if (wasCancelled) return;
+      result.innerHTML = '';
+      const parser = new DOMParser();
+      const xmlDoc = parser.parseFromString(`<root>${message.content}</root>`, 'application/xml');
+      const messages = xmlDoc.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 => {
+            if (node.nodeType === Node.TEXT_NODE) {
+              const text = node.textContent.trim();
+              if (text) {
+                const span = document.createElement('span');
+                span.textContent = text;
+                div.appendChild(span);
+              }
+            } else if (node.nodeName.toLowerCase() === 'sendback') {
+              const button = document.createElement('button');
+              button.textContent = node.textContent.trim();
+              button.addEventListener('click', () => {
+                vscode.postMessage({
+                  command: 'insert_text',
+                  provers: proversInput.value,
+                  isar: isarCheckbox.checked,
+                  try0: try0Checkbox.checked,
+                  text: node.textContent.trim()
+                });
+              });
+              div.appendChild(button);
+            } else {
+              const span = document.createElement('span');
+              span.textContent = node.textContent.trim();
+              div.appendChild(span);
+            }
+          });
+        } else {
+          div.textContent = msg.textContent.trim();
+        }
+        result.appendChild(div);
+      }
+      if (/Unknown proof context/i.test(message.content)) {
+        result.classList.add('error');
+      } else {
+        result.classList.remove('error');
+      }
+      kannbeCancelled = false;
+    }
+  });
+
+  window.onload = function () {
+    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);
+    }
+  };
+})();