asynchronous "session_build";
authorwenzelm
Wed, 14 Mar 2018 20:29:46 +0100
changeset 67861 cd1cac824ef8
parent 67860 5a6c483269f3
child 67862 20a0e0ea6237
asynchronous "session_build";
src/Pure/Tools/server.scala
src/Pure/Tools/server_commands.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)
--- 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(_))