--- a/src/Pure/Tools/server.scala Fri Mar 16 22:50:56 2018 +0100
+++ b/src/Pure/Tools/server.scala Sat Mar 17 15:10:50 2018 +0100
@@ -71,7 +71,7 @@
"session_build" ->
{ case (context, Server_Commands.Session_Build(args)) =>
context.make_task(task =>
- Server_Commands.Session_Build.command(task.progress, args)._1)
+ Server_Commands.Session_Build.command(args, progress = task.progress)._1)
},
"session_start" ->
{ case (context, Server_Commands.Session_Start(args)) =>
@@ -79,7 +79,7 @@
{
val (res, entry) =
Server_Commands.Session_Start.command(
- task.progress, args, log = context.server.log)
+ args, progress = task.progress, log = context.server.log)
context.server.add_session(entry)
res
})
--- a/src/Pure/Tools/server_commands.scala Fri Mar 16 22:50:56 2018 +0100
+++ b/src/Pure/Tools/server_commands.scala Sat Mar 17 15:10:50 2018 +0100
@@ -56,7 +56,7 @@
required_session = required_session, system_mode = system_mode, verbose = verbose)
}
- def command(progress: Progress, args: Args)
+ def command(args: Args, progress: Progress = No_Progress)
: (JSON.Object.T, Build.Results, Sessions.Base_Info) =
{
val options = Options.init(prefs = args.preferences, opts = args.options)
@@ -116,10 +116,10 @@
}
yield Args(build = build, print_mode = print_mode)
- def command(progress: Progress, args: Args, log: Logger = No_Logger)
+ def command(args: Args, progress: Progress = No_Progress, log: Logger = No_Logger)
: (JSON.Object.T, (UUID, Thy_Resources.Session)) =
{
- val base_info = Session_Build.command(progress, args.build)._3
+ val base_info = Session_Build.command(args.build, progress = progress)._3
val session =
Thy_Resources.start_session(