src/Pure/Tools/build.ML
changeset 71880 0ca353521753
parent 71879 fe7ee970c425
child 71884 2bf0283fc975
     1.1 --- a/src/Pure/Tools/build.ML	Sun May 24 14:15:44 2020 +0200
     1.2 +++ b/src/Pure/Tools/build.ML	Sun May 24 14:47:28 2020 +0200
     1.3 @@ -252,13 +252,18 @@
     1.4      (fn [args_yxml] =>
     1.5          let
     1.6            val args = decode_args true args_yxml;
     1.7 -          val (rc, errs) =
     1.8 -            Future.interruptible_task (fn () => (build_session args; (0, []))) () handle exn =>
     1.9 -              ((1, Runtime.exn_message_list exn) handle _ (*sic!*) => (2, ["CRASHED"]));
    1.10 +          fun exec e =
    1.11 +            if can Theory.get_pure () then
    1.12 +              Isabelle_Thread.fork
    1.13 +                {name = "build_session", stack_limit = NONE, interrupts = false} e
    1.14 +              |> ignore
    1.15 +            else e ();
    1.16          in
    1.17 -          (rc, errs)
    1.18 +          exec (fn () =>
    1.19 +            (Future.interruptible_task (fn () => (build_session args; (0, []))) () handle exn =>
    1.20 +              ((1, Runtime.exn_message_list exn) handle _ (*sic!*) => (2, ["CRASHED"])))
    1.21            |> let open XML.Encode in pair int (list string) end
    1.22 -          |> Output.protocol_message Markup.build_session_finished
    1.23 +          |> Output.protocol_message Markup.build_session_finished)
    1.24          end
    1.25        | _ => raise Match);
    1.26