clarified signature: more concise args;

--- a/src/Tools/VSCode/src/language_server.scala	Sat Nov 01 17:30:43 2025 +0100
+++ b/src/Tools/VSCode/src/language_server.scala	Sat Nov 01 17:54:44 2025 +0100
@@ -539,8 +539,7 @@
           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_Request(provers, isar, try0) =>
-            sledgehammer.handle_request(provers, isar, try0)
+          case LSP.Sledgehammer_Request(args) => sledgehammer.request(args)
           case LSP.Sledgehammer_Cancel() => sledgehammer.cancel()
           case LSP.Sledgehammer_Locate() => sledgehammer.locate()
           case LSP.Sledgehammer_Insert() => sledgehammer.insert()

--- a/src/Tools/VSCode/src/lsp.scala	Sat Nov 01 17:30:43 2025 +0100
+++ b/src/Tools/VSCode/src/lsp.scala	Sat Nov 01 17:54:44 2025 +0100
@@ -804,14 +804,14 @@
   }
 
   object Sledgehammer_Request {
-    def unapply(json: JSON.T): Option[(String, Boolean, Boolean)] =
+    def unapply(json: JSON.T): Option[List[String]] =
       json match {
         case Notification("PIDE/sledgehammer_request", Some(params)) =>
           for {
             provers <- JSON.string(params, "provers")
             isar <- JSON.bool(params, "isar")
             try0 <- JSON.bool(params, "try0")
-          } yield (provers, isar, try0)
+          } yield List(provers, isar.toString, try0.toString)
         case _ => None
       }
   }

--- a/src/Tools/VSCode/src/vscode_sledgehammer.scala	Sat Nov 01 17:30:43 2025 +0100
+++ b/src/Tools/VSCode/src/vscode_sledgehammer.scala	Sat Nov 01 17:54:44 2025 +0100
@@ -22,11 +22,6 @@
     server.channel.write(LSP.Sledgehammer_Provers_Response.apply(provers))
   }
 
-  def handle_request(provers: String, isar: Boolean, try0: Boolean): Unit =
-    server.editor.send_dispatcher {
-      query_operation.apply_query(List(provers, isar.toString, try0.toString))
-    }
-
   private def consume_status(status: Query_Operation.Status): Unit = {
     val msg =
       status match {
@@ -158,6 +153,9 @@
     }
   }
 
+  def request(args: List[String]): Unit =
+    server.editor.send_dispatcher { query_operation.apply_query(args) }
+
   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()