--- a/src/Pure/Tools/server.scala Thu Mar 15 16:16:19 2018 +0100
+++ b/src/Pure/Tools/server.scala Thu Mar 15 21:26:39 2018 +0100
@@ -72,6 +72,16 @@
{ case (context, Server_Commands.Session_Build(args)) =>
context.make_task(task =>
Server_Commands.Session_Build.command(task.progress, args)._1)
+ },
+ "session_start" ->
+ { case (context, Server_Commands.Session_Start(args)) =>
+ context.make_task(task =>
+ {
+ val (res, session_id, session) =
+ Server_Commands.Session_Start.command(task.progress, args, log = context.logger())
+ // FIXME store session in context
+ res
+ })
})
def unapply(name: String): Option[T] = table.get(name)