# HG changeset patch
# User wenzelm
# Date 1761565051 -3600
# Node ID c7849fa2ece0a653cfa9bf991900817c8fe48180
# Parent  e78d50e3e1eb238e92f28aacded89b0f645adcf5
more direct sledgehammer "locate" operation via official Query_Operation interface;
proper editor.send_dispatcher for "cancel" and "locate";

diff -r e78d50e3e1eb -r c7849fa2ece0 src/Tools/VSCode/extension/media/sledgehammer.js
--- a/src/Tools/VSCode/extension/media/sledgehammer.js	Mon Oct 27 12:15:14 2025 +0100
+++ b/src/Tools/VSCode/extension/media/sledgehammer.js	Mon Oct 27 12:37:31 2025 +0100
@@ -190,14 +190,7 @@
 
   const locate_button = document.createElement("button");
   locate_button.textContent = "Locate";
-  locate_button.addEventListener("click", () => {
-    vscode.postMessage({
-      command: "locate",
-      provers: provers_input.value,
-      isar: isar_checkbox.checked,
-      try0: try0_checkbox.checked
-    });
-  });
+  locate_button.addEventListener("click", () => vscode.postMessage({ command: "locate" }));
 
   top_row.appendChild(provers_label);
   top_row.appendChild(isar_label);
diff -r e78d50e3e1eb -r c7849fa2ece0 src/Tools/VSCode/extension/src/extension.ts
--- a/src/Tools/VSCode/extension/src/extension.ts	Mon Oct 27 12:15:14 2025 +0100
+++ b/src/Tools/VSCode/extension/src/extension.ts	Mon Oct 27 12:37:31 2025 +0100
@@ -242,8 +242,6 @@
         sledgehammer_provider.updateResult(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 =>
-        sledgehammer_provider.locate(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, () =>
diff -r e78d50e3e1eb -r c7849fa2ece0 src/Tools/VSCode/extension/src/lsp.ts
--- a/src/Tools/VSCode/extension/src/lsp.ts	Mon Oct 27 12:15:14 2025 +0100
+++ b/src/Tools/VSCode/extension/src/lsp.ts	Mon Oct 27 12:37:31 2025 +0100
@@ -211,14 +211,6 @@
   };
 }
 
-export interface Sledgehammer_Locate {
-  position: {
-    uri: string;
-    line: number;
-    character: number;
-  };
-}
-
 export interface SledgehammerInsertPosition {
   position: {
     uri: string;
@@ -241,6 +233,9 @@
 export const sledgehammer_cancel_type =
   new NotificationType<void>("PIDE/sledgehammer_cancel");
 
+export const sledgehammer_locate_type =
+  new NotificationType<void>("PIDE/sledgehammer_locate");
+
 export const sledgehammer_provers_request_type =
   new NotificationType<void>("PIDE/sledgehammer_provers_request");
 
@@ -253,9 +248,6 @@
 export const sledgehammer_apply_response_type =
   new NotificationType<SledgehammerApplyResult>("PIDE/sledgehammer_apply_response");
 
-export const sledgehammer_locate_response_type =
-  new NotificationType<Sledgehammer_Locate>("PIDE/sledgehammer_locate_response");
-
 export const sledgehammer_insert_position_response_type =
   new NotificationType<SledgehammerInsertPosition>("PIDE/sledgehammer_insert_position_response");
 
diff -r e78d50e3e1eb -r c7849fa2ece0 src/Tools/VSCode/extension/src/sledgehammer_panel.ts
--- a/src/Tools/VSCode/extension/src/sledgehammer_panel.ts	Mon Oct 27 12:15:14 2025 +0100
+++ b/src/Tools/VSCode/extension/src/sledgehammer_panel.ts	Mon Oct 27 12:37:31 2025 +0100
@@ -62,20 +62,13 @@
             try0: message.try0,
             purpose: 1
           });
-
           break;
         case "cancel":
           this._language_client.sendNotification(lsp.sledgehammer_cancel_type);
           break;
         case "locate":
