equal
deleted
inserted
replaced
148 } |
148 } |
149 |
149 |
150 |
150 |
151 /* PIDE protocol handler */ |
151 /* PIDE protocol handler */ |
152 |
152 |
153 class Handler(progress: Progress, session: Session, session_name: String) |
153 private class Protocol_Handler(progress: Progress, session: Session, session_name: String) |
154 extends Session.Protocol_Handler |
154 extends Session.Protocol_Handler |
155 { |
155 { |
156 val build_session_errors: Promise[List[String]] = Future.promise |
156 private val build_session_errors: Promise[List[String]] = Future.promise |
|
157 def build_session_join: List[String] = build_session_errors.join |
157 |
158 |
158 override def exit() { build_session_errors.cancel } |
159 override def exit() { build_session_errors.cancel } |
159 |
160 |
160 private def build_session_finished(msg: Prover.Protocol_Output): Boolean = |
161 private def build_session_finished(msg: Prover.Protocol_Output): Boolean = |
161 { |
162 { |
251 else Nil |
252 else Nil |
252 |
253 |
253 if (options.bool("pide_build")) { |
254 if (options.bool("pide_build")) { |
254 val resources = new Resources(sessions_structure, deps(parent)) |
255 val resources = new Resources(sessions_structure, deps(parent)) |
255 val session = new Session(options, resources) |
256 val session = new Session(options, resources) |
256 val handler = new Handler(progress, session, session_name) |
257 val handler = new Protocol_Handler(progress, session, session_name) |
257 session.init_protocol_handler(handler) |
258 session.init_protocol_handler(handler) |
258 |
259 |
259 val stdout = new StringBuilder(1000) |
260 val stdout = new StringBuilder(1000) |
260 val messages = new mutable.ListBuffer[String] |
261 val messages = new mutable.ListBuffer[String] |
261 val command_timings = new mutable.ListBuffer[Properties.T] |
262 val command_timings = new mutable.ListBuffer[Properties.T] |
297 |
298 |
298 val errors = |
299 val errors = |
299 Exn.capture { process.await_startup } match { |
300 Exn.capture { process.await_startup } match { |
300 case Exn.Res(_) => |
301 case Exn.Res(_) => |
301 session.protocol_command("build_session", args_yxml) |
302 session.protocol_command("build_session", args_yxml) |
302 handler.build_session_errors.join |
303 handler.build_session_join |
303 case Exn.Exn(exn) => List(Exn.message(exn)) |
304 case Exn.Exn(exn) => List(Exn.message(exn)) |
304 } |
305 } |
305 |
306 |
306 val process_result = process.await_shutdown |
307 val process_result = process.await_shutdown |
307 val process_output = |
308 val process_output = |