src/Pure/PIDE/protocol.scala

 
 trait Protocol
 {
   /* 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
 
 
   /* options */
 

 
 
   /* 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)
   {
     val blobs_yxml =
     {

       import XML.Encode._
       val encode_tok: T[Token] = (tok => pair(int, int)((tok.kind.id, Symbol.length(tok.source))))
       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)))
   }
 
 
   /* execution */
 

               (bool_atom(a) :: b.commands.map(cmd => long_atom(cmd.id)),
                 list(pair(id, pair(string, list(string))))(c.dest)) }))
       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])
   {
     val versions_yxml =