# HG changeset patch
# User wenzelm
# Date 1761228940 -7200
# Node ID 486e094b676c2e9d82499d636431284bdd7c955b
# Parent  3de18e94ac7c94981632e764dbfb3686ada1d7b3
various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München;

diff -r 3de18e94ac7c -r 486e094b676c etc/build.props
--- a/etc/build.props	Thu Oct 23 14:49:21 2025 +0200
+++ b/etc/build.props	Thu Oct 23 16:15:40 2025 +0200
@@ -283,6 +283,7 @@
   src/Tools/VSCode/src/language_server.scala \
   src/Tools/VSCode/src/lsp.scala \
   src/Tools/VSCode/src/pretty_text_panel.scala \
+  src/Tools/VSCode/src/sledgehammer_panel.scala \
   src/Tools/VSCode/src/preview_panel.scala \
   src/Tools/VSCode/src/state_panel.scala \
   src/Tools/VSCode/src/vscode_main.scala \
diff -r 3de18e94ac7c -r 486e094b676c src/Pure/PIDE/query_operation.scala
--- a/src/Pure/PIDE/query_operation.scala	Thu Oct 23 14:49:21 2025 +0200
+++ b/src/Pure/PIDE/query_operation.scala	Thu Oct 23 16:15:40 2025 +0200
@@ -166,13 +166,13 @@
     editor.require_dispatcher { editor.session.cancel_exec(current_state.value.exec_id) }
 
   def apply_query(query: List[String]): Unit = {
-    editor.require_dispatcher {}
+    editor.send_dispatcher {
 
-    editor.current_node_snapshot(editor_context) match {
-      case Some(snapshot) =>
-        remove_overlay()
-        current_state.change(_ => Query_Operation.State.empty)
-        consume_output(Document.Snapshot.init, Command.Results.empty, Nil)
+      editor.current_node_snapshot(editor_context) match {
+        case Some(snapshot) =>
+          remove_overlay()
+          current_state.change(_ => Query_Operation.State.empty)
+          consume_output(Document.Snapshot.init, Command.Results.empty, Nil)
 
         editor.current_command(editor_context, snapshot) match {
           case Some(command) =>
@@ -182,9 +182,10 @@
           case None =>
         }
 
-        consume_status(current_state.value.status)
-        editor.flush()
-      case None =>
+          consume_status(current_state.value.status)
+          editor.flush()
+        case None =>
+      }
     }
   }
 
diff -r 3de18e94ac7c -r 486e094b676c src/Tools/VSCode/etc/options
--- a/src/Tools/VSCode/etc/options	Thu Oct 23 14:49:21 2025 +0200
+++ b/src/Tools/VSCode/etc/options	Thu Oct 23 16:15:40 2025 +0200
@@ -3,6 +3,9 @@
 option vscode_input_delay : real = 0.1 for vscode
   -- "delay for client input (edits)"
 
+option sledgehammer_provers_history : string = "" for vscode
+  -- "history of used Sledgehammer provers"
+
 option vscode_output_delay : real = 0.5 for vscode
   -- "delay for client output (rendering)"
 
diff -r 3de18e94ac7c -r 486e094b676c src/Tools/VSCode/extension/MANIFEST
--- a/src/Tools/VSCode/extension/MANIFEST	Thu Oct 23 14:49:21 2025 +0200
+++ b/src/Tools/VSCode/extension/MANIFEST	Thu Oct 23 16:15:40 2025 +0200
@@ -5,15 +5,26 @@
 isabelle_vscode.png
 media/main.js
 media/Preview_inverse.svg
+media/documentation-panel.svg
+media/symbol-panel.svg
+media/sledgehammer-panel.svg
+media/output-panel.svg
 media/PreviewOnRightPane_16x_dark.svg
 media/PreviewOnRightPane_16x.svg
 media/Preview.svg
 media/ViewSource_inverse.svg
 media/ViewSource.svg
 media/vscode.css
+media/symbols.css
+media/symbols.js
+media/documentation.css
+media/documentation.js
+media/sledgehammer.css
+media/sledgehammer.js
 package.json
 README.md
 src/decorations.ts
+src/documentation_panel.ts
 src/extension.ts
 src/file.ts
 src/library.ts
@@ -22,7 +33,9 @@
 src/platform.ts
 src/preview_panel.ts
 src/script_decorations.ts
+src/sledgehammer_panel.ts
 src/state_panel.ts
+src/symbol_panel.ts
 src/vscode_lib.ts
 test/extension.test.ts
 test/index.ts
diff -r 3de18e94ac7c -r 486e094b676c src/Tools/VSCode/extension/media/documentation-panel.svg
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/VSCode/extension/media/documentation-panel.svg	Thu Oct 23 16:15:40 2025 +0200
@@ -0,0 +1,1 @@
+<svg width="16" height="16" viewBox="0 0 16 16" xmlns="http://www.w3.org/2000/svg" fill="currentColor"><path fill-rule="evenodd" clip-rule="evenodd" d="M14.5 2H9l-.35.15-.65.64-.65-.64L7 2H1.5l-.5.5v10l.5.5h5.29l.86.85h.7l.86-.85h5.29l.5-.5v-10l-.5-.5zm-7 10.32l-.18-.17L7 12H2V3h4.79l.74.74-.03 8.58zM14 12H9l-.35.15-.14.13V3.7l.7-.7H14v9zM6 5H3v1h3V5zm0 4H3v1h3V9zM3 7h3v1H3V7zm10-2h-3v1h3V5zm-3 2h3v1h-3V7zm0 2h3v1h-3V9z"/></svg>
\ No newline at end of file
diff -r 3de18e94ac7c -r 486e094b676c src/Tools/VSCode/extension/media/documentation.css
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/VSCode/extension/media/documentation.css	Thu Oct 23 16:15:40 2025 +0200
@@ -0,0 +1,66 @@
+:root {
+  --container-paddding: 20px;
+  --input-padding-vertical: 6px;
+  --input-padding-horizontal: 4px;
+  --input-margin-vertical: 4px;
+  --input-margin-horizontal: 0;
+}
+
+--font-size-base: var(--vscode-editor-font-size);
+--font-size-small: calc(var(--font-size-base) * 0.85);
+
+body {
+  font-family: var(--vscode-editor-font-family);
+  font-size: var(--font-size-base);
+  color: var(--vscode-foreground);
+  background-color: var(--vscode-sideBar-background);
+  padding: var(--container-paddding);
+  margin: 0;
+}
+
+.doc-list {
+  list-style-type: none;
+  padding-left: 0;
+}
+
+.doc-section {
+  font-weight: normal;
+}
+.section-title {
+  font-weight: normal;
+  color: var(--vscode-foreground);
+}
+
+.doc-sublist {
+  list-style-type: none;
+  padding-left: 10px;
+}
+
+.doc-link {
+  color: var(--vscode-textLink-foreground);
+  text-decoration: none;
+  outline: none;
+}
+
+.doc-link:focus {
+  outline: none; 
+}
+
+.doc-entry {
+  margin: 2px 0;
+  cursor: pointer;
+}
+
+.doc-entry.selected {
+  background-color: var(--vscode-list-activeSelectionBackground);
+  color: var(--vscode-list-activeSelectionForeground);
+}
+
+.doc-entry.selected .doc-link {
+  color: var(--vscode-list-activeSelectionForeground);
+}
+
+.doc-entry:not(.selected) .doc-link:hover {
+  background-color: var(--vscode-list-hoverBackground);
+  color: var(--vscode-list-hoverForeground);
+}
diff -r 3de18e94ac7c -r 486e094b676c src/Tools/VSCode/extension/media/documentation.js
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/VSCode/extension/media/documentation.js	Thu Oct 23 16:15:40 2025 +0200
@@ -0,0 +1,105 @@
+(function () {
+    const vscode = acquireVsCodeApi();
+  
+    window.addEventListener("message", event => {
+      const message = event.data;
+  
+      if (message.command === "update" && Array.isArray(message.sections)) {
+        renderDocumentation(message.sections);
+      }
+    });
+  
+    function renderDocumentation(sections) {
+      const container = document.getElementById("documentation-container");
+      if (!container) return;
+      container.innerHTML = "";
+
+      vscode.setState({ sections: sections });
+  
+      const list = document.createElement("ul");
+      list.classList.add("doc-list");
+  
+      let selectedEntry = null;
+  
+      sections.forEach(section => {
+        const sectionItem = document.createElement("li");
+        sectionItem.classList.add("doc-section");
+  
+        const titleElement = document.createElement("span");
+        titleElement.textContent = section.title;
+        titleElement.classList.add("section-title");
+  
+        const subList = document.createElement("ul");
+        subList.classList.add("doc-sublist");
+        subList.style.display = section.important ? "block" : "none";
+  
+        titleElement.addEventListener("click", () => {
+          subList.style.display = subList.style.display === "none" ? "block" : "none";
+        });
+  
+        section.entries.forEach(entry => {
+          const entryItem = document.createElement("li");
+          entryItem.classList.add("doc-entry");
+  
+          let cleanedPath = entry.path.replace(/["]/g, "");
+          if (section.title.includes("Examples")) {
+            cleanedPath = cleanedPath.replace(/^.*?src\//, "src/");
+          }
+          if (section.title.includes("Release Notes")) {
+            cleanedPath = cleanedPath.replace(/^\$ISABELLE_HOME\//, "");
+          }
+  
+          let displayText = cleanedPath;
+          const match = cleanedPath.match(/([^\/]+?)(?:\.pdf)?$/);
+          if (match) {
+            const filename = match[1];
+            const cleanTitle = entry.title.replace(/["']/g, "").trim();
+            displayText = `<b>${filename}</b>${cleanTitle ? ': ' + cleanTitle : ''}`;
+          }
+  
+          const entryLink = document.createElement("a");
+          entryLink.innerHTML = displayText;
+          entryLink.href = "#";
+          entryLink.classList.add("doc-link");
+  
+          entryLink.addEventListener("click", event => {
+            event.preventDefault();
+  
+            if (selectedEntry && selectedEntry !== entryItem) {
+              selectedEntry.classList.remove("selected");
+            }
+  
+            if (selectedEntry === entryItem) {
+              selectedEntry.classList.remove("selected");
+              selectedEntry = null;
+            } else {
+              selectedEntry = entryItem;
+              entryItem.classList.add("selected");
+              openFile(entry.path);
+            }
+          });
+  
+          entryItem.appendChild(entryLink);
+          subList.appendChild(entryItem);
+        });
+  
+        sectionItem.appendChild(titleElement);
+        sectionItem.appendChild(subList);
+        list.appendChild(sectionItem);
+      });
+  
+      container.appendChild(list);
+    }
+  
+    function openFile(filePath) {
+      vscode.postMessage({ command: "openFile", path: filePath });
+    }
+  
+    window.onload = function () {
+        const savedState = vscode.getState();
+        if (savedState && savedState.sections) {
+          renderDocumentation(savedState.sections);
+        }
+      };
+  })();
+  
\ No newline at end of file
diff -r 3de18e94ac7c -r 486e094b676c src/Tools/VSCode/extension/media/output-panel.svg
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/VSCode/extension/media/output-panel.svg	Thu Oct 23 16:15:40 2025 +0200
@@ -0,0 +1,1 @@
+<svg width="24" height="24" viewBox="0 0 24 24" xmlns="http://www.w3.org/2000/svg" fill="currentColor"><path fill-rule="evenodd" clip-rule="evenodd" d="M19.5 0v1.5L21 3v19.5L19.5 24h-15L3 22.5V3l1.5-1.5V0H6v1.5h3V0h1.5v1.5h3V0H15v1.5h3V0h1.5zm-15 22.5h15V3h-15v19.5zM7.5 6h9v1.5h-9V6zm9 6h-9v1.5h9V12zm-9 6h9v1.5h-9V18z"/></svg>
\ No newline at end of file
diff -r 3de18e94ac7c -r 486e094b676c src/Tools/VSCode/extension/media/sledgehammer-panel.svg
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/VSCode/extension/media/sledgehammer-panel.svg	Thu Oct 23 16:15:40 2025 +0200
@@ -0,0 +1,1 @@
+<svg width="16" height="16" viewBox="0 0 16 16" xmlns="http://www.w3.org/2000/svg" fill="currentColor"><path fill-rule="evenodd" clip-rule="evenodd" d="M11.67 8.658a3.661 3.661 0 0 0-.781 1.114 3.28 3.28 0 0 0-.268 1.329v1.6a1.304 1.304 0 0 1-.794 1.197 1.282 1.282 0 0 1-.509.102H7.712a1.285 1.285 0 0 1-.922-.379 1.303 1.303 0 0 1-.38-.92v-1.6c0-.479-.092-.921-.274-1.329a3.556 3.556 0 0 0-.776-1.114 4.689 4.689 0 0 1-1.006-1.437A4.187 4.187 0 0 1 4 5.5a4.432 4.432 0 0 1 .616-2.27c.197-.336.432-.64.705-.914a4.6 4.6 0 0 1 .911-.702c.338-.196.7-.348 1.084-.454a4.45 4.45 0 0 1 1.2-.16 4.476 4.476 0 0 1 2.276.614 4.475 4.475 0 0 1 1.622 1.616 4.438 4.438 0 0 1 .616 2.27c0 .617-.117 1.191-.353 1.721a4.69 4.69 0 0 1-1.006 1.437zM9.623 10.5H7.409v2.201c0 .081.028.15.09.212a.29.29 0 0 0 .213.09h1.606a.289.289 0 0 0 .213-.09.286.286 0 0 0 .09-.212V10.5z"/></svg>
\ No newline at end of file
diff -r 3de18e94ac7c -r 486e094b676c src/Tools/VSCode/extension/media/sledgehammer.css
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/VSCode/extension/media/sledgehammer.css	Thu Oct 23 16:15:40 2025 +0200
@@ -0,0 +1,300 @@
+:root {
+  --container-paddding: 20px;
+  --input-padding-vertical: 6px;
+  --input-padding-horizontal: 4px;
+  --input-margin-vertical: 4px;
+  --input-margin-horizontal: 0;
+}
+
+--font-size-base: var(--vscode-editor-font-size);
+--font-size-small: calc(var(--font-size-base) * 0.85);
+--font-size-tiny:  calc(var(--font-size-base) * 0.75);
+
+body {
+  padding: 0 var(--container-paddding);
+  font-size: var(--vscode-editor-font-size);
+  font-weight: var(--vscode-editor-font-weight);
+  font-family: var(--vscode-editor-font-family);
+  color: var(--vscode-foreground);
+  background-color: var(--vscode-sideBar-background);
+}
+
+#sledgehammer-container {
+  font-size: var(--font-size-small);
+  font-family: var(--vscode-editor-font-family);
+  padding: 6px;
+  color: var(--vscode-foreground);
+}
+
+#sledgehammer-container .top-row {
+  display: flex;
+  align-items: center;
+  flex-wrap: wrap;
+  justify-content: flex-end;
+  column-gap: 4px;
+  row-gap: 2px;
+  margin-bottom: 4px;
+}
+
+#sledgehammer-container label {
+  display: flex;
+  align-items: center;
+  gap: 2px;
+  margin: 2px 0;
+}
+
+#sledgehammer-spinner {
+  width: 10px;
+  height: 10px;
+  border: 2px solid rgba(0, 0, 0, 0.2);
+  border-top-color: #000;
+  border-radius: 50%;
+  animation: spin 1s linear infinite;
+  display: none;
+}
+
+#sledgehammer-spinner.loading {
+  display: inline-block;
+}
+
+@keyframes spin {
+  to {
+    transform: rotate(360deg);
+  }
+}
+
+#sledgehammer-container input[type="text"] {
+  font-size: var(--font-size-small);
+  font-family: var(--vscode-editor-font-family);
+  width: 23em;
+  min-height: calc(var(--font-size-base) * 1.4);
+  box-sizing: border-box;
+  margin-right: 4px;
+  color: var(--vscode-input-foreground);
+  background-color: var(--vscode-input-background);
+}
+
+#sledgehammer-container input[type="text"]:focus {
+  outline: 1.5px solid #9dc3e1;
+}
+
+#sledgehammer-container input[type="checkbox"] {
+  margin: 0;
+  transform: translateY(0.5px);
+}
+
+#sledgehammer-container button {
+  font-size: var(--font-size-small);
+  font-family: var(--vscode-editor-font-family);
+  font-weight: normal;
+  border: 0.5px solid #e2e2e2;
+  background-color: var(--vscode-button-secondaryBackground);
+  color: var(--vscode-button-secondaryForeground);
+  cursor: pointer;
+  margin: 2px 0;
+}
+
+#sledgehammer-container button#apply-btn {
+  font-weight: bold;
+  background-color: var(--vscode-button-background);
+  color: var(--vscode-button-foreground);
+}
+
+#sledgehammer-container button:hover {
+  background-color: var(--vscode-button-hoverBackground);
+  border: 0.5px solid #9dc3e1;
+}
+
+#result button {
+  background-color: var(--vscode-button-secondaryBackground);
+  color: var(--vscode-button-secondaryForeground);
+  border: none;
+  font-size: var(--font-size-small);
+  font-family: var(--vscode-editor-font-family);
+  cursor: pointer;
+}
+
+#result button:hover {
+  background-color: var(--vscode-button-hoverBackground);
+  color: var(--vscode-button-foreground);
+}
+
+#sledgehammer-container select {
+  font-size: var(--font-size-small);
+  font-family: var(--vscode-editor-font-family);
+  height: 10px;
+  margin: 2px 0;
+  background-color: var(--vscode-dropdown-background);
+  color: var(--vscode-dropdown-foreground);
+}
+
+#status {
+  font-style: italic;
+  color: var(--vscode-descriptionForeground);
+}
+
+#result div {
+  padding: 2px 4px;
+  border-bottom: 1px solid #ffffff;
+  white-space: pre-wrap;
+  background-color: var(--vscode-editor-inactiveSelectionBackground);
+  color: var(--vscode-foreground);
+  margin-bottom: 1px;
+}
+
+#result .sledge-line {
+  background-color: var(--vscode-editor-inactiveSelectionBackground);
+  border-bottom: 1px solid var(--vscode-panel-border);
+  color: #000;
+  white-space: pre-wrap;
+  padding: 2px 6px;
+  margin-bottom: 1px;
+  border-radius: 2px;
+}
+
+#result .interrupt {
+  background-color: var(--vscode-editorError-background);
+  border-bottom: 1px solid #ffffff;
+  color: var(--vscode-editorError-foreground);
+  white-space: pre-wrap;
+  padding: 2px 6px;
+  margin-bottom: 1px;
+  border-radius: 2px;
+}
+
+#result.error div {
+  background-color: #fdd;
+  color: var(--vscode-editorError-foreground);
+}
+
+#sledgehammer-container .provers-dropdown .history-header {
+  font-family: var(--vscode-editor-font-family);
+  font-size: var(--font-size-small);
+  color: var(--vscode-foreground);
+  background: var(--vscode-dropdown-background);
+  cursor: default;
+  padding: 4px 8px;
+  border-bottom: 1px solid #f4f4f4;
+}
+
+#sledgehammer-container .provers-dropdown .history-header:hover {
+  background: var(--vscode-list-hoverBackground);
+  color: var(--vscode-list-hoverForeground);
+}
+
+#sledgehammer-container .provers-dropdown div {
+  padding: 4px 8px;
+  cursor: pointer;
+  display: flex;
+  align-items: center;
+  justify-content: space-between;
+  border-bottom: 1px solid #f4f4f4;
+  font-size: var(--font-size-small);
+  background: var(--vscode-dropdown-background);
+  color: var(--vscode-dropdown-foreground);
+}
+
+#sledgehammer-container .provers-dropdown div:last-child {
+  border-bottom: none;
+}
+
+#sledgehammer-container .provers-dropdown div:hover {
+  background: #307dc3;
+  color: var(--vscode-list-hoverForeground);
+}
+
+#sledgehammer-container .provers-dropdown .delete-btn {
+  color: var(--vscode-errorForeground);
+  font-size: var(--font-size-small);
+  margin-left: 10px;
+  cursor: pointer;
+  user-select: none;
+  background: none;
+  border: none;
+  padding: 0 2px;
+  outline: none;
+}
+
+#sledgehammer-container .provers-dropdown .delete-btn:hover {
+  background: var(--vscode-list-hoverBackground);
+  border-radius: 2px;
+}
+
+.provers-dropdown {
+  position: absolute;
+  top: 110%;
+  left: 0;
+  width: 99%;
+  min-width: 99%;
+  box-sizing: border-box;
+  background: var(--vscode-dropdown-background);
+  border: 1px solid #e2e2e2;
+  border-top: none;
+  z-index: 20;
+  max-height: 200px;
+  overflow-y: auto;
+  font-family: var(--vscode-editor-font-family);
+  font-size: var(--font-size-small);
+  border-radius: 0 0 2px 2px;
+  display: none;
+}
+
+.provers-input-wrapper {
+  position: relative;
+  display: flex;
+  align-items: center;
+  width: 23em;
+}
+
+#provers {
+  width: 95%;
+  padding-right: 22px;
+}
+
+.provers-dropdown-toggle {
+  position: absolute;
+  right: 3px;
+  top: 38%;
+  transform: translateY(-50%);
+  height: 16px;
+  width: 16px;
+  background: none !important;
+  border: none !important;
+  color: var(--vscode-foreground);
+  font-size: var(--font-size-small);
+  cursor: pointer;
+  z-index: 3;
+  display: flex;
+  align-items: center;
+  justify-content: center;
+  pointer-events: auto;
+  padding: 0;
+}
+
+.provers-dropdown-toggle:hover,
+.provers-dropdown-toggle:focus {
+  color: var(--vscode-textLink-foreground);
+  background: none;
+  border-radius: 0;
+}
+
+
+.provers-dropdown.visible {
+  display: block;
+}
+
+.provers-dropdown .history-header {
+  font-family: var(--vscode-editor-font-family);
+  font-size: var(--font-size-small);
+  color: var(--vscode-dropdown-foreground);
+  background: var(--vscode-dropdown-background);
+  cursor: default;
+  padding: 4px 8px;
+  border-bottom: 1px solid #f4f4f4;
+}
+
+.provers-dropdown div {
+  padding: 4px 8px;
+  cursor: pointer;
+  display: flex;
+}
\ No newline at end of file
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);
+    }
+  };
+})();
diff -r 3de18e94ac7c -r 486e094b676c src/Tools/VSCode/extension/media/symbol-panel.svg
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/VSCode/extension/media/symbol-panel.svg	Thu Oct 23 16:15:40 2025 +0200
@@ -0,0 +1,1 @@
+<svg width="16" height="16" viewBox="0 0 16 16" xmlns="http://www.w3.org/2000/svg" fill="currentColor"><path fill-rule="evenodd" clip-rule="evenodd" d="M7.223 10.933c.326.192.699.29 1.077.282a2.159 2.159 0 0 0 1.754-.842 3.291 3.291 0 0 0 .654-2.113 2.886 2.886 0 0 0-.576-1.877 1.99 1.99 0 0 0-1.634-.733 2.294 2.294 0 0 0-1.523.567V3.475h-.991V11.1h.995v-.344c.076.066.158.125.244.177zM7.85 6.7c.186-.079.388-.113.59-.1a1.08 1.08 0 0 1 .896.428c.257.363.382.802.357 1.245a2.485 2.485 0 0 1-.4 1.484 1.133 1.133 0 0 1-.96.508 1.224 1.224 0 0 1-.976-.417A1.522 1.522 0 0 1 6.975 8.8v-.6a1.722 1.722 0 0 1 .393-1.145c.13-.154.296-.276.482-.355zM3.289 5.675a3.03 3.03 0 0 0-.937.162 2.59 2.59 0 0 0-.8.4l-.1.077v1.2l.423-.359a2.1 2.1 0 0 1 1.366-.572.758.758 0 0 1 .661.282c.15.232.23.503.231.779L2.9 7.825a2.6 2.6 0 0 0-1.378.575 1.65 1.65 0 0 0-.022 2.336 1.737 1.737 0 0 0 1.253.454 1.96 1.96 0 0 0 1.107-.332c.102-.068.197-.145.286-.229v.444h.941V7.715a2.193 2.193 0 0 0-.469-1.5 1.687 1.687 0 0 0-1.329-.54zm.857 3.041c.02.418-.12.829-.391 1.148a1.221 1.221 0 0 1-.955.422.832.832 0 0 1-.608-.2.833.833 0 0 1 0-1.091c.281-.174.6-.277.93-.3l1.02-.148.004.169zm8.313 2.317c.307.13.64.193.973.182.495.012.983-.114 1.41-.365l.123-.075.013-.007V9.615l-.446.32c-.316.224-.696.34-1.084.329A1.3 1.3 0 0 1 12.4 9.8a1.975 1.975 0 0 1-.4-1.312 2.01 2.01 0 0 1 .453-1.381A1.432 1.432 0 0 1 13.6 6.6a1.8 1.8 0 0 1 .971.279l.43.265V5.97l-.17-.073a2.9 2.9 0 0 0-1.17-.247 2.52 2.52 0 0 0-1.929.817 2.9 2.9 0 0 0-.747 2.049c-.028.707.21 1.4.67 1.939.222.249.497.446.804.578z"/></svg>
\ No newline at end of file
diff -r 3de18e94ac7c -r 486e094b676c src/Tools/VSCode/extension/media/symbols.css
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/VSCode/extension/media/symbols.css	Thu Oct 23 16:15:40 2025 +0200
@@ -0,0 +1,229 @@
+:root {
+  --container-paddding: 20px;
+  --input-padding-vertical: 6px;
+  --input-padding-horizontal: 4px;
+  --input-margin-vertical: 4px;
+  --input-margin-horizontal: 0;
+  --input-border-color: var(--vscode-input-border, var(--vscode-panel-border));
+}
+
+--font-size-base: var(--vscode-editor-font-size);
+--font-family-base: var(--vscode-editor-font-family);
+--font-weight-base: var(--vscode-editor-font-weight);
+--font-size-small: calc(var(--font-size-base) * 0.85);
+--font-size-tiny:  calc(var(--font-size-base) * 0.75);
+
+
+body {
+  padding: 0 var(--container-paddding);
+  color: var(--vscode-foreground);
+  font-size: var(--font-size-base);
+  font-weight: var(--font-weight-base);
+  font-family: var(--font-family-base);
+  background-color: var(--vscode-sideBar-background);
+}
+
+pre, code {
+  font-family: var(--font-family-base);
+  font-size: var(--font-size-base);
+}
+
+a {
+  color: var(--vscode-textLink-foreground);
+  text-decoration: none;
+}
+
+a:hover, a:active {
+  color: var(--vscode-textLink-activeForeground);
+}
+
+ol, ul {
+  padding-left: var(--container-paddding);
+}
+
+body > *, form > * {
+  margin-block-start: var(--input-margin-vertical);
+  margin-block-end: var(--input-margin-vertical);
+}
+
+
+.arrow-button, .abbrevs-button, .symbol-button, .reset-button, .control-button {
+  display: inline-flex;
+  align-items: center;
+  justify-content: center;
+  border: 1px solid var(--vscode-panel-border);
+  border-radius: 2px;
+  cursor: pointer;
+  padding: 2px;
+  text-align: center;
+  outline: 1px solid transparent;
+  outline-offset: 2px !important;
+  font-size: var(--font-size-small);
+  font-family: var(--vscode-editor-font-family);
+  color: var(--vscode-button-secondaryForeground);
+  background: var(--vscode-button-secondaryBackground);
+  white-space: nowrap;
+  overflow: hidden;
+  text-overflow: ellipsis;
+  width: auto;
+  height: auto;
+  min-width: 14px;
+  min-height: 14px;
+}
+
+.arrow-button:hover,
+.abbrevs-button:hover,
+.symbol-button:hover,
+.reset-button:hover,
+.control-button:hover {
+  border: 1px solid var(--vscode-focusBorder);
+  background: var(--vscode-button-hoverBackground);
+}
+
+.arrow-button:active, .abbrevs-button:active, .symbol-button:active, .reset-button:active, .control-button:active {
+  background: var(--vscode-button-background);
+  color: var(--vscode-button-foreground);
+}
+
+.tooltip {
+  position: absolute;
+  z-index: 9999;
+  background-color: var(--vscode-editorHoverWidget-background);
+  color: var(--vscode-editorHoverWidget-foreground);
+  padding: 4px 6px;
+  border-radius: 4px;
+  font-size: var(--font-size-small);
+  font-family: var(--font-family-base);
+  white-space: pre-line;
+  pointer-events: none;
+  opacity: 0;
+  transition: opacity 0.1s ease;
+  max-width: 250px;
+  box-shadow: 0 2px 4px var(--vscode-widget-shadow);
+}
+.tooltip.visible { opacity: 1; }
+
+.tabs {
+  display: flex;
+  flex-wrap: wrap;
+  background: var(--vscode-editor-background);
+  border-bottom: 1px solid var(--vscode-panel-border);
+}
+
+.tab {
+  padding: 2px 4px;
+  cursor: pointer;
+  color: var(--vscode-foreground);
+  background: var(--vscode-editor-background);
+  border: none;
+  font-size: var(--font-size-small);
+  font-family: var(--font-family-base);
+}
+.tab.active {
+  border-bottom: 1.5px solid var(--vscode-focusBorder);
+}
+.tab:hover {
+  background: var(--vscode-list-hoverBackground);
+}
+
+.content { padding: 5px; }
+
+.tab-content.hidden { display: none; }
+
+
+.tab-content {
+  display: flex;
+  flex-wrap: wrap;
+  gap: 6px;
+  row-gap: 8px;
+}
+
+.tab-content .symbol-button { margin: 0; }
+
+.tab-content .arrow-button,
+.tab-content .abbrevs-button,
+.tab-content .reset-button,
+.tab-content .control-button { margin: 0; }
+
+input:not([type='checkbox']), textarea {
+  display: block;
+  width: 100%;
+  border: 1px solid var(--input-border-color);
+  font-family: var(--font-family-base);
+  font-size: var(--font-size-base);
+  padding: var(--input-padding-vertical) var(--input-padding-horizontal);
+  color: var(--vscode-input-foreground);
+  background-color: var(--vscode-input-background);
+}
+
+input::placeholder, textarea::placeholder {
+  color: var(--vscode-input-placeholderForeground);
+}
+
+#controls {
+  display: flex;
+  flex-direction: row;
+  justify-content: flex-end;
+  align-items: center;
+}
+#controls > * {
+  margin-left: 5px;
+  margin-top: 5px;
+}
+
+pre {
+  white-space: pre-wrap;
+  word-wrap: break-word;
+}
+
+.search-container {
+  width: 100%;
+  display: flex;
+  flex-direction: column;
+}
+
+.search-input {
+  width: 100%;
+  font-family: var(--font-family-base);
+  font-size: var(--font-size-base);
+  color: var(--vscode-input-foreground);
+  background-color: var(--vscode-input-background);
+  border: 1px solid var(--input-border-colorr);
+  padding: 4px 6px;
+  box-sizing: border-box;
+}
+
+.search-input:hover {
+  border-color: var(--input-border-color);
+}
+
+.search-input::placeholder {
+  animation: blink 1s steps(2, start) infinite;
+}
+
+.search-input:focus {
+  border-color: var(--vscode-focusBorder);
+  outline: none;
+}
+
+.search-results {
+  display: flex;
+  flex-wrap: wrap;
+  gap: 6px;
+  margin-top: 6px;
+}
+
+.search-results .symbol-button {
+  width: auto;
+  height: auto;
+  min-width: 14px;
+  min-height: 14px;
+  padding: 2px 6px;
+  box-sizing: border-box;
+}
+
+
+@keyframes blink {
+  0%, 100% { opacity: 1; }
+  50% { opacity: 0; }
+}
diff -r 3de18e94ac7c -r 486e094b676c src/Tools/VSCode/extension/media/symbols.js
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/VSCode/extension/media/symbols.js	Thu Oct 23 16:15:40 2025 +0200
@@ -0,0 +1,348 @@
+(function () {
+  const vscode = acquireVsCodeApi();
+  let allSymbols = {};
+  let allAbbrevsFromThy = [];
+  let controlSup = "";
+  let controlSub = "";
+
+  function decodeHtmlEntity(code) {
+    try {
+      return String.fromCodePoint(code);
+    } catch (error) {
+      return "?";
+    }
+  }
+
+  function formatGroupName(group) {
+    const groupNameMap = {
+      "Z_Notation": "Z Notation",
+      "Control_Block": "Control Block",
+      "Arrow": "Arrow",
+      "Control": "Control",
+      "Digit": "Digit",
+      "Document": "Document",
+      "Greek": "Greek",
+      "Icon": "Icon",
+      "Letter": "Letter",
+      "Logic": "Logic",
+      "Operator": "Operator",
+      "Punctuation": "Punctuation",
+      "Relation": "Relation",
+      "Unsorted": "Unsorted",
+      "Search": "Search"
+    };
+
+    return groupNameMap[group] || group.replace(/_/g, " ").replace(/\b\w/g, c => c.toUpperCase());
+  }
+
+  function createSearchField() {
+    const searchContainer = document.createElement('div');
+    searchContainer.classList.add('search-container');
+
+    const searchInput = document.createElement('input');
+    searchInput.type = "text";
+    searchInput.classList.add('search-input');
+
+    const searchResults = document.createElement('div');
+    searchResults.classList.add('search-results');
+
+    searchInput.addEventListener('input', () => filterSymbols(searchInput.value, searchResults));
+
+    searchContainer.appendChild(searchInput);
+    searchContainer.appendChild(searchResults);
+    return { searchContainer, searchResults };
+  }
+
+  function filterSymbols(query, resultsContainer) {
+    const normalizedQuery = query.toLowerCase().trim();
+    resultsContainer.innerHTML = '';
+
+    if (normalizedQuery === "") return;
+
+    const matchingSymbols = [];
+    Object.values(allSymbols).forEach(symbolList => {
+      symbolList.forEach(symbol => {
+        if (!symbol.code) return;
+
+        if (
+          symbol.symbol.toLowerCase().includes(normalizedQuery) ||
+          (symbol.abbrevs && symbol.abbrevs.some(abbr => abbr.toLowerCase().includes(normalizedQuery)))
+        ) {
+          matchingSymbols.push(symbol);
+        }
+      });
+    });
+
+    const searchLimit = 50;
+    if (matchingSymbols.length === 0) {
+      resultsContainer.innerHTML = "<p>No symbols found</p>";
+    } else {
+      matchingSymbols.slice(0, searchLimit).forEach(symbol => {
+        const decodedSymbol = decodeHtmlEntity(symbol.code);
+        if (!decodedSymbol) return;
+
+        const button = document.createElement('div');
+        button.classList.add('symbol-button');
+        button.textContent = decodedSymbol;
+        button.setAttribute("data-tooltip", `${symbol.symbol}\nAbbreviations: ${symbol.abbrevs.join(', ')}`);
+
+        button.addEventListener('click', () => {
+          vscode.postMessage({ command: 'insertSymbol', symbol: decodedSymbol });
+        });
+
+        resultsContainer.appendChild(button);
+      });
+
+      if (matchingSymbols.length > searchLimit) {
+        const moreResults = document.createElement('div');
+        moreResults.classList.add('more-results');
+        moreResults.textContent = `(${matchingSymbols.length - searchLimit} more...)`;
+        resultsContainer.appendChild(moreResults);
+      }
+    }
+  }
+
+  function renderWithEffects(symbol) {
+    if (!symbol) return "";
+
+    let result = "";
+    let i = 0;
+    while (i < symbol.length) {
+      const char = symbol[i];
+      if (char === "⇧") {
+        i++;
+        if (i < symbol.length) result += "<sup>" + symbol[i] + "</sup>";
+      } else if (char === "⇩") { 
+        i++;
+        if (i < symbol.length) result += "<sub>" + symbol[i] + "</sub>";
+      } else {
+        result += char;
+      }
+      i++;
+    }
+    return result;
+  }
+
+  function convertSymbolWithEffects(symbol) {
+  let result = "";
+  let i = 0;
+  while (i < symbol.length) {
+    const char = symbol[i];
+    if (char === "⇧") {
+      i++;
+      if (i < symbol.length) {
+        if (controlSup) result += controlSup + symbol[i];
+        else result += symbol[i];
+      }
+    } else if (char === "⇩") {
+      i++;
+      if (i < symbol.length) {
+        if (controlSub) result += controlSub + symbol[i];
+        else result += symbol[i];
+      }
+    } else {
+      result += char;
+    }
+    i++;
+  }
+  return result;
+}
+
+  function sanitizeSymbolForInsert(symbol) {
+    return symbol.replace(/\u0007/g, '');
+  }
+
+  function extractControlSymbols(symbolGroups) {
+    if (!symbolGroups || !symbolGroups["control"]) return;
+    symbolGroups["control"].forEach(symbol => {
+      if (symbol.name === "sup") controlSup = String.fromCodePoint(symbol.code);
+      if (symbol.name === "sub") controlSub = String.fromCodePoint(symbol.code);
+    });
+  }
+
+  function renderSymbols(groupedSymbols, abbrevsFromThy) {
+    const container = document.getElementById('symbols-container');
+    container.innerHTML = '';
+
+    allSymbols = groupedSymbols;
+    allAbbrevsFromThy = abbrevsFromThy || [];
+
+    extractControlSymbols(groupedSymbols);
+
+    vscode.setState({ symbols: groupedSymbols, abbrevs_from_Thy: allAbbrevsFromThy });
+
+    if (!groupedSymbols || Object.keys(groupedSymbols).length === 0) {
+      container.innerHTML = "<p>No symbols available.</p>";
+      return;
+    }
+
+    const tabs = document.createElement('div');
+    tabs.classList.add('tabs');
+
+    const content = document.createElement('div');
+    content.classList.add('content');
+
+    Object.keys(groupedSymbols).forEach((group, index) => {
+      const tab = document.createElement('button');
+      tab.classList.add('tab');
+      tab.textContent = formatGroupName(group);
+      if (index === 0) tab.classList.add('active');
+
+      tab.addEventListener('click', () => {
+        document.querySelectorAll('.tab').forEach(t => t.classList.remove('active'));
+        tab.classList.add('active');
+        document.querySelectorAll('.tab-content').forEach(c => c.classList.add('hidden'));
+        document.getElementById(`content-${group}`).classList.remove('hidden');
+      });
+
+      tabs.appendChild(tab);
+
+      const groupContent = document.createElement('div');
+      groupContent.classList.add('tab-content');
+      groupContent.id = `content-${group}`;
+      if (index !== 0) groupContent.classList.add('hidden');
+
+      if (group === "control") {
+        const resetButton = document.createElement('button');
+        resetButton.classList.add('reset-button');
+        resetButton.textContent = "Reset";
+
+
+        resetButton.addEventListener('click', () => {
+          vscode.postMessage({ command: 'resetControlSymbols' });
+        });
+        groupContent.appendChild(resetButton);
+
+        const controlButtons = ["sup", "sub", "bold"];
+        controlButtons.forEach(action => {
+          const controlSymbol = groupedSymbols[group].find(s => s.name === action);
+          if (controlSymbol) {
+            const decodedSymbol = decodeHtmlEntity(controlSymbol.code);
+            const button = document.createElement('button');
+            button.classList.add('control-button');
+            button.textContent = decodedSymbol;
+            button.title = action.charAt(0).toUpperCase() + action.slice(1);
+            button.addEventListener('click', () => {
+              vscode.postMessage({ command: 'applyControl', action: action });
+            });
+            groupContent.appendChild(button);
+          }
+        });
+      }
+
+      groupedSymbols[group].forEach(symbol => {
+        if (!symbol.code) return;
+        if (["sup", "sub", "bold"].includes(symbol.name)) return;
+        const decodedSymbol = decodeHtmlEntity(symbol.code);
+        if (!decodedSymbol) return;
+
+        const button = document.createElement('div');
+        if (group === "arrow") {
+          button.classList.add('arrow-button'); // Spezielle Klasse für Pfeile
+        } else {
+          button.classList.add('symbol-button');
+        }
+        button.textContent = decodedSymbol;
+        button.setAttribute("data-tooltip", `${symbol.symbol}\nAbbreviations: ${symbol.abbrevs.join(', ')}`);
+
+        button.addEventListener('click', () => {
+          vscode.postMessage({ command: 'insertSymbol', symbol: decodedSymbol });
+        });
+
+        groupContent.appendChild(button);
+      });
+
+      content.appendChild(groupContent);
+    });
+
+    const abbrevsTab = document.createElement('button');
+    abbrevsTab.classList.add('tab');
+    abbrevsTab.textContent = "Abbrevs";
+    abbrevsTab.addEventListener('click', () => {
+      document.querySelectorAll('.tab').forEach(t => t.classList.remove('active'));
+      abbrevsTab.classList.add('active');
+      document.querySelectorAll('.tab-content').forEach(c => c.classList.add('hidden'));
+      document.getElementById("abbrevs-tab-content").classList.remove('hidden');
+    });
+    tabs.appendChild(abbrevsTab);
+
+    const abbrevsContent = document.createElement('div');
+    abbrevsContent.classList.add('tab-content', 'hidden');
+    abbrevsContent.id = "abbrevs-tab-content";
+
+    allAbbrevsFromThy
+      .filter(([abbr, symbol]) => symbol && symbol.trim() !== "" && !/^[a-zA-Z0-9 _-]+$/.test(symbol)) 
+      .forEach(([abbr, symbol]) => {
+        const btn = document.createElement('div');
+        btn.classList.add('abbrevs-button');
+        btn.innerHTML = renderWithEffects(symbol); 
+        btn.title = abbr;
+        btn.addEventListener('click', () => {
+          vscode.postMessage({ command: 'insertSymbol', symbol: convertSymbolWithEffects(sanitizeSymbolForInsert(symbol)) });
+        });
+
+        abbrevsContent.appendChild(btn);
+      });
+
+    content.appendChild(abbrevsContent);
+
+    const searchTab = document.createElement('button');
+    searchTab.classList.add('tab');
+    searchTab.textContent = "Search";
+    searchTab.addEventListener('click', () => {
+      document.querySelectorAll('.tab').forEach(t => t.classList.remove('active'));
+      searchTab.classList.add('active');
+      document.querySelectorAll('.tab-content').forEach(c => c.classList.add('hidden'));
+      document.getElementById("search-tab-content").classList.remove('hidden');
+    });
+    tabs.appendChild(searchTab);
+
+    const { searchContainer, searchResults } = createSearchField();
+    const searchContent = document.createElement('div');
+    searchContent.classList.add('tab-content', 'hidden');
+    searchContent.id = "search-tab-content";
+    searchContent.appendChild(searchContainer);
+
+    content.appendChild(searchContent);
+    container.appendChild(tabs);
+    container.appendChild(content);
+
+    const tooltip = document.createElement("div");
+    tooltip.className = "tooltip";
+    document.body.appendChild(tooltip);
+
+    document.querySelectorAll(".symbol-button, .arrow-button, .abbrevs-button").forEach(button => {
+       button.addEventListener("mouseenter", (e) => {
+       const rect = button.getBoundingClientRect();
+       const text = button.getAttribute("data-tooltip");
+
+       if (text) {
+        tooltip.textContent = text;
+        tooltip.style.left = `${rect.left + window.scrollX}px`;
+        tooltip.style.top = `${rect.bottom + 6 + window.scrollY}px`;
+        tooltip.classList.add("visible");
+       }
+       });
+
+       button.addEventListener("mouseleave", () => {
+       tooltip.classList.remove("visible");
+       tooltip.textContent = "";
+       });
+    });
+
+  }
+
+  window.addEventListener('message', event => {
+    if (event.data.command === 'update' && event.data.symbols) {
+      renderSymbols(event.data.symbols, event.data.abbrevs_from_Thy);
+    }
+  });
+
+  window.onload = function () {
+    const savedState = vscode.getState();
+    if (savedState && savedState.symbols) {
+      renderSymbols(savedState.symbols, savedState.abbrevs_from_Thy);
+    }
+  };
+
+})();
diff -r 3de18e94ac7c -r 486e094b676c src/Tools/VSCode/extension/package.json
--- a/src/Tools/VSCode/extension/package.json	Thu Oct 23 14:49:21 2025 +0200
+++ b/src/Tools/VSCode/extension/package.json	Thu Oct 23 16:15:40 2025 +0200
@@ -33,10 +33,36 @@
                     "id": "isabelle",
                     "title": "Isabelle",
                     "icon": "isabelle.png"
