src/Pure/Tools/build.scala

           for (err <- XML.Decode.list(x => x)(Symbol.decode_yxml(msg.text))) yield
             Pretty.string_of(Protocol_Message.expose_no_reports(err), metric = Symbol.Metric)
         }
         catch { case ERROR(err) => List(err) }
       build_session_errors.fulfill(errors)
-      session.send_stop()
       true
     }
 
     private def loading_theory(msg: Prover.Protocol_Output): Boolean =
       msg.properties match {

               logic = parent, raw_ml_system = is_pure,
               use_prelude = use_prelude, eval_main = eval_main,
               cwd = info.dir.file, env = env).await_startup
 
           session.protocol_command("build_session", args_yxml)
-
-          val process_result = process.join
+          val errors = handler.build_session_errors.join
+
+          val process_result = process.await_shutdown
           val process_output =
             stdout.toString :: messages.toList :::
             command_timings.toList.map(Protocol.Command_Timing_Marker.apply) :::
             theory_timings.toList.map(Protocol.Theory_Timing_Marker.apply) :::
             runtime_statistics.toList.map(Protocol.ML_Statistics_Marker.apply) :::
             task_statistics.toList.map(Protocol.Task_Statistics_Marker.apply)
 
           val result = process_result.output(process_output)
-          handler.build_session_errors.join match {
-            case Nil => result
-            case errors =>
-              result.error_rc.output(
-                errors.flatMap(s => split_lines(Output.error_message_text(s))) :::
-                errors.map(Protocol.Error_Message_Marker.apply))
+          if (errors.isEmpty) result
+          else {
+            result.error_rc.output(
+              errors.flatMap(s => split_lines(Output.error_message_text(s))) :::
+              errors.map(Protocol.Error_Message_Marker.apply))
           }
         }
         else {
           val args_file = Isabelle_System.tmp_file("build")
           File.write(args_file, args_yxml)