discontinue redundant treatment of interrupts: this is already done by Isabelle/Scala/ML;
authorwenzelm
Sat, 01 Nov 2025 18:02:31 +0100
changeset 83447 83dccdabf0a1
parent 83446 c0c0d860acd2
child 83448 8514909bb601
discontinue redundant treatment of interrupts: this is already done by Isabelle/Scala/ML;
src/Tools/VSCode/extension/media/sledgehammer.css
src/Tools/VSCode/extension/media/sledgehammer.js
--- a/src/Tools/VSCode/extension/media/sledgehammer.css	Sat Nov 01 17:54:44 2025 +0100
+++ b/src/Tools/VSCode/extension/media/sledgehammer.css	Sat Nov 01 18:02:31 2025 +0100
@@ -152,16 +152,6 @@
   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 {
   background-color: var(--vscode-editorError-background);
   color: var(--vscode-editorError-foreground);
--- a/src/Tools/VSCode/extension/media/sledgehammer.js	Sat Nov 01 17:54:44 2025 +0100
+++ b/src/Tools/VSCode/extension/media/sledgehammer.js	Sat Nov 01 18:02:31 2025 +0100
@@ -1,7 +1,5 @@
 (function () {
   const vscode = acquireVsCodeApi();
-  let was_cancelled = false;
-  let can_be_cancelled = false;
 
   let history = [];
 
@@ -161,8 +159,6 @@
   apply_button.textContent = "Apply";
   apply_button.id = "apply-btn";
   apply_button.addEventListener("click", () => {
-    was_cancelled = false;
-    can_be_cancelled = true;
     result.innerHTML = "";
     add_to_history(provers_input.value);
     hide_dropdown();
@@ -176,17 +172,7 @@
 
   const cancel_button = document.createElement("button");
   cancel_button.textContent = "Cancel";
-  cancel_button.addEventListener("click", () => {
-    vscode.postMessage({ command: "cancel" });
-    if (was_cancelled) return;
-    if (!can_be_cancelled) return;
-    was_cancelled = true;
-    spinner.classList.remove("loading");
-    const div = document.createElement("div");
-    div.classList.add("interrupt");
-    div.textContent = "Interrupt";
-    result.appendChild(div);
-  });
+  cancel_button.addEventListener("click", () => vscode.postMessage({ command: "cancel" }));
 
   const locate_button = document.createElement("button");
   locate_button.textContent = "Locate";
@@ -218,7 +204,6 @@
       provers_input.value = message.provers;
     }
     else if (message.command === "result") {
-      if (was_cancelled) return;
       result.innerHTML = "";
       const parser = new DOMParser();
       const xml_doc = parser.parseFromString(`<root>${message.content}</root>`, "application/xml");
@@ -259,7 +244,6 @@
           result.appendChild(div);
         }
       }
-      can_be_cancelled = false;
     }
   });