tuned signature;
authorwenzelm
Sat, 17 Mar 2018 15:10:50 +0100
changeset 67886 26510aad2ec6
parent 67885 839a624aabb9
child 67887 a4d5342898b1
tuned signature;
src/Pure/Tools/server.scala
src/Pure/Tools/server_commands.scala
--- 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(