# HG changeset patch
# User wenzelm
# Date 1590324448 -7200
# Node ID 0ca3535217530c90b498c61488b1342a2209dea7
# Parent  fe7ee970c425217cafc53f130a9b2ddabedce5a3
asynchronous build_session: notably for Scala.fulfill protocol commands during run;

diff -r fe7ee970c425 -r 0ca353521753 src/Pure/Tools/build.ML
--- a/src/Pure/Tools/build.ML	Sun May 24 14:15:44 2020 +0200
+++ b/src/Pure/Tools/build.ML	Sun May 24 14:47:28 2020 +0200
@@ -252,13 +252,18 @@
     (fn [args_yxml] =>
         let
           val args = decode_args true args_yxml;
-          val (rc, errs) =
-            Future.interruptible_task (fn () => (build_session args; (0, []))) () handle exn =>
-              ((1, Runtime.exn_message_list exn) handle _ (*sic!*) => (2, ["CRASHED"]));
+          fun exec e =
+            if can Theory.get_pure () then
+              Isabelle_Thread.fork
+                {name = "build_session", stack_limit = NONE, interrupts = false} e
+              |> ignore
+            else e ();
         in
-          (rc, errs)
+          exec (fn () =>
+            (Future.interruptible_task (fn () => (build_session args; (0, []))) () handle exn =>
+              ((1, Runtime.exn_message_list exn) handle _ (*sic!*) => (2, ["CRASHED"])))
           |> let open XML.Encode in pair int (list string) end
-          |> Output.protocol_message Markup.build_session_finished
+          |> Output.protocol_message Markup.build_session_finished)
         end
       | _ => raise Match);