+                },
+                {
+                    "id": "isabelle-symbols",
+                    "title": "Symbols",
+                    "icon": "./media/symbol-panel.svg"
+                },
+                {
+                    "id": "isabelle-sledgehammer",
+                    "title": "Sledgehammer",
+                    "icon": "./media/sledgehammer-panel.svg"
+                }
+            ],
+            "activitybar": [
+                {
+                    "id": "isabelle-documentation",
+                    "title": "Documentation",
+                    "icon":"./media/documentation-panel.svg"
                 }
             ]
         },
         "views": {
+            "isabelle-symbols": [
+                { "id": "isabelle-symbols", "name": "Symbols", "type": "webview", "icon": "./media/symbol-panel.svg" }
+            ],
+            "isabelle-documentation": [
+                { "id": "isabelle-documentation", "name": "Documentation", "type": "webview", "icon": "./media/documentation-panel.svg" }
+            ],
+            "isabelle-sledgehammer": [
+                { "id": "isabelle-sledgehammer", "name": "Sledgehammer", "type": "webview" , "icon": "./media/sledgehammer-panel.svg" }
+            ],
             "isabelle": [
                 {
                     "type": "webview",
@@ -126,6 +152,37 @@
                     "when": "editorLangId == bibtex",
                     "command": "isabelle.preview-split",
                     "group": "navigation"
+                },
+                {
+                    "when": "editorLangId == isabelle",
+                    "command": "isabelle.openSymbolsPanel",
+                    "group": "navigation"
+                },
+                {
+                    "when": "editorLangId == isabelle-ml",
+                    "command": "isabelle.openSymbolsPanel",
+                    "group": "navigation"
+                },
+                {
+                    "when": "editorLangId == isabelle",
+                    "command": "isabelle.openDocumentationPanel",
+                    "group": "navigation"
+                },
+                {
+                    "when": "editorLangId == isabelle-ml",
+                    "command": "isabelle.openDocumentationPanel",
+                    "group": "navigation"
+                },
+                {
+                    "when": "editorLangId == isabelle",
+                    "command": "isabelle.openSledgehammerPanel",
+                    "group": "navigation"
+                },
+                {
+                    "when": "editorLangId == isabelle-ml",
+                    "command": "isabelle.openSledgehammerPanel",
+                    "group": "navigation"
+
                 }
             ],
             "explorer/context": [
@@ -171,12 +228,12 @@
             }
         ],
         "configurationDefaults": {
-          "[isabelle]": {
-            "files.encoding": "utf8isabelle"
-          },
-          "[isabelle-ml]": {
-            "files.encoding": "utf8isabelle"
-          }
+            "[isabelle]": {
+                "files.encoding": "utf8isabelle"
+            },
+            "[isabelle-ml]": {
+                "files.encoding": "utf8isabelle"
+            }
         },
         "grammars": [
             {
diff -r 3de18e94ac7c -r 486e094b676c src/Tools/VSCode/extension/src/documentation_panel.ts
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/VSCode/extension/src/documentation_panel.ts	Thu Oct 23 16:15:40 2025 +0200
@@ -0,0 +1,158 @@
+/*  Author:     Diana Korchmar, LMU Muenchen
+
+Isabelle documentation panel as web view.
+*/
+
+'use strict';
+
+import {
+  WebviewViewProvider, WebviewView, Uri, WebviewViewResolveContext,
+  CancellationToken, window, workspace, Webview, env
+} from 'vscode'
+import { text_colors } from './decorations'
+import * as vscode_lib from './vscode_lib'
+import * as path from 'path'
+import * as lsp from './lsp'
+import { commands } from 'vscode'
+import { LanguageClient } from 'vscode-languageclient/node';
+
+class Documentation_Panel_Provider implements WebviewViewProvider {
+  public static readonly view_type = 'isabelle-documentation';
+
+  private _view?: WebviewView;
+  private _documentationSections: any[] = [];
+  private _initialized = false;
+
+  constructor(
+    private readonly _extension_uri: Uri,
+    private readonly _language_client: LanguageClient
+  ) { }
+
+  request(language_client: LanguageClient) {
+    if (language_client) {
+      this._language_client.sendNotification(lsp.documentation_request_type, { init: true });
+      
+    }
+  }
+
+  setupDocumentation(language_client: LanguageClient) {
+    language_client.onNotification(lsp.documentation_response_type, params => {
+      if (!params || !params.sections || !Array.isArray(params.sections)) {
+        return;
+      }
+      this._documentationSections = params.sections;
+      if (this._view) {
+        this._update_webview();
+      }
+    });
+  }
+
+  public resolveWebviewView(view: WebviewView, context: WebviewViewResolveContext, _token: CancellationToken): void {
+    this._view = view;
+    this._view.webview.options = {
+      enableScripts: true,
+      localResourceRoots: [
+        this._extension_uri
+      ]
+    };
+
+    this._view.webview.html = this._get_html();
+
+    if (Object.keys(this._documentationSections).length > 0) {
+      this._update_webview();
+    }
+
+    this._view.webview.onDidReceiveMessage(async message => {
+      if (message.command === 'openFile') {
+        this._open_document(message.path);
+      }
+    });
+
+    this._initialized = true;
+  }
+
+  private _update_webview(): void {
+    if (!this._view) {
+      return;
+    }
+
+    this._view.webview.postMessage({
+      command: 'update',
+      sections: this._documentationSections,
+    });
+  }
+
+  private _open_document(filePath: string): void {
+    let cleanPath = filePath.replace(/^"+|"+$/g, '').trim();
+
+    const isabelleHome = process.env.ISABELLE_HOME;
+    if (isabelleHome && cleanPath.includes("$ISABELLE_HOME")) {
+      cleanPath = cleanPath.replace("$ISABELLE_HOME", isabelleHome);
+    }
+
+    if (cleanPath.startsWith("/cygdrive/")) {
+      const match = cleanPath.match(/^\/cygdrive\/([a-zA-Z])\/(.*)/);
+      if (match) {
+        const driveLetter = match[1].toUpperCase();
+        const rest = match[2].replace(/\//g, '\\');
+        cleanPath = `${driveLetter}:\\${rest}`;
+      }
+    }
+
+    const uri = Uri.file(cleanPath);
+
+    if (cleanPath.toLowerCase().endsWith(".pdf")) {
+      commands.executeCommand("vscode.open", uri)
+    } else {
+      workspace.openTextDocument(uri).then(document => {
+        window.showTextDocument(document);
+      });
+    }
+  }
+
+
+  private _get_html(): string {
+    return get_webview_html(this._view?.webview, this._extension_uri.fsPath);
+  }
+}
+
+function get_webview_html(webview: Webview | undefined, extension_path: string): string {
+  const script_uri = webview.asWebviewUri(Uri.file(path.join(extension_path, 'media', 'documentation.js')))
+  const css_uri = webview.asWebviewUri(Uri.file(path.join(extension_path, 'media', 'documentation.css')))
+  const font_uri =
+    webview.asWebviewUri(Uri.file(path.join(extension_path, 'fonts', 'IsabelleDejaVuSansMono.ttf')))
+
+  return `
+    <!DOCTYPE html>
+    <html lang="en">
+      <head>
+        <meta charset="UTF-8">
+        <meta name="viewport" content="width=device-width, initial-scale=1.0">
+        <link href="${css_uri}" rel="stylesheet">
+        <style>
+            @font-face {
+                font-family: "Isabelle DejaVu Sans Mono";
+                src: url(${font_uri});
+            }
+            ${_get_decorations()}
+        </style>        
+        <title>Documentation Panel</title>
+      </head>
+      <body>
+        <div id="documentation-container">Loading documentation...</div>
+        <script src="${script_uri}"></script>
+      </body>
+    </html>`;
+}
+
+function _get_decorations(): string {
+  let style: string[] = []
+  for (const key of text_colors) {
+    style.push(`body.vscode-light .${key} { color: ${vscode_lib.get_color(key, true)} }\n`)
+    style.push(`body.vscode-dark .${key} { color: ${vscode_lib.get_color(key, false)} }\n`)
+  }
+  return style.join("")
+}
+
+export { Documentation_Panel_Provider, get_webview_html };
+
diff -r 3de18e94ac7c -r 486e094b676c src/Tools/VSCode/extension/src/extension.ts
--- a/src/Tools/VSCode/extension/src/extension.ts	Thu Oct 23 14:49:21 2025 +0200
+++ b/src/Tools/VSCode/extension/src/extension.ts	Thu Oct 23 16:15:40 2025 +0200
@@ -16,9 +16,12 @@
 import * as lsp from './lsp'
 import * as state_panel from './state_panel'
 import { Uri, TextEditor, ViewColumn, Selection, Position, ExtensionContext, workspace, window,
-  commands, ProgressLocation } from 'vscode'
+  commands, ProgressLocation, Range } from 'vscode'
 import { LanguageClient, LanguageClientOptions, ServerOptions } from 'vscode-languageclient/node'
 import { Output_View_Provider } from './output_view'
+import { Symbols_Panel_Provider } from './symbol_panel'
+import { Documentation_Panel_Provider } from './documentation_panel'
+import { Sledgehammer_Panel_Provider } from './sledgehammer_panel'
 import { register_script_decorations } from './script_decorations'
 
 
@@ -206,6 +209,46 @@
         params => provider.update_content(params.content))
     })
 
