# HG changeset patch
# User wenzelm
# Date 1567779079 -7200
# Node ID 9c4809ec28ef7ea290356b1f1e152e070543062c
# Parent  373d95cf1b9808be13ab224d124e9eba6fded6d2
tuned signature;

diff -r 373d95cf1b98 -r 9c4809ec28ef src/Pure/PIDE/protocol.scala
--- a/src/Pure/PIDE/protocol.scala	Fri Sep 06 15:50:57 2019 +0200
+++ b/src/Pure/PIDE/protocol.scala	Fri Sep 06 16:11:19 2019 +0200
@@ -197,7 +197,8 @@
 {
   /* protocol commands */
 
-  def protocol_command_bytes(name: String, args: Bytes*): Unit
+  def protocol_command_raw(name: String, args: List[Bytes]): Unit
+  def protocol_command_args(name: String, args: List[String])
   def protocol_command(name: String, args: String*): Unit
 
 
@@ -242,7 +243,7 @@
   /* interned items */
 
   def define_blob(digest: SHA1.Digest, bytes: Bytes): Unit =
-    protocol_command_bytes("Document.define_blob", Bytes(digest.toString), bytes)
+    protocol_command_raw("Document.define_blob", List(Bytes(digest.toString), bytes))
 
   def define_command(command: Command)
   {
@@ -266,9 +267,9 @@
       Symbol.encode_yxml(list(encode_tok)(toks))
     }
 
-    protocol_command("Document.define_command",
-      (Document_ID(command.id) :: Symbol.encode(command.span.name) :: blobs_yxml :: toks_yxml ::
-        toks.map(tok => Symbol.encode(tok.source))): _*)
+    protocol_command_args("Document.define_command",
+      Document_ID(command.id) :: Symbol.encode(command.span.name) :: blobs_yxml :: toks_yxml ::
+        toks.map(tok => Symbol.encode(tok.source)))
   }
 
 
@@ -314,8 +315,8 @@
       edits.map({ case (name, edit) =>
         Symbol.encode_yxml(pair(string, encode_edit(name))(name.node, edit)) })
     }
-    protocol_command("Document.update",
-      (Document_ID(old_id) :: Document_ID(new_id) :: consolidate_yxml :: edits_yxml): _*)
+    protocol_command_args("Document.update",
+      Document_ID(old_id) :: Document_ID(new_id) :: consolidate_yxml :: edits_yxml)
   }
 
   def remove_versions(versions: List[Document.Version])
diff -r 373d95cf1b98 -r 9c4809ec28ef src/Pure/PIDE/prover.scala
--- a/src/Pure/PIDE/prover.scala	Fri Sep 06 15:50:57 2019 +0200
+++ b/src/Pure/PIDE/prover.scala	Fri Sep 06 16:11:19 2019 +0200
@@ -341,15 +341,18 @@
 
   /** protocol commands **/
 
-  def protocol_command_bytes(name: String, args: Bytes*): Unit =
+  def protocol_command_raw(name: String, args: List[Bytes]): Unit =
     command_input match {
-      case Some(thread) if thread.is_active => thread.send(Bytes(name) :: args.toList)
+      case Some(thread) if thread.is_active => thread.send(Bytes(name) :: args)
       case _ => error("Inactive prover input thread for command " + quote(name))
     }
 
-  def protocol_command(name: String, args: String*)
+  def protocol_command_args(name: String, args: List[String])
   {
-    receiver(new Prover.Input(name, args.toList))
-    protocol_command_bytes(name, args.map(Bytes(_)): _*)
+    receiver(new Prover.Input(name, args))
+    protocol_command_raw(name, args.map(Bytes(_)))
   }
+
+  def protocol_command(name: String, args: String*): Unit =
+    protocol_command_args(name, args.toList)
 }
diff -r 373d95cf1b98 -r 9c4809ec28ef src/Pure/PIDE/session.scala
--- a/src/Pure/PIDE/session.scala	Fri Sep 06 15:50:57 2019 +0200
+++ b/src/Pure/PIDE/session.scala	Fri Sep 06 16:11:19 2019 +0200
@@ -629,7 +629,7 @@
             handle_output(new Prover.Output(Protocol.Dialog_Result(id, serial, result)))
 
           case Protocol_Command(name, args) if prover.defined =>
-            prover.get.protocol_command(name, args:_*)
+            prover.get.protocol_command_args(name, args)
 
           case change: Session.Change if prover.defined =>
             val state = global_state.value