clarified signature;

--- a/src/Tools/VSCode/src/language_server.scala	Sun Nov 02 16:00:25 2025 +0100
+++ b/src/Tools/VSCode/src/language_server.scala	Sun Nov 02 16:07:47 2025 +0100
@@ -539,11 +539,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_Provers_Request() => sledgehammer.provers()
           case LSP.Sledgehammer_Request(args) => sledgehammer.request(args)
           case LSP.Sledgehammer_Cancel() => sledgehammer.cancel()
           case LSP.Sledgehammer_Locate() => sledgehammer.locate()
           case LSP.Sledgehammer_Sendback(text) => sledgehammer.sendback(text)
-          case LSP.Sledgehammer_Provers_Request() => sledgehammer.send_provers()
           case _ => if (!LSP.ResponseMessage.is_empty(json)) log("### IGNORED")
         }
       }

--- a/src/Tools/VSCode/src/vscode_sledgehammer.scala	Sun Nov 02 16:00:25 2025 +0100
+++ b/src/Tools/VSCode/src/vscode_sledgehammer.scala	Sun Nov 02 16:07:47 2025 +0100
@@ -15,11 +15,6 @@
   private val query_operation =
     new Query_Operation(server.editor, (), "sledgehammer", consume_status, consume_output)
 
-  def send_provers(): Unit = {
-    val provers = server.options.string("sledgehammer_provers")
-    server.channel.write(LSP.Sledgehammer_Provers_Response.apply(provers))
-  }
-
   private def consume_status(status: Query_Operation.Status): Unit = {
     val message =
       status match {
@@ -35,6 +30,10 @@
     server.channel.write(LSP.Sledgehammer_Output(content))
   }
 
+  def provers(): Unit =
+    server.channel.write(
+      LSP.Sledgehammer_Provers_Response(server.options.string("sledgehammer_provers")))
+
   def request(args: List[String]): Unit =
     server.editor.send_dispatcher { query_operation.apply_query(args) }
 
@@ -51,6 +50,7 @@
 
   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()
 }