+    const documentation_provider = new Documentation_Panel_Provider(context.extensionUri, language_client);
+    context.subscriptions.push(window.registerWebviewViewProvider(Documentation_Panel_Provider.view_type, documentation_provider));
+
+    language_client.onReady().then(() => {
+      documentation_provider.request(language_client);
+      documentation_provider.setupDocumentation(language_client);
+    });
+    
+    const symbols_provider = new Symbols_Panel_Provider(context.extensionUri, language_client);
+    context.subscriptions.push(
+      window.registerWebviewViewProvider(Symbols_Panel_Provider.view_type, symbols_provider)
+    );
+    language_client.onReady().then(() => symbols_provider.request(language_client));
+    language_client.onReady().then(() => symbols_provider.setup(language_client));
+
+
+    const sledgehammer_provider = new Sledgehammer_Panel_Provider(context.extensionUri, language_client);
+    context.subscriptions.push(
+      window.registerWebviewViewProvider(Sledgehammer_Panel_Provider.view_type, sledgehammer_provider)
+    );
+    language_client.onReady().then(() => sledgehammer_provider.request_provers(language_client))
+
+    language_client.onReady().then(() => {
+      language_client.onNotification(lsp.sledgehammer_status_type, msg =>
+        sledgehammer_provider.updateStatus(msg.message))
+      language_client.onNotification(lsp.sledgehammer_apply_response_type, msg =>
+        sledgehammer_provider.updateResult(msg))
+      language_client.onNotification(lsp.sledgehammer_no_such_prover_type, msg =>
+        sledgehammer_provider.updateNoProver(msg))
+      language_client.onNotification(lsp.sledgehammer_insert_position_response_type, msg =>
+        sledgehammer_provider.insert(msg.position))
+      language_client.onNotification(lsp.sledgehammer_locate_response_type, msg =>
+        sledgehammer_provider.locate(msg.position))
+      language_client.onNotification(lsp.sledgehammer_provers_response, msg => {
+        sledgehammer_provider.update_provers(msg.provers, msg.history)
+      })
+      language_client.onNotification(lsp.sledgehammer_no_proof_context_type, () =>
+        sledgehammer_provider.updateNoProofContext());
+    })
+
 
     /* state panel */
 
