# HG changeset patch
# User wenzelm
# Date 1761561572 -3600
# Node ID f61236e8c7b0c4653b153b5f39b9f4d082c3dcbd
# Parent  068cfdd057d087783a8f1efa8ef7921be003f9cf
clarified signature and protocol (again);

diff -r 068cfdd057d0 -r f61236e8c7b0 src/Tools/VSCode/extension/src/lsp.ts
--- a/src/Tools/VSCode/extension/src/lsp.ts	Mon Oct 27 11:09:41 2025 +0100
+++ b/src/Tools/VSCode/extension/src/lsp.ts	Mon Oct 27 11:39:32 2025 +0100
@@ -238,8 +238,8 @@
 export const sledgehammer_request_type =
   new NotificationType<SledgehammerApplyRequest>("PIDE/sledgehammer_request");
 
-export const sledgehammer_cancel_request_type =
-  new NotificationType<void>("PIDE/sledgehammer_cancel_request");
+export const sledgehammer_cancel_type =
+  new NotificationType<void>("PIDE/sledgehammer_cancel");
 
 export const sledgehammer_provers_request_type =
   new NotificationType<void>("PIDE/sledgehammer_provers_request");
diff -r 068cfdd057d0 -r f61236e8c7b0 src/Tools/VSCode/extension/src/sledgehammer_panel.ts
--- a/src/Tools/VSCode/extension/src/sledgehammer_panel.ts	Mon Oct 27 11:09:41 2025 +0100
+++ b/src/Tools/VSCode/extension/src/sledgehammer_panel.ts	Mon Oct 27 11:39:32 2025 +0100
@@ -65,7 +65,7 @@
 
           break;
         case "cancel":
-          this._language_client.sendNotification(lsp.sledgehammer_cancel_request_type);
+          this._language_client.sendNotification(lsp.sledgehammer_cancel_type);
           break;
         case "locate":
           this._language_client.sendNotification(lsp.sledgehammer_request_type, {
diff -r 068cfdd057d0 -r f61236e8c7b0 src/Tools/VSCode/src/language_server.scala
--- a/src/Tools/VSCode/src/language_server.scala	Mon Oct 27 11:09:41 2025 +0100
+++ b/src/Tools/VSCode/src/language_server.scala	Mon Oct 27 11:39:32 2025 +0100
@@ -551,7 +551,7 @@
           case LSP.Documentation_Request => documentation_request()
           case LSP.Sledgehammer_Request(provers, isar, try0, purpose) =>
             sledgehammer.handle_request(provers, isar, try0, purpose)
-          case LSP.Sledgehammer_Cancel_Request => sledgehammer.cancel_query()
+          case LSP.Sledgehammer_Cancel => sledgehammer.cancel()
           case LSP.Sledgehammer_Provers_Request => sledgehammer.send_provers()
           case _ => if (!LSP.ResponseMessage.is_empty(json)) log("### IGNORED")
         }
diff -r 068cfdd057d0 -r f61236e8c7b0 src/Tools/VSCode/src/lsp.scala
--- a/src/Tools/VSCode/src/lsp.scala	Mon Oct 27 11:09:41 2025 +0100
+++ b/src/Tools/VSCode/src/lsp.scala	Mon Oct 27 11:39:32 2025 +0100
@@ -821,8 +821,7 @@
       }
   }
 
-  object Sledgehammer_Cancel_Request
-    extends Notification0("PIDE/sledgehammer_cancel_request")
+  object Sledgehammer_Cancel extends Notification0("PIDE/sledgehammer_cancel")
 
   object Sledgehammer_Status_Response {
     def apply(message: String): JSON.T =
diff -r 068cfdd057d0 -r f61236e8c7b0 src/Tools/VSCode/src/vscode_sledgehammer.scala
--- a/src/Tools/VSCode/src/vscode_sledgehammer.scala	Mon Oct 27 11:09:41 2025 +0100
+++ b/src/Tools/VSCode/src/vscode_sledgehammer.scala	Mon Oct 27 11:39:32 2025 +0100
@@ -202,7 +202,7 @@
     }
   }
 
-  def cancel_query(): Unit = query_operation.cancel_query()
+  def cancel(): Unit = query_operation.cancel_query()
   def locate_query(): Unit = query_operation.locate_query()
   def init(): Unit = query_operation.activate()
   def exit(): Unit = query_operation.deactivate()