removed attempts at error detection: this is the job of sledgehammer in Isabelle/ML;

--- a/src/Tools/VSCode/extension/media/sledgehammer.js	Sun Oct 26 20:46:09 2025 +0100
+++ b/src/Tools/VSCode/extension/media/sledgehammer.js	Sun Oct 26 21:02:21 2025 +0100
@@ -230,12 +230,6 @@
       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 (was_cancelled) return;
       result.innerHTML = "";

--- a/src/Tools/VSCode/extension/src/extension.ts	Sun Oct 26 20:46:09 2025 +0100
+++ b/src/Tools/VSCode/extension/src/extension.ts	Sun Oct 26 21:02:21 2025 +0100
@@ -240,8 +240,6 @@
         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 =>

--- a/src/Tools/VSCode/extension/src/lsp.ts	Sun Oct 26 20:46:09 2025 +0100
+++ b/src/Tools/VSCode/extension/src/lsp.ts	Sun Oct 26 21:02:21 2025 +0100
@@ -251,9 +251,6 @@
 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");
 

--- a/src/Tools/VSCode/extension/src/sledgehammer_panel.ts	Sun Oct 26 20:46:09 2025 +0100
+++ b/src/Tools/VSCode/extension/src/sledgehammer_panel.ts	Sun Oct 26 21:02:21 2025 +0100
@@ -149,13 +149,6 @@
     }
   }
 
-  public updateNoProver(provers: lsp.SledgehammerNoSuchProver): void {
-    if (this._view) {
-      this._view.webview.postMessage({ command: "no_provers" });
-    }
-  }
-
-
   public update_no_proof(): void {
     if (this._view) {
       this._view.webview.postMessage({ command: "no_proof" });

--- a/src/Tools/VSCode/src/lsp.scala	Sun Oct 26 20:46:09 2025 +0100
+++ b/src/Tools/VSCode/src/lsp.scala	Sun Oct 26 21:02:21 2025 +0100
@@ -830,11 +830,6 @@
       Notification("PIDE/sledgehammer_provers_response", JSON.Object("provers" -> provers))
   }
 
-  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))