diff -r 3de18e94ac7c -r 486e094b676c src/Tools/VSCode/extension/src/lsp.ts
--- a/src/Tools/VSCode/extension/src/lsp.ts	Thu Oct 23 14:49:21 2025 +0200
+++ b/src/Tools/VSCode/extension/src/lsp.ts	Thu Oct 23 16:15:40 2025 +0200
@@ -129,6 +129,136 @@
   content: string
 }
 
+export interface Symbol_Entry {
+  name: string;
+  abbrevs: string[];
+  groups: string[];
+  code?: number; 
+  font?: string; 
+  symbol: string;
+  argument: string;
+  decoded: string;
+}
+
+export interface Symbols_Response {
+  symbols: Symbol_Entry [];
+  abbrevs_from_Thy: [string, string][];
+}
+
+export const symbols_response_type =
+    new NotificationType<Symbols_Response>('PIDE/symbols_response');
+
+export interface InitRequest {
+  init: boolean;
+}
+
+export const symbols_request_type =
+    new NotificationType<InitRequest>("PIDE/symbols_panel_request")
+
+
+export const documentation_request_type =
+  new NotificationType<InitRequest>("PIDE/documentation_request")
+
+export interface Documentation_Response {
+  sections: Array<{
+    title: string;
+    important: boolean;
+    entries: Array<{ title: string; path: string }>;
+  }>;
+}
+
+export const documentation_response_type =
+  new NotificationType<Documentation_Response>("PIDE/documentation_response");
+
+export interface SledgehammerApplyRequest {
+  provers: string;
+  isar: boolean;
+  try0: boolean;
+  purpose: number;
+}
+
+export interface SledgehammerStatus {
+  message: string;
+}
+
+export interface SledgehammerApplyResult {
+  content: string;
+  position: {
+    uri: string;
+    line: number;
+    character: number;
+  };
+  sendbackId: number;
+  state_location: {
+    uri: string;
+    line: number;
+    character: number;
+  };
+}
+
+export interface SledgehammerLocate {
+  position: {
+    uri: string;
+    line: number;
+    character: number;
+  };
+}
+
+export interface SledgehammerInsertPosition {
+  position: {
+    uri: string;
+    line: number;
+    character: number;
+  };
+}
+
+export interface Sledgehammer_Provers {
+  provers: string;
+  history: string[];
+}
+
+export interface Sledgehammer_Provers_Delete {
+  entry: string;
+}
+
+export interface SledgehammerNoSuchProver {
+  provers: string[];
+}
+
+export const sledgehammer_request_type =
+  new NotificationType<SledgehammerApplyRequest>('PIDE/sledgehammer_request');
+
+export const sledgehammer_provers_delete =
+  new NotificationType<Sledgehammer_Provers_Delete>('PIDE/sledgehammer_deleteProvers_request');
+
+export const sledgehammer_cancel_type =
+  new NotificationType<void>('PIDE/sledgehammer_cancel_request');
+
+export const sledgehammer_provers =
+  new NotificationType<InitRequest>('PIDE/sledgehammer_provers_request');
+ 
+export const sledgehammer_provers_response =
+  new NotificationType<Sledgehammer_Provers>('PIDE/sledgehammer_provers_response');
+
+export const sledgehammer_no_such_prover_type =
+  new NotificationType<SledgehammerNoSuchProver>('PIDE/sledgehammer_noProver_response');
+
+export const sledgehammer_status_type =
+  new NotificationType<SledgehammerStatus>('PIDE/sledgehammer_status_response');
+
+export const sledgehammer_apply_response_type =
+  new NotificationType<SledgehammerApplyResult>('PIDE/sledgehammer_apply_response');
+
+export const sledgehammer_locate_response_type =
+  new NotificationType<SledgehammerLocate>('PIDE/sledgehammer_locate_response');
+
+export const sledgehammer_insert_position_response_type =
+  new NotificationType<SledgehammerInsertPosition>('PIDE/sledgehammer_insert_position_response');
+
+export const sledgehammer_no_proof_context_type =
+  new NotificationType<void>('PIDE/sledgehammer_no_proof_context');
+
+
 export const preview_request_type =
   new NotificationType<Preview_Request>("PIDE/preview_request")
 
