# HG changeset patch
# User wenzelm
# Date 1585400505 -3600
# Node ID d97f504c8145bf8ec96e77c7f9204fe135128e42
# Parent  b3b0d87edd20e0f74f55ff9568a5ebdb39567c11
clarified Isabelle_Process phases;

diff -r b3b0d87edd20 -r d97f504c8145 src/Pure/PIDE/headless.scala
--- 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
     }
diff -r b3b0d87edd20 -r d97f504c8145 src/Pure/System/isabelle_process.scala
--- 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
diff -r b3b0d87edd20 -r d97f504c8145 src/Pure/Tools/build.scala
--- 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 =>
diff -r b3b0d87edd20 -r d97f504c8145 src/Tools/VSCode/src/server.scala
--- 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) }