--- a/src/Pure/PIDE/headless.scala Sat Mar 28 13:40:55 2020 +0100
+++ b/src/Pure/PIDE/headless.scala Sat Mar 28 14:01:45 2020 +0100
@@ -573,7 +573,7 @@
progress.echo("Starting session " + session_base_info.session + " ...")
Isabelle_Process(session, options, session_base_info.sessions_structure, store,
- logic = session_base_info.session, modes = print_mode).startup_join()
+ logic = session_base_info.session, modes = print_mode).await_startup
session
}
--- a/src/Pure/System/isabelle_process.scala Sat Mar 28 13:40:55 2020 +0100
+++ b/src/Pure/System/isabelle_process.scala Sat Mar 28 14:01:45 2020 +0100
@@ -41,24 +41,30 @@
class Isabelle_Process private(session: Session, channel: System_Channel, process: Bash.Process)
{
- private val startup_error = Future.promise[String]
+ private val startup = Future.promise[String]
+ private val terminated = Future.promise[Process_Result]
session.phase_changed +=
Session.Consumer(getClass.getName) {
case Session.Ready =>
- startup_error.fulfill("")
- case Session.Terminated(result) if !result.ok && !startup_error.is_finished =>
- val syslog = session.syslog_content()
- val err = "Session startup failed" + (if (syslog.isEmpty) "" else ":\n" + syslog)
- startup_error.fulfill(err)
+ startup.fulfill("")
+ case Session.Terminated(result) =>
+ if (!result.ok && !startup.is_finished) {
+ val syslog = session.syslog_content()
+ val err = "Session startup failed" + (if (syslog.isEmpty) "" else ":\n" + syslog)
+ startup.fulfill(err)
+ }
+ terminated.fulfill(result)
case _ =>
}
- def startup_join(): Unit =
- startup_error.join match {
- case "" =>
- case msg => session.stop(); error(msg)
+ session.start(receiver => new Prover(receiver, session.xml_cache, channel, process))
+
+ def await_startup(): Isabelle_Process =
+ startup.join match {
+ case "" => this
+ case err => session.stop(); error(err)
}
- session.start(receiver => new Prover(receiver, session.xml_cache, channel, process))
+ def join(): Process_Result = terminated.join
}
\ No newline at end of file
--- a/src/Pure/Tools/build.scala Sat Mar 28 13:40:55 2020 +0100
+++ b/src/Pure/Tools/build.scala Sat Mar 28 14:01:45 2020 +0100
@@ -248,17 +248,13 @@
val handler = new Handler(progress, session, name)
session.init_protocol_handler(handler)
- val session_result = Future.promise[Process_Result]
- session.phase_changed += Session.Consumer("build_session")
- {
- case Session.Ready => session.protocol_command("build_session", args_yxml)
- case Session.Terminated(result) => session_result.fulfill(result)
- case _ =>
- }
- Isabelle_Process(session, options, sessions_structure, store,
- logic = parent, cwd = info.dir.file, env = env)
+ val process =
+ Isabelle_Process(session, options, sessions_structure, store,
+ logic = parent, cwd = info.dir.file, env = env).await_startup
- val result = session_result.join
+ session.protocol_command("build_session", args_yxml)
+
+ val result = process.join
handler.result_error.join match {
case "" => result
case msg =>
--- a/src/Tools/VSCode/src/server.scala Sat Mar 28 13:40:55 2020 +0100
+++ b/src/Tools/VSCode/src/server.scala Sat Mar 28 14:01:45 2020 +0100
@@ -305,11 +305,9 @@
dynamic_output.init()
- val process =
+ try {
Isabelle_Process(session, options, base_info.sessions_structure, Sessions.store(options),
- modes = modes, logic = base_info.session)
- try {
- process.startup_join()
+ modes = modes, logic = base_info.session).await_startup
reply_ok("Welcome to Isabelle/" + base_info.session + " (" + Distribution.version + ")")
}
catch { case ERROR(msg) => reply_error(msg) }