diff -r 3de18e94ac7c -r 486e094b676c src/Tools/VSCode/extension/src/sledgehammer_panel.ts
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/VSCode/extension/src/sledgehammer_panel.ts	Thu Oct 23 16:15:40 2025 +0200
@@ -0,0 +1,218 @@
+/*  Author:     Diana Korchmar, LMU Muenchen
+
+Isabelle sledgehammer panel as web view.
+*/
+
+import { WebviewViewProvider, WebviewView, Uri, WebviewViewResolveContext, CancellationToken, window, Webview, Selection, Range, TextDocument, TextDocumentContentChangeEvent } from 'vscode';
+import * as path from 'path';
+import { text_colors } from './decorations';
+import * as vscode_lib from './vscode_lib'
+import * as lsp from './lsp';
+import { LanguageClient } from 'vscode-languageclient/node';
+import { Position } from 'vscode';
+
+
+class Sledgehammer_Panel_Provider implements WebviewViewProvider {
+  public static readonly view_type = 'isabelle-sledgehammer';
+  private _view?: WebviewView;
+  private _lastResultPosition?: { uri: string; line: number; character: number; lineText: string };
+  private text_to_insert: string;
+
+  constructor(
+    private readonly _extension_uri: Uri,
+    private readonly _language_client: LanguageClient
+  ) { }
+
+  public resolveWebviewView(view: WebviewView, context: WebviewViewResolveContext, _token: CancellationToken): void {
+    this._view = view;
+    this._view.webview.options = {
+      enableScripts: true,
+      localResourceRoots: [this._extension_uri]
+    };
+    this._view.webview.html = this._get_html();
+    this._setup_message_handler();
+  }
+
+  request_provers(language_client: LanguageClient) {
+    if (language_client) {
+      this._language_client.sendNotification(lsp.sledgehammer_provers, { init: true });
+    }
+  }
+
+  private _setup_message_handler(): void {
+    if (!this._view) return;
+    this._view.webview.onDidReceiveMessage(async message => {
+      const editor = window.activeTextEditor;
+      const pos = editor?.selection.active;
+
+      if (editor && pos) {
+        this._language_client.sendNotification(lsp.caret_update_type, {
+          uri: editor.document.uri.toString(),
+          line: pos.line,
+          character: pos.character
+        });
+      }
+      switch (message.command) {
+        case 'apply':
+          this._language_client.sendNotification(lsp.sledgehammer_request_type, {
+            provers: message.provers,
+            isar: message.isar,
+            try0: message.try0,
+            purpose: 1
+          });
+
+          break;
+        case 'cancel':
+          this._language_client.sendNotification(lsp.sledgehammer_cancel_type);
+          break;
+        case 'locate':
+          this._language_client.sendNotification(lsp.sledgehammer_request_type, {
+            provers: message.provers,
+            isar: message.isar,
+            try0: message.try0,
+            purpose: 2
+          });
+          break;
+
+        case 'insert_text':
+          this._language_client.sendNotification(lsp.sledgehammer_request_type, {
+            provers: message.provers,
+            isar: message.isar,
+            try0: message.try0,
+            purpose: 3
+          });
+          this.text_to_insert = message.text;
+          break;
+
+        case 'delete_prover_history':
+          this._language_client.sendNotification(lsp.sledgehammer_provers_delete, {
+            entry: message.entry
+          });
+          break;
+
+      }
+    });
+  }
+
+  public updateStatus(message: string): void {
+    if (this._view) {
+      this._view.webview.postMessage({ command: 'status', message });
+    }
+  }
+
+  public update_provers(provers: string, history: string[]): void {
+    if (this._view) {
+      this._view.webview.postMessage({ command: 'provers', provers, history });
+    }
+  }
+
+  public locate(state_location: { uri: string; line: number; character: number }): void {
+    const docUri = Uri.parse(state_location.uri);
+    const editor = window.activeTextEditor;
+
+    if (editor && editor.document.uri.toString() === docUri.toString()) {
+      const position = new Position(state_location.line, state_location.character);
+      editor.selections = [new Selection(position, position)];
+      editor.revealRange(new Range(position, position));
+    } 
+  }
+
+  public insert(position: { uri: string; line: number; character: number }): void {
+    const editor = window.activeTextEditor;
+    if (!editor) return;
+
+    const uri = Uri.parse(position.uri);
+    if (editor.document.uri.toString() !== uri.toString()) return;
+
+    const pos = new Position(position.line, position.character);
+    const existingLineText = editor.document.lineAt(pos.line).text;
+    const textToInsert = existingLineText.trim() === '' ? this.text_to_insert : '\n' + this.text_to_insert;
+
+    editor.edit(editBuilder => {
+      editBuilder.insert(pos, textToInsert);
+    });
+  }
+
+
+  public updateResult(result: lsp.SledgehammerApplyResult): void {
+    const editor = window.activeTextEditor;
+    const lineText = editor?.document.lineAt(result.position.line).text ?? "";
+    this._lastResultPosition = {
+      ...result.position,
+      lineText
+    };
+
+    if (this._view) {
+        this._view.webview.postMessage({
+          command: 'result',
+          content: result.content,
+          position: result.position,
+          sendbackId: result.sendbackId
+        });
+      
+    }
+  }
+
+  public updateNoProver(provers: lsp.SledgehammerNoSuchProver): void {
+    if (this._view) {
+      this._view.webview.postMessage({ command: 'no_provers' });
+    }
+  }
+
+
+  public updateNoProofContext(): void {
+    if (this._view) {
+      this._view.webview.postMessage({ command: 'no_proof_context' });
+    }
+  }
+
+  private _get_html(): string {
+    return get_webview_html(this._view?.webview, this._extension_uri.fsPath);
+  }
+}
+
+function get_webview_html(webview: Webview | undefined, extension_path: string): string {
+  const script_uri = webview?.asWebviewUri(Uri.file(path.join(extension_path, 'media', 'sledgehammer.js')));
+  const css_uri = webview?.asWebviewUri(Uri.file(path.join(extension_path, 'media', 'sledgehammer.css')));
+  const font_uri =
+    webview.asWebviewUri(Uri.file(path.join(extension_path, 'fonts', 'IsabelleDejaVuSansMono.ttf')))
+
+
+  return `
+    <!DOCTYPE html>
+    <html lang="en">
+      <head>
+        <meta charset="UTF-8">
+        <meta name="viewport" content="width=device-width, initial-scale=1.0">
+        <link href="${css_uri}" rel="stylesheet">
+        <style>
+            @font-face {
+                font-family: "Isabelle DejaVu Sans Mono";
+                src: url(${font_uri});
+            }
+            ${_get_decorations()}
+        </style>        
+        <title>Sledgehammer Panel</title>
+      </head>
+      <body>
+        <script src="${script_uri}"></script>
+      </body>
+    </html>`;
+}
+
+function _get_decorations(): string {
+  let style: string[] = []
+  for (const key of text_colors) {
+    style.push(`body.vscode-light .${key} { color: ${vscode_lib.get_color(key, true)} }\n`)
+    style.push(`body.vscode-dark .${key} { color: ${vscode_lib.get_color(key, false)} }\n`)
+  }
+  return style.join("")
+}
+
+export { Sledgehammer_Panel_Provider, get_webview_html };
+
+export interface PositionInfo {
+  uri: string;
+  line: number;
+  character: number;
+}
diff -r 3de18e94ac7c -r 486e094b676c src/Tools/VSCode/extension/src/symbol_panel.ts
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/VSCode/extension/src/symbol_panel.ts	Thu Oct 23 16:15:40 2025 +0200
@@ -0,0 +1,275 @@
+/*  Author:     Diana Korchmar, LMU Muenchen
+
+Isabelle symbols panel as web view.
+*/
+
+'use strict';
+
+import {
+  WebviewViewProvider, WebviewView, Uri, WebviewViewResolveContext,
+  CancellationToken, window, Position, Selection, Webview
+} from 'vscode'
+import { text_colors } from './decorations'
+import * as vscode_lib from './vscode_lib'
+import * as path from 'path'
+import * as lsp from './lsp'
+import { LanguageClient } from 'vscode-languageclient/node';
+import * as fs from 'fs';
+
+class Symbols_Panel_Provider implements WebviewViewProvider {
+  public static readonly view_type = 'isabelle-symbols'
+
+  private _view?: WebviewView
+  private _groupedSymbols: { [key: string]: lsp.Symbol_Entry[] } = {}
+  private _initialized = false;
+  private _abbrevsFromThy: [string, string][] = [];
+
+  constructor(
+    private readonly _extension_uri: Uri,
+    private readonly _language_client: LanguageClient
+  ) { }
+
+  request( language_client: LanguageClient) {
+    if (language_client) {
+      this._language_client.sendNotification(lsp.symbols_request_type, { init: true });
+    }
+  }
+
+  setup(language_client: LanguageClient) {
+    language_client.onNotification(lsp.symbols_response_type, params => {
+      if (!params?.symbols || !Array.isArray(params.symbols)) {
+        return;
+
+      }
+
+      this._groupedSymbols = this._group_symbols(params.symbols);
+      this._abbrevsFromThy = params.abbrevs_from_Thy ?? [];
+      if (this._view) {
+        this._update_webview();
+      }
+    });
+  }
+
+  public resolveWebviewView(
+    view: WebviewView,
+    context: WebviewViewResolveContext,
+    _token: CancellationToken) {
+    this._view = view
+
+    view.webview.options = {
+      enableScripts: true,
+
+      localResourceRoots: [
+        this._extension_uri
+      ]
+    }
+
+    view.webview.html = this._get_html()
+
+    if (Object.keys(this._groupedSymbols).length > 0) {
+      this._update_webview();
+    }
+
+    this._view.webview.onDidReceiveMessage(message => {
+      if (message.command === 'insertSymbol') {
+        this._insert_symbol(message.symbol);
+      } else if (message.command === 'resetControlSymbols') {
+        this._reset_control_symbols();
+      } else if (message.command === 'applyControl') {
+        this._apply_control_effect(message.action);
+      }
+    });
+
+
+    this._initialized = true;
+  }
+
+  private _apply_control_effect(action: string): void {
+    const editor = window.activeTextEditor;
+    if (!editor) return;
+
+    const document = editor.document;
+    const selection = editor.selection;
+    let selectedText = document.getText(selection);
+
+    if (!selectedText.trim() && !selection.isEmpty) return;
+
+    const controlGroup = this._groupedSymbols["control"];
+    if (!controlGroup) return;
+
+    const controlSymbols: { [key: string]: string } = {};
+    controlGroup.forEach(symbol => {
+      if (symbol.name === "sup" || symbol.name === "sub" || symbol.name === "bold") {
+        controlSymbols[symbol.name] = String.fromCodePoint(symbol.code);
+      }
+    });
+
+    if (!controlSymbols[action]) return;
+    const controlSymbol = controlSymbols[action];
+    const allControlSymbols = Object.values(controlSymbols);
+
+
+    editor.edit(editBuilder => {
+      if (!selection.isEmpty) {
+        if (action === "bold") {
+          editor.setDecorations(this.boldDecoration, [{ range: selection }]);
+        } else {
+          let newText = selectedText
+            .split("")
+            .map((char, index, arr) => {
+              const prevChar = index > 0 ? arr[index - 1] : null;
+              if (char.trim() === "") return char;
+              if (allControlSymbols.includes(char)) return "";
+
+              return `${controlSymbol}${char}`;
+            })
+            .join("");
+
+          editBuilder.replace(selection, newText);
+        }
+      } else {
+        editBuilder.insert(selection.active, controlSymbol);
+      }
+    }).then(success => {
+      if (!success) {
+        window.showErrorMessage("Failed to apply control effect.");
+      }
+    });
+  }
+
+  private _insert_symbol(symbol: string): void {
+    const editor = window.activeTextEditor;
+    if (editor) {
+      editor.edit(editBuilder => {
+        editBuilder.insert(editor.selection.active, symbol);
+      });
+    }
+  }
+
+  private boldDecoration = window.createTextEditorDecorationType({
+    fontWeight: "bold",
+    textDecoration: "none"
+  });
+
+  private _reset_control_symbols(): void {
+    const editor = window.activeTextEditor;
+    if (!editor) {
+      return;
+    }
+
+    const document = editor.document;
+    const selection = editor.selection;
+    let selectedText = document.getText(selection);
+
+    if (!selectedText.trim() && !selection.isEmpty) return;
+
+    const controlGroup = this._groupedSymbols["control"];
+    if (!controlGroup) return;
+
+
+    const controlSymbols: { [key: string]: string } = {};
+    controlGroup.forEach(symbol => {
+      if (symbol.name === "sup" || symbol.name === "sub" || symbol.name === "bold") {
+        controlSymbols[String.fromCodePoint(symbol.code)] = symbol.name;
+      }
+    });
+
+    const allControlSymbols = Object.keys(controlSymbols);
+
+    editor.edit(editBuilder => {
+      if (!selection.isEmpty) {
+        if (this.boldDecoration) {
+          editor.setDecorations(this.boldDecoration, []);
+        }
+
+        let newText = selectedText
+          .split("")
+          .map(char => (allControlSymbols.includes(char) ? "" : char))
+          .join("");
+
+        editBuilder.replace(selection, newText);
+      }
+    }).then(success => {
+      if (!success) {
+      }
+    });
+  }
+
+  private _update_webview(): void {
+    this._view.webview.postMessage({
+      command: 'update',
+      symbols: this._groupedSymbols,
+      abbrevs_from_Thy: this._abbrevsFromThy,
+    });
+  }
+
+  private _group_symbols(symbols: lsp.Symbol_Entry[]): { [key: string]: lsp.Symbol_Entry[] } {
+    const groupedSymbols: { [key: string]: lsp.Symbol_Entry[] } = {};
+    symbols.forEach(symbol => {
+      if (!symbol.groups || !Array.isArray(symbol.groups)) {
+        return;
+      }
+
+      symbol.groups.forEach(group => {
+        if (!groupedSymbols[group]) {
+          groupedSymbols[group] = [];
+        }
+        groupedSymbols[group].push(symbol);
+      });
+    });
+    return groupedSymbols;
+  }
+
+  private _get_html(): string {
+    return get_webview_html(this._view.webview, this._extension_uri.fsPath)
+  }
+}
+
+function open_webview_link(link: string) {
+  const uri = Uri.parse(link)
+  const line = Number(uri.fragment) || 0
+  const pos = new Position(line, 0)
+  window.showTextDocument(uri.with({ fragment: '' }), {
+    preserveFocus: false,
+    selection: new Selection(pos, pos)
+  })
+}
+
+function get_webview_html(webview: Webview, extension_path: string): string {
+  const script_uri = webview.asWebviewUri(Uri.file(path.join(extension_path, 'media', 'symbols.js')))
+  const css_uri = webview.asWebviewUri(Uri.file(path.join(extension_path, 'media', 'symbols.css')))
+  const font_uri =
+    webview.asWebviewUri(Uri.file(path.join(extension_path, 'fonts', 'IsabelleDejaVuSansMono.ttf')))
+
+  return `<!DOCTYPE html>
+    <html lang='en'>
+      <head>
+        <meta charset='UTF-8'>
+        <meta name='viewport' content='width=device-width, initial-scale=1.0'>
+        <link href='${css_uri}' rel='stylesheet' type='text/css'>
+        <style>
+            @font-face {
+                font-family: "Isabelle DejaVu Sans Mono";
+                src: url(${font_uri});
+            }
+            ${_get_decorations()}
+        </style>
+        <title>Symbols Panel</title>
+      </head>
+      <body>
+        <div id="symbols-container"></div>
+        <script src='${script_uri}'></script>
+      </body>
+    </html>`
+}
+
+function _get_decorations(): string {
+  let style: string[] = []
+  for (const key of text_colors) {
+    style.push(`body.vscode-light .${key} { color: ${vscode_lib.get_color(key, true)} }\n`)
+    style.push(`body.vscode-dark .${key} { color: ${vscode_lib.get_color(key, false)} }\n`)
+  }
+  return style.join("")
+}
+
+export { Symbols_Panel_Provider, get_webview_html, open_webview_link }
diff -r 3de18e94ac7c -r 486e094b676c src/Tools/VSCode/src/language_server.scala
--- a/src/Tools/VSCode/src/language_server.scala	Thu Oct 23 14:49:21 2025 +0200
+++ b/src/Tools/VSCode/src/language_server.scala	Thu Oct 23 16:15:40 2025 +0200
@@ -14,7 +14,7 @@
 import isabelle._
 
 import java.io.{PrintStream, OutputStream, File => JFile}
