clarified signature and protocol (again);

--- a/src/Tools/VSCode/extension/media/sledgehammer.js	Mon Oct 27 15:45:06 2025 +0100
+++ b/src/Tools/VSCode/extension/media/sledgehammer.js	Mon Oct 27 16:20:06 2025 +0100
@@ -247,15 +247,8 @@
             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: provers_input.value,
-                  isar: isar_checkbox.checked,
-                  try0: try0_checkbox.checked,
-                  text: node.textContent.trim()
-                });
-              });
+              button.addEventListener("click", () =>
+                vscode.postMessage({ command: "insert", text: node.textContent.trim() }));
               div.appendChild(button);
             }
             else {

--- a/src/Tools/VSCode/extension/src/extension.ts	Mon Oct 27 15:45:06 2025 +0100
+++ b/src/Tools/VSCode/extension/src/extension.ts	Mon Oct 27 16:20:06 2025 +0100
@@ -236,10 +236,10 @@
     language_client.onReady().then(() => sledgehammer_provider.request_provers(language_client))
 
     language_client.onReady().then(() => {
-      language_client.onNotification(lsp.sledgehammer_status_response_type, msg =>
+      language_client.onNotification(lsp.sledgehammer_status_type, msg =>
         sledgehammer_provider.update_status(msg.message))
-      language_client.onNotification(lsp.sledgehammer_apply_response_type, msg =>
-        sledgehammer_provider.updateResult(msg))
+      language_client.onNotification(lsp.sledgehammer_output_type, msg =>
+        sledgehammer_provider.update_output(msg))
       language_client.onNotification(lsp.sledgehammer_insert_position_response_type, msg =>
         sledgehammer_provider.insert(msg.position))
       language_client.onNotification(lsp.sledgehammer_provers_response_type, msg =>

--- a/src/Tools/VSCode/extension/src/lsp.ts	Mon Oct 27 15:45:06 2025 +0100
+++ b/src/Tools/VSCode/extension/src/lsp.ts	Mon Oct 27 16:20:06 2025 +0100
@@ -189,14 +189,17 @@
 
 /* Sledgehammer */
 
-export interface SledgehammerApplyRequest {
+export interface Sledgehammer_Request {
   provers: string;
   isar: boolean;
   try0: boolean;
-  purpose: number;
 }
 
-export interface SledgehammerApplyResult {
+export interface Sledgehammer_Status {
+  message: string;
+}
+
+export interface Sledgehammer_Output {
   content: string;
   position: {
     uri: string;
@@ -219,16 +222,12 @@
   };
 }
 
-export interface Sledgehammer_Status {
-  message: string;
-}
-
 export interface Sledgehammer_Provers {
   provers: string;
 }
 
 export const sledgehammer_request_type =
-  new NotificationType<SledgehammerApplyRequest>("PIDE/sledgehammer_request");
+  new NotificationType<Sledgehammer_Request>("PIDE/sledgehammer_request");
 
 export const sledgehammer_cancel_type =
   new NotificationType<void>("PIDE/sledgehammer_cancel");
@@ -236,17 +235,20 @@
 export const sledgehammer_locate_type =
   new NotificationType<void>("PIDE/sledgehammer_locate");
 
+export const sledgehammer_insert_type =
+  new NotificationType<void>("PIDE/sledgehammer_insert");
+
 export const sledgehammer_provers_request_type =
   new NotificationType<void>("PIDE/sledgehammer_provers_request");
 
 export const sledgehammer_provers_response_type =
   new NotificationType<Sledgehammer_Provers>("PIDE/sledgehammer_provers_response");
 
-export const sledgehammer_status_response_type =
-  new NotificationType<Sledgehammer_Status>("PIDE/sledgehammer_status_response");
+export const sledgehammer_status_type =
+  new NotificationType<Sledgehammer_Status>("PIDE/sledgehammer_status");
 
-export const sledgehammer_apply_response_type =
-  new NotificationType<SledgehammerApplyResult>("PIDE/sledgehammer_apply_response");
+export const sledgehammer_output_type =
+  new NotificationType<Sledgehammer_Output>("PIDE/sledgehammer_output");
 
 export const sledgehammer_insert_position_response_type =
   new NotificationType<SledgehammerInsertPosition>("PIDE/sledgehammer_insert_position_response");

--- a/src/Tools/VSCode/extension/src/sledgehammer_panel.ts	Mon Oct 27 15:45:06 2025 +0100
+++ b/src/Tools/VSCode/extension/src/sledgehammer_panel.ts	Mon Oct 27 16:20:06 2025 +0100
@@ -59,8 +59,7 @@
           this._language_client.sendNotification(lsp.sledgehammer_request_type, {
             provers: message.provers,
             isar: message.isar,
-            try0: message.try0,
-            purpose: 1
+            try0: message.try0
           });
           break;
         case "cancel":
@@ -69,13 +68,8 @@
         case "locate":
           this._language_client.sendNotification(lsp.sledgehammer_locate_type);
           break;
-        case "insert_text":
-          this._language_client.sendNotification(lsp.sledgehammer_request_type, {
-            provers: message.provers,
-            isar: message.isar,
-            try0: message.try0,
-            purpose: 3
-          });
+        case "insert":
+          this._language_client.sendNotification(lsp.sledgehammer_insert_type);
           this.text_to_insert = message.text;
           break;
       }
@@ -123,7 +117,7 @@
   }
 
 
-  public updateResult(result: lsp.SledgehammerApplyResult): void {
+  public update_output(result: lsp.Sledgehammer_Output): void {
     const editor = window.activeTextEditor;
     const lineText = editor?.document.lineAt(result.position.line).text ?? "";
     this._lastResultPosition = {

--- a/src/Tools/VSCode/src/language_server.scala	Mon Oct 27 15:45:06 2025 +0100
+++ b/src/Tools/VSCode/src/language_server.scala	Mon Oct 27 16:20:06 2025 +0100
@@ -549,10 +549,11 @@
           case LSP.Preview_Request(file, column) => preview_request(file, column)
           case LSP.Symbols_Panel_Request => symbols_panel_request()
           case LSP.Documentation_Request => documentation_request()
-          case LSP.Sledgehammer_Request(provers, isar, try0, purpose) =>
-            sledgehammer.handle_request(provers, isar, try0, purpose)
+          case LSP.Sledgehammer_Request(provers, isar, try0) =>
+            sledgehammer.handle_request(provers, isar, try0)
           case LSP.Sledgehammer_Cancel(()) => sledgehammer.cancel()
           case LSP.Sledgehammer_Locate(()) => sledgehammer.locate()
+          case LSP.Sledgehammer_Insert(()) => sledgehammer.insert()
           case LSP.Sledgehammer_Provers_Request(()) => sledgehammer.send_provers()
           case _ => if (!LSP.ResponseMessage.is_empty(json)) log("### IGNORED")
         }

--- a/src/Tools/VSCode/src/lsp.scala	Mon Oct 27 15:45:06 2025 +0100
+++ b/src/Tools/VSCode/src/lsp.scala	Mon Oct 27 16:20:06 2025 +0100
@@ -808,32 +808,33 @@
   }
 
   object Sledgehammer_Request {
-    def unapply(json: JSON.T): Option[(String, Boolean, Boolean, Int)] =
+    def unapply(json: JSON.T): Option[(String, Boolean, Boolean)] =
       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_default(params, "purpose", 1)
-          } yield (provers, isar, try0, purpose)
+          } yield (provers, isar, try0)
         case _ => None
       }
   }
 
+  object Sledgehammer_Status {
+    def apply(message: String): JSON.T =
+      Notification("PIDE/sledgehammer_status", JSON.Object("message" -> message))
+  }
+
+  object Sledgehammer_Output {
+    def apply(json: JSON.Object.T): JSON.T =
+      Notification("PIDE/sledgehammer_output", json)
+  }
+
   object Sledgehammer_Cancel extends Notification0("PIDE/sledgehammer_cancel")
 
   object Sledgehammer_Locate extends Notification0("PIDE/sledgehammer_locate")
 
-  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(json: JSON.Object.T): JSON.T =
-      Notification("PIDE/sledgehammer_apply_response", json)
-  }
+  object Sledgehammer_Insert extends Notification0("PIDE/sledgehammer_insert")
 
   object Sledgehammer_Insert_Position_Response {
     def apply(json: JSON.Object.T): JSON.T =

--- a/src/Tools/VSCode/src/vscode_sledgehammer.scala	Mon Oct 27 15:45:06 2025 +0100
+++ b/src/Tools/VSCode/src/vscode_sledgehammer.scala	Mon Oct 27 16:20:06 2025 +0100
@@ -29,22 +29,16 @@
     server.channel.write(LSP.Sledgehammer_Provers_Response.apply(provers))
   }
 
-  def handle_request(provers: String, isar: Boolean, try0: Boolean, purpose: Int): Unit = {
-    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())
+  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 3 => insert_query()
-      case _ =>
+      case None => server.channel.write(LSP.Sledgehammer_No_Proof_Response())
     }
-  }
 
   private def consume_status(status: Query_Operation.Status): Unit = {
     val msg =
@@ -53,7 +47,7 @@
         case Query_Operation.Status.running => "Sledgehammering ..."
         case Query_Operation.Status.finished => "Finished"
       }
-    server.channel.write(LSP.Sledgehammer_Status_Response(msg))
+    server.channel.write(LSP.Sledgehammer_Status(msg))
   }
 
   private def extract_sendback_id(body: List[XML.Elem]): Option[Int] = {
@@ -143,10 +137,10 @@
         "line" -> query_position._2,
         "character" -> query_position._3)
     )
-    server.channel.write(LSP.Sledgehammer_Apply_Response(json))
+    server.channel.write(LSP.Sledgehammer_Output(json))
   }
 
-  def insert_query(): Unit = {
+  def insert(): Unit = {
     last_sendback_id match {
       case Some(sendback_id) =>
         val models = server.resources.get_models()