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