-
+import isabelle.vscode.Sledgehammer_Panel
 import scala.annotation.tailrec
 
 
@@ -117,6 +117,7 @@
   private val session_ = Synchronized(None: Option[VSCode_Session])
   def session: VSCode_Session = session_.value getOrElse error("Server inactive")
   def resources: VSCode_Resources = session.resources
+  private val sledgehammer_panel = Sledgehammer_Panel(this)
 
   def rendering_offset(node_pos: Line.Node_Position): Option[(VSCode_Rendering, Text.Offset)] =
     for {
@@ -296,6 +297,7 @@
       session.syslog_messages += syslog_messages
 
       dynamic_output.init()
+      sledgehammer_panel.init()
 
       try {
         Isabelle_Process.start(
@@ -324,6 +326,7 @@
         delay_output.revoke()
         delay_caret_update.revoke()
         delay_preview.revoke()
+        sledgehammer_panel.exit()
 
         val result = session.stop()
         if (result.ok) reply("")
@@ -487,6 +490,20 @@
     channel.write(LSP.Symbols_Convert_Request.reply(id, converted))
   }
 
+  def symbols_panel_request(init: Boolean): Unit = {
+    val abbrevs =
+      resources.get_caret().flatMap { caret =>
+        resources.get_model(caret.file).map(_.syntax().abbrevs)
+      }.getOrElse(session.resources.session_base.overall_syntax.abbrevs)
+
+    channel.write(LSP.Symbols_Response(Symbol.symbols, abbrevs))
+  }
+
+
+  def documentation_request(init: Boolean): Unit = {
+    channel.write(LSP.Documentation_Response())
+  }
+
 
   /* main loop */
 
@@ -530,6 +547,12 @@
           case LSP.Symbols_Convert_Request(id, text, boolean) =>
             symbols_convert_request(id, text, boolean)
           case LSP.Preview_Request(file, column) => preview_request(file, column)
+          case LSP.Symbols_Panel_Request(init) => symbols_panel_request(init)
+          case LSP.Documentation_Request(init) => documentation_request(init)
+          case LSP.Sledgehammer_Request(provers, isar, try0, purpose) => sledgehammer_panel.handle_request(provers, isar, try0, purpose)
+          case LSP.Sledgehammer_Cancel => sledgehammer_panel.cancel_query()
+          case LSP.Sledgehammer_Provers(init) => sledgehammer_panel.send_provers_and_history(init)
+          case LSP.Sledgehammer_Delete_Prover(entry) => sledgehammer_panel.handle_sledgehammer_delete(entry)
           case _ => if (!LSP.ResponseMessage.is_empty(json)) log("### IGNORED")
         }
       }
