# HG changeset patch
# User wenzelm
# Date 1762014643 -3600
# Node ID ed531427234a9990ae4797087cc60871591748fd
# Parent  1b6b837345a41d48cf92f36f1c84d05636a69085
discontinue redundant error situations: the sledgehammer command does this already;

diff -r 1b6b837345a4 -r ed531427234a src/Tools/VSCode/extension/media/sledgehammer.js
--- a/src/Tools/VSCode/extension/media/sledgehammer.js	Sat Nov 01 16:35:04 2025 +0100
+++ b/src/Tools/VSCode/extension/media/sledgehammer.js	Sat Nov 01 17:30:43 2025 +0100
@@ -217,12 +217,6 @@
     else if (message.command === "provers" && message.provers) {
       provers_input.value = message.provers;
     }
-    else if (message.command === "no_proof") {
-      const div = document.createElement("div");
-      div.classList.add("interrupt");
-      div.textContent = "Unknown proof context";
-      result.appendChild(div);
-    }
     else if (message.command === "result") {
       if (was_cancelled) return;
       result.innerHTML = "";
diff -r 1b6b837345a4 -r ed531427234a src/Tools/VSCode/extension/src/extension.ts
--- a/src/Tools/VSCode/extension/src/extension.ts	Sat Nov 01 16:35:04 2025 +0100
+++ b/src/Tools/VSCode/extension/src/extension.ts	Sat Nov 01 17:30:43 2025 +0100
@@ -244,8 +244,6 @@
         sledgehammer_provider.insert(msg.position))
       language_client.onNotification(lsp.sledgehammer_provers_response_type, msg =>
         sledgehammer_provider.update_provers(msg.provers))
-      language_client.onNotification(lsp.sledgehammer_no_proof_response_type, () =>
-        sledgehammer_provider.update_no_proof());
     })
 
 
diff -r 1b6b837345a4 -r ed531427234a src/Tools/VSCode/extension/src/lsp.ts
--- a/src/Tools/VSCode/extension/src/lsp.ts	Sat Nov 01 16:35:04 2025 +0100
+++ b/src/Tools/VSCode/extension/src/lsp.ts	Sat Nov 01 17:30:43 2025 +0100
@@ -253,9 +253,6 @@
 export const sledgehammer_insert_position_response_type =
   new NotificationType<SledgehammerInsertPosition>("PIDE/sledgehammer_insert_position_response");
 
-export const sledgehammer_no_proof_response_type =
-  new NotificationType<void>("PIDE/sledgehammer_no_proof_resonse");
-
 
 /* spell checker */
 
diff -r 1b6b837345a4 -r ed531427234a src/Tools/VSCode/extension/src/sledgehammer_panel.ts
--- a/src/Tools/VSCode/extension/src/sledgehammer_panel.ts	Sat Nov 01 16:35:04 2025 +0100
+++ b/src/Tools/VSCode/extension/src/sledgehammer_panel.ts	Sat Nov 01 17:30:43 2025 +0100
@@ -130,12 +130,6 @@
     }
   }
 
-  public update_no_proof(): void {
-    if (this._view) {
-      this._view.webview.postMessage({ command: "no_proof" });
-    }
-  }
-
   private _get_html(): string {
     return get_webview_html(this._view?.webview, this._extension_uri.fsPath);
   }
diff -r 1b6b837345a4 -r ed531427234a src/Tools/VSCode/src/lsp.scala
--- a/src/Tools/VSCode/src/lsp.scala	Sat Nov 01 16:35:04 2025 +0100
+++ b/src/Tools/VSCode/src/lsp.scala	Sat Nov 01 17:30:43 2025 +0100
@@ -836,9 +836,4 @@
     def apply(json: JSON.Object.T): JSON.T =
       Notification("PIDE/sledgehammer_insert_position_response", json)
   }
-
-  object Sledgehammer_No_Proof_Response {
-    def apply(): JSON.T =
-      Notification("PIDE/sledgehammer_no_proof_response", None)
-  }
 }
diff -r 1b6b837345a4 -r ed531427234a src/Tools/VSCode/src/vscode_sledgehammer.scala
--- a/src/Tools/VSCode/src/vscode_sledgehammer.scala	Sat Nov 01 16:35:04 2025 +0100
+++ b/src/Tools/VSCode/src/vscode_sledgehammer.scala	Sat Nov 01 17:30:43 2025 +0100
@@ -23,14 +23,8 @@
   }
 
   def handle_request(provers: String, isar: Boolean, try0: Boolean): Unit =
-    server.resources.get_caret() match {
-      case Some(caret) =>
-        val snapshot = server.resources.snapshot(caret.model)
-        val uri = Url.print_file(caret.file)
-        server.editor.send_dispatcher {
-          query_operation.apply_query(List(provers, isar.toString, try0.toString))
-        }
-      case None => server.channel.write(LSP.Sledgehammer_No_Proof_Response())
+    server.editor.send_dispatcher {
+      query_operation.apply_query(List(provers, isar.toString, try0.toString))
     }
 
   private def consume_status(status: Query_Operation.Status): Unit = {