clarified signature: more uniform names;

--- a/src/Tools/VSCode/extension/src/extension.ts	Sun Oct 26 21:02:21 2025 +0100
+++ b/src/Tools/VSCode/extension/src/extension.ts	Sun Oct 26 21:16:52 2025 +0100
@@ -236,8 +236,8 @@
     language_client.onReady().then(() => sledgehammer_provider.request_provers(language_client))
 
     language_client.onReady().then(() => {
-      language_client.onNotification(lsp.sledgehammer_status_type, msg =>
-        sledgehammer_provider.updateStatus(msg.message))
+      language_client.onNotification(lsp.sledgehammer_status_response_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_insert_position_response_type, msg =>

--- a/src/Tools/VSCode/extension/src/lsp.ts	Sun Oct 26 21:02:21 2025 +0100
+++ b/src/Tools/VSCode/extension/src/lsp.ts	Sun Oct 26 21:16:52 2025 +0100
@@ -196,7 +196,7 @@
   purpose: number;
 }
 
-export interface SledgehammerStatus {
+export interface Sledgehammer_Status {
   message: string;
 }
 
@@ -251,8 +251,8 @@
 export const sledgehammer_provers_response =
   new NotificationType<Sledgehammer_Provers>("PIDE/sledgehammer_provers_response");
 
-export const sledgehammer_status_type =
-  new NotificationType<SledgehammerStatus>("PIDE/sledgehammer_status_response");
+export const sledgehammer_status_response_type =
+  new NotificationType<Sledgehammer_Status>("PIDE/sledgehammer_status_response");
 
 export const sledgehammer_apply_response_type =
   new NotificationType<SledgehammerApplyResult>("PIDE/sledgehammer_apply_response");

--- a/src/Tools/VSCode/extension/src/sledgehammer_panel.ts	Sun Oct 26 21:02:21 2025 +0100
+++ b/src/Tools/VSCode/extension/src/sledgehammer_panel.ts	Sun Oct 26 21:16:52 2025 +0100
@@ -89,7 +89,7 @@
     });
   }
 
-  public updateStatus(message: string): void {
+  public update_status(message: string): void {
     if (this._view) {
       this._view.webview.postMessage({ command: "status", message });
     }

--- a/src/Tools/VSCode/src/vscode_sledgehammer.scala	Sun Oct 26 21:02:21 2025 +0100
+++ b/src/Tools/VSCode/src/vscode_sledgehammer.scala	Sun Oct 26 21:16:52 2025 +0100
@@ -48,12 +48,13 @@
   }
 
   private def consume_status(status: Query_Operation.Status): Unit = {
-    val msg = status match {
-      case Query_Operation.Status.waiting => "Waiting for evaluation of context ..."
-      case Query_Operation.Status.running => "Sledgehammering ..."
-      case Query_Operation.Status.finished => "Finished"
-    }
-    if (msg.nonEmpty) server.channel.write(LSP.Sledgehammer_Status_Response(msg))
+    val msg =
+      status match {
+        case Query_Operation.Status.waiting => "Waiting for evaluation of context ..."
+        case Query_Operation.Status.running => "Sledgehammering ..."
+        case Query_Operation.Status.finished => "Finished"
+      }
+    server.channel.write(LSP.Sledgehammer_Status_Response(msg))
   }
 
   private def extract_sendback_id(body: List[XML.Elem]): Option[Int] = {