proper treatment of startup errors, notably for Pure ROOT.ML;
authorwenzelm
Thu, 02 Apr 2020 20:37:11 +0200
changeset 71668 25ef5c7287a7
parent 71667 4d2de35214c5
child 71669 12ebd8d0deee
proper treatment of startup errors, notably for Pure ROOT.ML;
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 =