diff -r 3de18e94ac7c -r 486e094b676c src/Tools/VSCode/src/lsp.scala
--- a/src/Tools/VSCode/src/lsp.scala	Thu Oct 23 14:49:21 2025 +0200
+++ b/src/Tools/VSCode/src/lsp.scala	Thu Oct 23 16:15:40 2025 +0200
@@ -737,4 +737,152 @@
           "label" -> label,
           "content" -> content))
   }
+
+  object Symbols_Panel_Request {
+    def unapply(json: JSON.T): Option[(Boolean)] =
+      json match {
+        case Notification("PIDE/symbols_panel_request", Some(params)) =>
+          for {
+            init <- JSON.bool(params, "init")
+          } yield (init)
+        case _ => None
+      }
+  }
+
+  object Documentation_Request {
+    def unapply(json: JSON.T): Option[(Boolean)] =
+      json match {
+        case Notification("PIDE/documentation_request", Some(params)) =>
+          for {
+            init <- JSON.bool(params, "init")
+          } yield (init)
+        case _ => None
+      }
+  }
+
+
+  object Sledgehammer_Provers {
+    def unapply(json: JSON.T): Option[(Boolean)] =
+      json match {
+        case Notification("PIDE/documentation_request", Some(params)) =>
+          for {
+            init <- JSON.bool(params, "init")
+          } yield (init)
+        case _ => None
+      }
+  }
+
+
+  object Symbols_Response {
+    def apply(symbols: Symbol.Symbols, abbrevs: List[(String, String)]): JSON.T = {
+      def json(symbol: Symbol.Entry): JSON.T = {
+        val decoded = Symbol.decode(symbol.symbol)
+
+        JSON.Object(
+          "symbol" -> symbol.symbol,
+          "name" -> symbol.name,
+          "argument" -> symbol.argument.toString,
+          "decoded" -> decoded
+        ) ++
+          JSON.optional("code", symbol.code) ++
+          JSON.optional("font", symbol.font) ++
+          JSON.Object(
+            "groups" -> symbol.groups,
+            "abbrevs" -> symbol.abbrevs
+          )
+      }
+
+
+      Notification("PIDE/symbols_response", JSON.Object("symbols" -> symbols.entries.map(json), "abbrevs_from_Thy" -> abbrevs.map { case (a, b) => List(a, b) }
+      ))
+    }
+  }
+
+
+  object Documentation_Response {
+    def apply(): JSON.T = {
+      val ml_settings = ML_Settings.init()
+      val doc_contents = Doc.contents(ml_settings)
+      val json_sections = doc_contents.sections.map { section =>
+        JSON.Object(
+          "title" -> section.title,
+          "important" -> section.important,
+          "entries" -> section.entries.map { entry =>
+            JSON.Object("title" -> entry.title, "path" -> entry.path.toString)
+          }
+        )
+      }
+
+      Notification("PIDE/documentation_response", JSON.Object("sections" -> json_sections))
+    }
+  }
+
+  object Sledgehammer_Request {
+    def unapply(json: JSON.T): Option[(String, Boolean, Boolean, Int)] =
+      json match {
+        case Notification("PIDE/sledgehammer_request", Some(params)) =>
+          for {
+            provers <- JSON.string(params, "provers")
+            isar <- JSON.bool(params, "isar")
+            try0 <- JSON.bool(params, "try0")
+            purpose <- JSON.int(params, "purpose") orElse Some(1)  // fallback default
+          } yield (provers, isar, try0, purpose)
+        case _ => None
+      }
+  }
+
+  object Sledgehammer_Delete_Prover {
+    def unapply(json: JSON.T): Option[String] =
+      json match {
+        case Notification("PIDE/sledgehammer_deleteProvers_request", Some(params)) =>
+          JSON.string(params, "entry")
+        case _ => None
+      }
+  }
+
+  object Sledgehammer_Cancel extends Notification0("PIDE/sledgehammer_cancel_request")
+
+  object Sledgehammer_Provers_Response {
+    def apply(provers: String, history: List[String]): JSON.T = {
+      Notification(
+        "PIDE/sledgehammer_provers_response",
+        JSON.Object("provers" -> provers, "history" -> history)
+      )
+    }
+  }
+
+  object Sledgehammer_NoProver_Response {
+    def apply(provers: List[String]): JSON.T =
+      Notification("PIDE/sledgehammer_noProver_response", JSON.Object("provers" -> provers))
+  }
+
+  object Sledgehammer_Status_Response {
+    def apply(message: String): JSON.T =
+      Notification("PIDE/sledgehammer_status_response", JSON.Object("message" -> message))
+  }
+
+  object Sledgehammer_Apply_Response {
+    def apply(resultJson: JSON.Object.T): JSON.T = {
+      Notification("PIDE/sledgehammer_apply_response", resultJson)
+    }
+  }
+
+  object Sledgehammer_Locate_Response {
+    def apply(resultJson: JSON.Object.T): JSON.T = {
+      Notification("PIDE/sledgehammer_locate_response", resultJson)
+    }
+  }
+
+  object Sledgehammer_InsertPosition_Response {
+    def apply(resultJson: JSON.Object.T): JSON.T = {
+      Notification("PIDE/sledgehammer_insert_position_response", resultJson)
+    }
+  }
+
+  object Sledgehammer_NoProof_Response{
+    def apply(): JSON.T =
+      Notification("PIDE/sledgehammer_no_proof_context", None)
+  }
+
 }
