# HG changeset patch
# User wenzelm
# Date 1521055786 -3600
# Node ID cd1cac824ef87224fab3b85194a12db1910a19e4
# Parent  5a6c483269f39fa63e2712ae27150223aefc82a1
asynchronous "session_build";

diff -r 5a6c483269f3 -r cd1cac824ef8 src/Pure/Tools/server.scala
--- a/src/Pure/Tools/server.scala	Wed Mar 14 20:20:10 2018 +0100
+++ b/src/Pure/Tools/server.scala	Wed Mar 14 20:29:46 2018 +0100
@@ -70,7 +70,8 @@
         "cancel" -> { case (context, JSON.Value.String(id)) => context.cancel_task(id) },
         "session_build" ->
           { case (context, Server_Commands.Session_Build(args)) =>
-             Server_Commands.Session_Build.command(context.progress(), args)._1
+              context.make_task(task =>
+                Server_Commands.Session_Build.command(task.progress, args)._1)
           })
 
     def unapply(name: String): Option[T] = table.get(name)
diff -r 5a6c483269f3 -r cd1cac824ef8 src/Pure/Tools/server_commands.scala
--- a/src/Pure/Tools/server_commands.scala	Wed Mar 14 20:20:10 2018 +0100
+++ b/src/Pure/Tools/server_commands.scala	Wed Mar 14 20:29:46 2018 +0100
@@ -42,7 +42,8 @@
           system_mode = system_mode, verbose = verbose)
       }
 
-    def command(progress: Progress, args: Args): (JSON.T, Build.Results, Sessions.Base_Info) =
+    def command(progress: Progress, args: Args)
+      : (JSON.Object.T, Build.Results, Sessions.Base_Info) =
     {
       val options = Options.init(prefs = args.prefs, opts = args.opts)
       val dirs = args.dirs.map(Path.explode(_))