various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München;
--- 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 \
--- 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 =>
+ }
}
}
--- 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)"
--- 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
--- /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
--- /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);
+}
--- /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
--- /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
--- /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
--- /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
--- /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);
+ }
+ };
+})();
--- /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
--- /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; }
+}
--- /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);
+ }
+ };
+
+})();
--- 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": [
{
--- /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 };
+
--- 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 */
--- 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")
--- /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;
+}
--- /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 }
--- 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")
}
}
--- 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)
+ }
+
}
+
--- /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()
+}
