clarified signature: more uniform names;

--- a/src/Tools/VSCode/extension/src/extension.ts	Sun Oct 26 21:18:27 2025 +0100
+++ b/src/Tools/VSCode/extension/src/extension.ts	Sun Oct 26 21:36:08 2025 +0100
@@ -244,7 +244,7 @@
         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, msg =>
+      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());

--- a/src/Tools/VSCode/extension/src/lsp.ts	Sun Oct 26 21:18:27 2025 +0100
+++ b/src/Tools/VSCode/extension/src/lsp.ts	Sun Oct 26 21:36:08 2025 +0100
@@ -196,10 +196,6 @@
   purpose: number;
 }
 
-export interface Sledgehammer_Status {
-  message: string;
-}
-
 export interface SledgehammerApplyResult {
   content: string;
   position: {
@@ -215,7 +211,7 @@
   };
 }
 
-export interface SledgehammerLocate {
+export interface Sledgehammer_Locate {
   position: {
     uri: string;
     line: number;
@@ -231,6 +227,10 @@
   };
 }
 
+export interface Sledgehammer_Status {
+  message: string;
+}
+
 export interface Sledgehammer_Provers {
   provers: string;
 }
@@ -238,13 +238,13 @@
 export const sledgehammer_request_type =
   new NotificationType<SledgehammerApplyRequest>("PIDE/sledgehammer_request");
 
-export const sledgehammer_cancel_type =
+export const sledgehammer_cancel_request_type =
   new NotificationType<void>("PIDE/sledgehammer_cancel_request");
 
-export const sledgehammer_provers =
+export const sledgehammer_provers_request_type =
   new NotificationType<void>("PIDE/sledgehammer_provers_request");
 
-export const sledgehammer_provers_response =
+export const sledgehammer_provers_response_type =
   new NotificationType<Sledgehammer_Provers>("PIDE/sledgehammer_provers_response");
 
 export const sledgehammer_status_response_type =
@@ -254,7 +254,7 @@
   new NotificationType<SledgehammerApplyResult>("PIDE/sledgehammer_apply_response");
 
 export const sledgehammer_locate_response_type =
-  new NotificationType<SledgehammerLocate>("PIDE/sledgehammer_locate_response");
+  new NotificationType<Sledgehammer_Locate>("PIDE/sledgehammer_locate_response");
 
 export const sledgehammer_insert_position_response_type =
   new NotificationType<SledgehammerInsertPosition>("PIDE/sledgehammer_insert_position_response");

--- a/src/Tools/VSCode/extension/src/sledgehammer_panel.ts	Sun Oct 26 21:18:27 2025 +0100
+++ b/src/Tools/VSCode/extension/src/sledgehammer_panel.ts	Sun Oct 26 21:36:08 2025 +0100
@@ -37,7 +37,7 @@
 
   request_provers(language_client: LanguageClient) {
     if (language_client) {
-      this._language_client.sendNotification(lsp.sledgehammer_provers);
+      this._language_client.sendNotification(lsp.sledgehammer_provers_request_type);
     }
   }
 
@@ -65,7 +65,7 @@
 
           break;
         case "cancel":
-          this._language_client.sendNotification(lsp.sledgehammer_cancel_type);
+          this._language_client.sendNotification(lsp.sledgehammer_cancel_request_type);
           break;
         case "locate":
           this._language_client.sendNotification(lsp.sledgehammer_request_type, {

--- a/src/Tools/VSCode/src/language_server.scala	Sun Oct 26 21:18:27 2025 +0100
+++ b/src/Tools/VSCode/src/language_server.scala	Sun Oct 26 21:36:08 2025 +0100
@@ -551,8 +551,8 @@
           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 => sledgehammer.cancel_query()
-          case LSP.Sledgehammer_Provers => sledgehammer.send_provers()
+          case LSP.Sledgehammer_Cancel_Request => sledgehammer.cancel_query()
+          case LSP.Sledgehammer_Provers_Request => sledgehammer.send_provers()
           case _ => if (!LSP.ResponseMessage.is_empty(json)) log("### IGNORED")
         }
       }

--- a/src/Tools/VSCode/src/lsp.scala	Sun Oct 26 21:18:27 2025 +0100
+++ b/src/Tools/VSCode/src/lsp.scala	Sun Oct 26 21:36:08 2025 +0100
@@ -805,9 +805,14 @@
 
   /* sledgehammer */
 
-  object Sledgehammer_Provers
+  object Sledgehammer_Provers_Request
     extends Notification0("PIDE/sledgehammer_provers_request")
 
+  object Sledgehammer_Provers_Response {
+    def apply(provers: String): JSON.T =
+      Notification("PIDE/sledgehammer_provers_response", JSON.Object("provers" -> provers))
+  }
+
   object Sledgehammer_Request {
     def unapply(json: JSON.T): Option[(String, Boolean, Boolean, Int)] =
       json match {
@@ -822,14 +827,9 @@
       }
   }
 
-  object Sledgehammer_Cancel
+  object Sledgehammer_Cancel_Request
     extends Notification0("PIDE/sledgehammer_cancel_request")
 
-  object Sledgehammer_Provers_Response {
-    def apply(provers: String): JSON.T =
-      Notification("PIDE/sledgehammer_provers_response", JSON.Object("provers" -> provers))
-  }
-
   object Sledgehammer_Status_Response {
     def apply(message: String): JSON.T =
       Notification("PIDE/sledgehammer_status_response", JSON.Object("message" -> message))
@@ -845,7 +845,7 @@
       Notification("PIDE/sledgehammer_locate_response", json)
   }
 
-  object Sledgehammer_InsertPosition_Response {
+  object Sledgehammer_Insert_Position_Response {
     def apply(json: JSON.Object.T): JSON.T =
       Notification("PIDE/sledgehammer_insert_position_response", json)
   }

--- a/src/Tools/VSCode/src/vscode_sledgehammer.scala	Sun Oct 26 21:18:27 2025 +0100
+++ b/src/Tools/VSCode/src/vscode_sledgehammer.scala	Sun Oct 26 21:36:08 2025 +0100
@@ -193,7 +193,7 @@
                     "character" -> col
                   )
                 )
-                server.channel.write(LSP.Sledgehammer_InsertPosition_Response(json))
+                server.channel.write(LSP.Sledgehammer_Insert_Position_Response(json))
               case None =>
             }
           case None =>