-          this._language_client.sendNotification(lsp.sledgehammer_request_type, {
-            provers: message.provers,
-            isar: message.isar,
-            try0: message.try0,
-            purpose: 2
-          });
+          this._language_client.sendNotification(lsp.sledgehammer_locate_type);
           break;
-
         case "insert_text":
           this._language_client.sendNotification(lsp.sledgehammer_request_type, {
             provers: message.provers,
diff -r e78d50e3e1eb -r c7849fa2ece0 src/Tools/VSCode/src/language_server.scala
--- a/src/Tools/VSCode/src/language_server.scala	Mon Oct 27 12:15:14 2025 +0100
+++ b/src/Tools/VSCode/src/language_server.scala	Mon Oct 27 12:37:31 2025 +0100
@@ -552,6 +552,7 @@
           case LSP.Sledgehammer_Request(provers, isar, try0, purpose) =>
             sledgehammer.handle_request(provers, isar, try0, purpose)
           case LSP.Sledgehammer_Cancel(()) => sledgehammer.cancel()
+          case LSP.Sledgehammer_Locate(()) => sledgehammer.locate()
           case LSP.Sledgehammer_Provers_Request(()) => sledgehammer.send_provers()
           case _ => if (!LSP.ResponseMessage.is_empty(json)) log("### IGNORED")
         }
diff -r e78d50e3e1eb -r c7849fa2ece0 src/Tools/VSCode/src/lsp.scala
--- a/src/Tools/VSCode/src/lsp.scala	Mon Oct 27 12:15:14 2025 +0100
+++ b/src/Tools/VSCode/src/lsp.scala	Mon Oct 27 12:37:31 2025 +0100
@@ -823,6 +823,8 @@
 
   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))
@@ -833,11 +835,6 @@
       Notification("PIDE/sledgehammer_apply_response", json)
   }
 
-  object Sledgehammer_Locate_Response {
-    def apply(json: JSON.Object.T): JSON.T =
-      Notification("PIDE/sledgehammer_locate_response", json)
-  }
-
   object Sledgehammer_Insert_Position_Response {
     def apply(json: JSON.Object.T): JSON.T =
       Notification("PIDE/sledgehammer_insert_position_response", json)
diff -r e78d50e3e1eb -r c7849fa2ece0 src/Tools/VSCode/src/vscode_sledgehammer.scala
--- a/src/Tools/VSCode/src/vscode_sledgehammer.scala	Mon Oct 27 12:15:14 2025 +0100
+++ b/src/Tools/VSCode/src/vscode_sledgehammer.scala	Mon Oct 27 12:37:31 2025 +0100
@@ -41,7 +41,6 @@
             }
           case None => server.channel.write(LSP.Sledgehammer_No_Proof_Response())
         }
-      case 2 => locate()
       case 3 => insert_query()
       case _ =>
     }
@@ -153,24 +152,6 @@
     }
   }
 
-  def locate(): Unit = {
-    for {
-      sendback_id <- last_sendback_id
-      caret <- server.resources.get_caret()
-      snapshot = server.resources.snapshot(caret.model)
-      query_position <- query_position_from_sendback(snapshot, sendback_id)
-    } {
-      val json = JSON.Object(
-        "position" -> JSON.Object(
-          "uri" -> query_position._1,
-          "line" -> query_position._2,
-          "character" -> query_position._3
-        )
-      )
-      server.channel.write(LSP.Sledgehammer_Locate_Response(json))
-    }
-  }
-
   def insert_query(): Unit = {
     last_sendback_id match {
       case Some(sendback_id) =>
@@ -202,8 +183,8 @@
     }
   }
 
-  def cancel(): Unit = query_operation.cancel_query()
-  def locate_query(): Unit = query_operation.locate_query()
+  def cancel(): Unit = server.editor.send_dispatcher { query_operation.cancel_query() }
+  def locate(): Unit = server.editor.send_dispatcher { query_operation.locate_query() }
   def init(): Unit = query_operation.activate()
   def exit(): Unit = query_operation.deactivate()
 }