+
diff -r 3de18e94ac7c -r 486e094b676c src/Tools/VSCode/src/sledgehammer_panel.scala
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/VSCode/src/sledgehammer_panel.scala	Thu Oct 23 16:15:40 2025 +0200
@@ -0,0 +1,242 @@
+/*  Title:      Tools/VSCode/src/sledgehammer_panel.scala
+    Author:     Diana Korchmar
+*/
+
+package isabelle.vscode
+
+
+import isabelle._
+
+import java.io.{PrintStream, PrintWriter, FileWriter, OutputStream, File => JFile}
+
+object Sledgehammer_Panel {
+  def apply(server: Language_Server): Sledgehammer_Panel =
+    new Sledgehammer_Panel(server)
+}
+
+class Sledgehammer_Panel private(server: Language_Server) {
+  private val query_operation =
+    new Query_Operation(server.editor, (), "sledgehammer", consume_status, consume_result)
+  var current_purpose: Int = 1
+  private var last_sendback_id: Option[Int] = None
+
+  private val provers_history_option: String = "sledgehammer_provers_history"
+  private val provers_history_delim: Char = '|'
+
+  private var persistent_options: Options = Options.init()
+
+  private def get_provers_history(): List[String] =
+    Library.space_explode(provers_history_delim, persistent_options.string(provers_history_option)).filterNot(_.isEmpty)
+
+  private def set_provers_history(new_history: String): Unit = {
+    persistent_options = persistent_options.string.update(provers_history_option, new_history)
+    persistent_options.save_prefs()
+  }
+
+  def send_provers_and_history(init: Boolean): Unit = {
+    val provers = persistent_options.check_name("sledgehammer_provers").value
+    val history = get_provers_history()
+    server.channel.write(LSP.Sledgehammer_Provers_Response.apply(provers, history))
+  }
+
+  def add_provers_history(entry: String): Unit = {
+    val current = get_provers_history()
+    val history = (entry :: current.filter(_ != entry)).take(10)
+    val history_str = history.mkString(provers_history_delim.toString)
+    set_provers_history(history_str)
+  }
+
+  def handle_request(provers: String, isar: Boolean, try0: Boolean, purpose: Int): Unit = {
+    val available_provers = persistent_options.string("sledgehammer_provers").split("\\s+").toSet
+    val user_provers = provers.trim.split("\\s+").toSet
+    val invalid = user_provers.diff(available_provers)
+    if (invalid.nonEmpty) {
+      server.channel.write(LSP.Sledgehammer_NoProver_Response.apply(invalid.toList))
+      return
+    }
+    choose_purpose(List(provers, isar.toString, try0.toString), purpose)
+    add_provers_history(provers)
+  }
+
+  def handle_sledgehammer_delete(entry: String): Unit = {
+    val history = get_provers_history().filter(_ != entry)
+    val history_str = history.mkString(provers_history_delim.toString)
+    set_provers_history(history_str)
+  }
+
+  private def reload_persistent_options(): Unit = {
+    persistent_options = Options.init()
+  }
+
+  private def consume_status(status: Query_Operation.Status): Unit = {
+    val msg = status match {
+      case Query_Operation.Status.waiting => "Warte auf Kontext..."
+      case Query_Operation.Status.running => "Sledgehammer läuft..."
+      case Query_Operation.Status.finished => "Beendet"
+    }
+    if (msg.nonEmpty) server.channel.write(LSP.Sledgehammer_Status_Response(msg))
+  }
+
+  private def extractSendbackId(body: List[XML.Elem]): Option[Int] = {
+    def traverse(tree: XML.Tree): Option[Int] = tree match {
+      case XML.Elem(markup, body) if markup.name == "sendback" =>
+        markup.properties.find(_._1 == "id").flatMap {
+          case (_, id_str) => scala.util.Try(id_str.toInt).toOption
+        }.orElse(body.view.flatMap(traverse).headOption)
+
+      case XML.Elem(_, body) =>
+        body.view.flatMap(traverse).headOption
+
+      case _ => None
+    }
+    body.view.flatMap(traverse).headOption
+  }
+
+  private def count_lines(text: String, offset: Int): Int =
+    text.substring(0, offset).count(_ == '\n')
+
+  private def count_column(text: String, offset: Int): Int = {
+    val lastNewline = text.substring(0, offset).lastIndexOf('\n')
+    if (lastNewline >= 0) offset - lastNewline - 1 else offset
+  }
+
+  private def resolvePosition(snapshot: Document.Snapshot, sendbackId: Int): Option[(String, Int, Int)] = {
+    snapshot.node.commands.find(_.id == sendbackId).flatMap { command =>
+      snapshot.node.command_iterator().find(_._1 == command).map {
+        case (_, start_offset) =>
+          val end_offset = start_offset + command.length // Hier nehmen wir das Ende des Command!
+          val text = snapshot.node.source
+          val line = count_lines(text, end_offset)
+          val column = count_column(text, end_offset)
+          val uri = Url.print_file(new java.io.File(snapshot.node_name.node))
+          (uri, line, column)
+      }
+    }
+  }
+
+  private def query_position_from_sendback(snapshot: Document.Snapshot, sendbackId: Int): Option[(String, Int, Int)] = {
+    val node = snapshot.node
+    val iterator = node.command_iterator().toList
+
+    iterator.find(_._1.id == sendbackId).map { case (command, start_offset) =>
+      val text = node.source
+      val line = count_lines(text, start_offset)
+      val column = count_column(text, start_offset)
+      val uri = Url.print_file(new java.io.File(snapshot.node_name.node))
+
+      val snippet = text.substring(start_offset, (start_offset + command.length).min(text.length)).replace("\n", "\\n")
+
+      (uri, line, column)
+    }
+  }
+
+  private def consume_result(snapshot: Document.Snapshot, results: Command.Results, body: List[XML.Elem]): Unit = {
+    val xmlString = body.map(XML.string_of_tree).mkString
+
+    if (xmlString.contains("Done")) {
+      val sendbackIdOpt = extractSendbackId(body)
+      last_sendback_id = sendbackIdOpt
+
+      val position = sendbackIdOpt.flatMap(id => resolvePosition(snapshot, id))
+        .getOrElse(("unknown", 0, 0))
+
+      val query_position = sendbackIdOpt.flatMap(id => query_position_from_sendback(snapshot, id))
+        .getOrElse(("unknown", 0, 0))
+
+      val text = snapshot.node.source
+
+      val resultJson = JSON.Object(
+        "content" -> xmlString,
+        "position" -> JSON.Object(
+          "uri" -> position._1,
+          "line" -> position._2,
+          "character" -> position._3
+        ),
+        "sendbackId" -> sendbackIdOpt.getOrElse(-1),
+        "state_location" -> JSON.Object(
+          "uri" -> query_position._1,
+          "line" -> query_position._2,
+          "character" -> query_position._3)
+      )
+
+      server.channel.write(LSP.Sledgehammer_Apply_Response(resultJson))
+    }
+  }
+
+  def choose_purpose(args: List[String], purpose: Int): Unit = {
+    current_purpose = purpose
+    purpose match {
+      case 1 =>
+        server.resources.get_caret() match {
+          case Some(caret) =>
+            val snapshot = server.resources.snapshot(caret.model)
+            val uri = Url.print_file(caret.file)
+            query_operation.apply_query(args)
+          case None =>
+            server.channel.write(LSP.Sledgehammer_NoProof_Response())
+        }
+
+      case 2 =>
+        locate()
+
+      case 3 =>
+        insert_query()
+
+      case _ =>
+    }
+  }
+
+  def locate(): Unit = {
+    for {
+      sendbackId <- last_sendback_id
+      caret <- server.resources.get_caret()
+      snapshot = server.resources.snapshot(caret.model)
+      query_position <- query_position_from_sendback(snapshot, sendbackId)
+    } {
+      val json = JSON.Object(
+        "position" -> JSON.Object(
+          "uri" -> query_position._1,
+          "line" -> query_position._2,
+          "character" -> query_position._3
+        )
+      )
+      server.channel.write(LSP.Sledgehammer_Locate_Response(json))
+    }
+  }
+
+  def insert_query(): Unit = {
+    last_sendback_id match {
+      case Some(sendbackId) =>
+        val models = server.resources.get_models()
+        val modelOpt = models.find { model =>
+          val snapshot = server.resources.snapshot(model)
+          val contains = snapshot.node.commands.exists(_.id == sendbackId)
+          contains
+        }
+
+        modelOpt match {
+          case Some(model) =>
+            val snapshot = server.resources.snapshot(model)
+            resolvePosition(snapshot, sendbackId) match {
+              case Some((uri, line, col)) =>
+                val json = JSON.Object(
+                  "position" -> JSON.Object(
+                    "uri" -> uri,
+                    "line" -> line,
+                    "character" -> col
+                  )
+                )
+                server.channel.write(LSP.Sledgehammer_InsertPosition_Response(json))
+              case None =>
+            }
+          case None =>
+        }
+      case None =>
+    }
+  }
+
+  def cancel_query(): Unit = query_operation.cancel_query()
+  def locate_query(): Unit = query_operation.locate_query()
+  def init(): Unit = query_operation.activate()
+  def exit(): Unit = query_operation.deactivate()
+}