# HG changeset patch
# User wenzelm
# Date 1590322544 -7200
# Node ID fe7ee970c425217cafc53f130a9b2ddabedce5a3
# Parent  3cd8449829fad273e8ec2e9980b9be1a2172975c
clarified build_session protocol;

diff -r 3cd8449829fa -r fe7ee970c425 src/Pure/PIDE/protocol.ML
--- a/src/Pure/PIDE/protocol.ML	Sun May 24 13:39:45 2020 +0200
+++ b/src/Pure/PIDE/protocol.ML	Sun May 24 14:15:44 2020 +0200
@@ -12,6 +12,10 @@
     (fn args => List.app writeln args);
 
 val _ =
+  Isabelle_Process.protocol_command "Prover.stop"
+    (fn [rc] => raise Isabelle_Process.STOP (Value.parse_int rc));
+
+val _ =
   Isabelle_Process.protocol_command "Prover.options"
     (fn [options_yxml] =>
       (Options.set_default (Options.decode (YXML.parse_body options_yxml));
diff -r 3cd8449829fa -r fe7ee970c425 src/Pure/Tools/build.ML
--- a/src/Pure/Tools/build.ML	Sun May 24 13:39:45 2020 +0200
+++ b/src/Pure/Tools/build.ML	Sun May 24 14:15:44 2020 +0200
@@ -247,25 +247,18 @@
 
 (* PIDE version *)
 
-fun build_session_finished errs =
-  XML.Encode.list XML.Encode.string errs
-  |> Output.protocol_message Markup.build_session_finished;
-
 val _ =
   Isabelle_Process.protocol_command "build_session"
     (fn [args_yxml] =>
         let
           val args = decode_args true args_yxml;
-          val errs =
-            Future.interruptible_task (fn () => (build_session args; [])) () handle exn =>
-              (Runtime.exn_message_list exn handle _ (*sic!*) =>
-                (build_session_finished ["CRASHED"];
-                  raise Isabelle_Process.STOP 2));
-          val _ = build_session_finished errs;
+          val (rc, errs) =
+            Future.interruptible_task (fn () => (build_session args; (0, []))) () handle exn =>
+              ((1, Runtime.exn_message_list exn) handle _ (*sic!*) => (2, ["CRASHED"]));
         in
-          if null errs
-          then raise Isabelle_Process.STOP 0
-          else raise Isabelle_Process.STOP 1
+          (rc, errs)
+          |> let open XML.Encode in pair int (list string) end
+          |> Output.protocol_message Markup.build_session_finished
         end
       | _ => raise Match);
 
diff -r 3cd8449829fa -r fe7ee970c425 src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Sun May 24 13:39:45 2020 +0200
+++ b/src/Pure/Tools/build.scala	Sun May 24 14:15:44 2020 +0200
@@ -234,15 +234,23 @@
 
               private def build_session_finished(msg: Prover.Protocol_Output): Boolean =
               {
-                val errors =
+                val (rc, errors) =
                   try {
-                    for (err <- XML.Decode.list(x => x)(Symbol.decode_yxml(msg.text)))
-                    yield {
-                      val prt = Protocol_Message.expose_no_reports(err)
-                      Pretty.string_of(prt, metric = Symbol.Metric)
+                    val (rc, errs) =
+                    {
+                      import XML.Decode._
+                      pair(int, list(x => x))(Symbol.decode_yxml(msg.text))
                     }
+                    val errors =
+                      for (err <- errs) yield {
+                        val prt = Protocol_Message.expose_no_reports(err)
+                        Pretty.string_of(prt, metric = Symbol.Metric)
+                      }
+                    (rc, errors)
                   }
-                  catch { case ERROR(err) => List(err) }
+                  catch { case ERROR(err) => (2, List(err)) }
+
+                session.protocol_command("Prover.stop", rc.toString)
                 build_session_errors.fulfill(errors)
                 true
               }