39 } |
39 } |
40 } |
40 } |
41 |
41 |
42 class Isabelle_Process private(session: Session, channel: System_Channel, process: Bash.Process) |
42 class Isabelle_Process private(session: Session, channel: System_Channel, process: Bash.Process) |
43 { |
43 { |
44 private val startup_error = Future.promise[String] |
44 private val startup = Future.promise[String] |
|
45 private val terminated = Future.promise[Process_Result] |
45 |
46 |
46 session.phase_changed += |
47 session.phase_changed += |
47 Session.Consumer(getClass.getName) { |
48 Session.Consumer(getClass.getName) { |
48 case Session.Ready => |
49 case Session.Ready => |
49 startup_error.fulfill("") |
50 startup.fulfill("") |
50 case Session.Terminated(result) if !result.ok && !startup_error.is_finished => |
51 case Session.Terminated(result) => |
51 val syslog = session.syslog_content() |
52 if (!result.ok && !startup.is_finished) { |
52 val err = "Session startup failed" + (if (syslog.isEmpty) "" else ":\n" + syslog) |
53 val syslog = session.syslog_content() |
53 startup_error.fulfill(err) |
54 val err = "Session startup failed" + (if (syslog.isEmpty) "" else ":\n" + syslog) |
|
55 startup.fulfill(err) |
|
56 } |
|
57 terminated.fulfill(result) |
54 case _ => |
58 case _ => |
55 } |
59 } |
56 |
60 |
57 def startup_join(): Unit = |
61 session.start(receiver => new Prover(receiver, session.xml_cache, channel, process)) |
58 startup_error.join match { |
62 |
59 case "" => |
63 def await_startup(): Isabelle_Process = |
60 case msg => session.stop(); error(msg) |
64 startup.join match { |
|
65 case "" => this |
|
66 case err => session.stop(); error(err) |
61 } |
67 } |
62 |
68 |
63 session.start(receiver => new Prover(receiver, session.xml_cache, channel, process)) |
69 def join(): Process_Result = terminated.join |
64 } |
70 } |