more robust build_session protocol: allow prover process to terminate/crash without build_session_finished message;

--- a/src/Pure/Tools/build.scala	Thu Jul 09 11:39:16 2020 +0200
+++ b/src/Pure/Tools/build.scala	Fri Jul 10 21:23:01 2020 +0200
@@ -269,7 +269,8 @@
                   catch { case ERROR(err) => (2, List(err)) }
 
                 session.protocol_command("Prover.stop", rc.toString)
-                build_session_errors.fulfill(errors)
+                try { build_session_errors.fulfill(errors) }
+                catch { case _ : IllegalStateException => }
                 true
               }
 
@@ -314,6 +315,16 @@
                 else if (Protocol.is_exported(message)) {
                   messages += message
                 }
+                else if (msg.is_exit) {
+                  val err =
+                    "Prover terminated" +
+                      (msg.properties match {
+                        case Markup.Process_Result(result) => ": " + result.print_rc
+                        case _ => ""
+                      })
+                  try { build_session_errors.fulfill(List(err)) }
+                  catch { case _ : IllegalStateException => }
+                }
               case _ =>
             }