equal
deleted
inserted
replaced
44 Args(session, preferences = preferences, options = options, dirs = dirs, |
44 Args(session, preferences = preferences, options = options, dirs = dirs, |
45 include_sessions = include_sessions, verbose = verbose) |
45 include_sessions = include_sessions, verbose = verbose) |
46 } |
46 } |
47 |
47 |
48 def command(args: Args, progress: Progress = No_Progress) |
48 def command(args: Args, progress: Progress = No_Progress) |
49 : (JSON.Object.T, Build.Results, Sessions.Base_Info) = |
49 : (JSON.Object.T, Build.Results, Options, Sessions.Base_Info) = |
50 { |
50 { |
51 val options = Options.init(prefs = args.preferences, opts = args.options) |
51 val options = Options.init(prefs = args.preferences, opts = args.options) |
52 val dirs = args.dirs.map(Path.explode(_)) |
52 val dirs = args.dirs.map(Path.explode(_)) |
53 |
53 |
54 val base_info = |
54 val base_info = |
83 "return_code" -> result.rc, |
83 "return_code" -> result.rc, |
84 "timeout" -> result.timeout, |
84 "timeout" -> result.timeout, |
85 "timing" -> result.timing.json) |
85 "timing" -> result.timing.json) |
86 })) |
86 })) |
87 |
87 |
88 if (results.ok) (results_json, results, base_info) |
88 if (results.ok) (results_json, results, options, base_info) |
89 else throw new Server.Error("Session build failed: return code " + results.rc, results_json) |
89 else throw new Server.Error("Session build failed: return code " + results.rc, results_json) |
90 } |
90 } |
91 } |
91 } |
92 |
92 |
93 object Session_Start |
93 object Session_Start |
104 yield Args(build = build, print_mode = print_mode) |
104 yield Args(build = build, print_mode = print_mode) |
105 |
105 |
106 def command(args: Args, progress: Progress = No_Progress, log: Logger = No_Logger) |
106 def command(args: Args, progress: Progress = No_Progress, log: Logger = No_Logger) |
107 : (JSON.Object.T, (UUID.T, Headless.Session)) = |
107 : (JSON.Object.T, (UUID.T, Headless.Session)) = |
108 { |
108 { |
109 val base_info = |
109 val (_, _, options, base_info) = |
110 try { Session_Build.command(args.build, progress = progress)._3 } |
110 try { Session_Build.command(args.build, progress = progress) } |
111 catch { case exn: Server.Error => error(exn.message) } |
111 catch { case exn: Server.Error => error(exn.message) } |
112 |
112 |
113 val resources = Headless.Resources(base_info, log = log) |
113 val resources = Headless.Resources(options, base_info, log = log) |
114 |
114 |
115 val session = resources.start_session(print_mode = args.print_mode, progress = progress) |
115 val session = resources.start_session(print_mode = args.print_mode, progress = progress) |
116 |
116 |
117 val id = UUID.random() |
117 val id = UUID.random() |
118 |
118 |