equal
deleted
inserted
replaced
103 print_mode <- JSON.list_default(json, "print_mode", JSON.Value.String.unapply _) |
103 print_mode <- JSON.list_default(json, "print_mode", JSON.Value.String.unapply _) |
104 } |
104 } |
105 yield Args(build = build, print_mode = print_mode) |
105 yield Args(build = build, print_mode = print_mode) |
106 |
106 |
107 def command(progress: Progress, args: Args, log: Logger = No_Logger) |
107 def command(progress: Progress, args: Args, log: Logger = No_Logger) |
108 : (JSON.Object.T, (String, Session)) = |
108 : (JSON.Object.T, (String, Thy_Resources.Session)) = |
109 { |
109 { |
110 val base_info = Session_Build.command(progress, args.build)._3 |
110 val base_info = Session_Build.command(progress, args.build)._3 |
111 |
111 |
112 val session = |
112 val session = |
113 Thy_Resources.start_session( |
113 Thy_Resources.start_session( |
129 object Session_Stop |
129 object Session_Stop |
130 { |
130 { |
131 def unapply(json: JSON.T): Option[String] = |
131 def unapply(json: JSON.T): Option[String] = |
132 JSON.string(json, "session_id") |
132 JSON.string(json, "session_id") |
133 |
133 |
134 def command(session: Session): (JSON.Object.T, Process_Result) = |
134 def command(session: Thy_Resources.Session): (JSON.Object.T, Process_Result) = |
135 { |
135 { |
136 val result = session.stop() |
136 val result = session.stop() |
137 val result_json = JSON.Object("return_code" -> result.rc) |
137 val result_json = JSON.Object("return_code" -> result.rc) |
138 |
138 |
139 if (result.ok) (result_json, result) |
139 if (result.ok) (result_json, result) |