--- 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(_))