# HG changeset patch
# User wenzelm
# Date 1585852631 -7200
# Node ID 25ef5c7287a76b16569e4a5ac96f05e71e5eac57
# Parent  4d2de35214c51f9563ced83336be67dd337c340c
proper treatment of startup errors, notably for Pure ROOT.ML;

diff -r 4d2de35214c5 -r 25ef5c7287a7 src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Thu Apr 02 20:06:43 2020 +0200
+++ b/src/Pure/Tools/build.scala	Thu Apr 02 20:37:11 2020 +0200
@@ -293,10 +293,15 @@
             Isabelle_Process(session, options, sessions_structure, store,
               logic = parent, raw_ml_system = is_pure,
               use_prelude = use_prelude, eval_main = eval_main,
-              cwd = info.dir.file, env = env).await_startup
+              cwd = info.dir.file, env = env)
 
-          session.protocol_command("build_session", args_yxml)
-          val errors = handler.build_session_errors.join
+          val errors =
+            Exn.capture { process.await_startup } match {
+              case Exn.Res(_) =>
+                session.protocol_command("build_session", args_yxml)
+                handler.build_session_errors.join
+              case Exn.Exn(exn) => List(Exn.message(exn))
+            }
 
           val process_result = process.await_shutdown
           val process_output =