# HG changeset patch
# User wenzelm
# Date 1761503918 -3600
# Node ID 6ac2c6c2e549307ce4b49312b7d298a3ea1f8e58
# Parent  4c9ed0e60da20a0f9569b67f5a2a36467d643120
more direct treatment of "purpose";
clarified message names;

diff -r 4c9ed0e60da2 -r 6ac2c6c2e549 src/Tools/VSCode/extension/media/sledgehammer.js
--- a/src/Tools/VSCode/extension/media/sledgehammer.js	Sun Oct 26 19:22:05 2025 +0100
+++ b/src/Tools/VSCode/extension/media/sledgehammer.js	Sun Oct 26 19:38:38 2025 +0100
@@ -224,7 +224,7 @@
     else if (message.command === "provers" && message.provers) {
       provers_input.value = message.provers;
     }
-    else if (message.command === "no_proof_context") {
+    else if (message.command === "no_proof") {
       const div = document.createElement("div");
       div.classList.add("interrupt");
       div.textContent = "Unknown proof context";
diff -r 4c9ed0e60da2 -r 6ac2c6c2e549 src/Tools/VSCode/extension/src/extension.ts
--- a/src/Tools/VSCode/extension/src/extension.ts	Sun Oct 26 19:22:05 2025 +0100
+++ b/src/Tools/VSCode/extension/src/extension.ts	Sun Oct 26 19:38:38 2025 +0100
@@ -248,8 +248,8 @@
         sledgehammer_provider.locate(msg.position))
       language_client.onNotification(lsp.sledgehammer_provers_response, msg =>
         sledgehammer_provider.update_provers(msg.provers))
-      language_client.onNotification(lsp.sledgehammer_no_proof_context_type, () =>
-        sledgehammer_provider.updateNoProofContext());
+      language_client.onNotification(lsp.sledgehammer_no_proof_response_type, () =>
+        sledgehammer_provider.update_no_proof());
     })
 
 
diff -r 4c9ed0e60da2 -r 6ac2c6c2e549 src/Tools/VSCode/extension/src/lsp.ts
--- a/src/Tools/VSCode/extension/src/lsp.ts	Sun Oct 26 19:22:05 2025 +0100
+++ b/src/Tools/VSCode/extension/src/lsp.ts	Sun Oct 26 19:38:38 2025 +0100
@@ -270,8 +270,8 @@
 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 sledgehammer_no_proof_response_type =
+  new NotificationType<void>("PIDE/sledgehammer_no_proof_resonse");
 
 
 /* spell checker */
diff -r 4c9ed0e60da2 -r 6ac2c6c2e549 src/Tools/VSCode/extension/src/sledgehammer_panel.ts
--- a/src/Tools/VSCode/extension/src/sledgehammer_panel.ts	Sun Oct 26 19:22:05 2025 +0100
+++ b/src/Tools/VSCode/extension/src/sledgehammer_panel.ts	Sun Oct 26 19:38:38 2025 +0100
@@ -156,9 +156,9 @@
   }
 
 
-  public updateNoProofContext(): void {
+  public update_no_proof(): void {
     if (this._view) {
-      this._view.webview.postMessage({ command: "no_proof_context" });
+      this._view.webview.postMessage({ command: "no_proof" });
     }
   }
 
diff -r 4c9ed0e60da2 -r 6ac2c6c2e549 src/Tools/VSCode/src/lsp.scala
--- a/src/Tools/VSCode/src/lsp.scala	Sun Oct 26 19:22:05 2025 +0100
+++ b/src/Tools/VSCode/src/lsp.scala	Sun Oct 26 19:38:38 2025 +0100
@@ -861,8 +861,8 @@
       Notification("PIDE/sledgehammer_insert_position_response", json)
   }
 
-  object Sledgehammer_NoProof_Response{
+  object Sledgehammer_No_Proof_Response {
     def apply(): JSON.T =
-      Notification("PIDE/sledgehammer_no_proof_context", None)
+      Notification("PIDE/sledgehammer_no_proof_response", None)
   }
 }
diff -r 4c9ed0e60da2 -r 6ac2c6c2e549 src/Tools/VSCode/src/vscode_sledgehammer.scala
--- a/src/Tools/VSCode/src/vscode_sledgehammer.scala	Sun Oct 26 19:22:05 2025 +0100
+++ b/src/Tools/VSCode/src/vscode_sledgehammer.scala	Sun Oct 26 19:38:38 2025 +0100
@@ -21,7 +21,7 @@
 class VSCode_Sledgehammer 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
 
   def send_provers(): Unit = {
@@ -30,14 +30,21 @@
   }
 
   def handle_request(provers: String, isar: Boolean, try0: Boolean, purpose: Int): Unit = {
-    val available_provers = Word.explode(server.options.string("sledgehammer_provers")).toSet
-    val user_provers = Word.explode(provers).toSet
-    val invalid = user_provers.diff(available_provers)
-    if (invalid.nonEmpty) {
-      server.channel.write(LSP.Sledgehammer_NoProver_Response.apply(invalid.toList))
-      return
+    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)
+            server.editor.send_dispatcher {
+              query_operation.apply_query(List(provers, isar.toString, try0.toString))
+            }
+          case None => server.channel.write(LSP.Sledgehammer_No_Proof_Response())
+        }
+      case 2 => locate()
+      case 3 => insert_query()
+      case _ =>
     }
-    choose_purpose(List(provers, isar.toString, try0.toString), purpose)
   }
 
   private def consume_status(status: Query_Operation.Status): Unit = {
@@ -145,29 +152,6 @@
     }
   }
 
-  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)
-            server.editor.send_dispatcher { 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 {
       sendback_id <- last_sendback_id