src/Pure/Tools/server.scala
changeset 67869 8cb4fef58379
parent 67867 fb66d099adb2
child 67870 586be47e00b3
--- 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)