--- a/src/Pure/PIDE/session.scala Sat Feb 13 20:01:48 2016 +0100
+++ b/src/Pure/PIDE/session.scala Sat Feb 13 20:41:56 2016 +0100
@@ -212,7 +212,7 @@
/* internal messages */
- private case class Start(name: String, args: List[String])
+ private case class Start(name: String, args: String)
private case object Stop
private case class Cancel_Exec(exec_id: Document_ID.Exec)
private case class Protocol_Command(name: String, args: List[String])
@@ -601,7 +601,7 @@
pending_edits: List[Text.Edit] = Nil): Document.Snapshot =
global_state.value.snapshot(name, pending_edits)
- def start(name: String, args: List[String])
+ def start(name: String, args: String)
{ manager.send(Start(name, args)) }
def stop()