# 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 =