src/Pure/Tools/build.ML
changeset 71880 0ca353521753
parent 71879 fe7ee970c425
child 71884 2bf0283fc975
equal deleted inserted replaced
71879:fe7ee970c425 71880:0ca353521753
   250 val _ =
   250 val _ =
   251   Isabelle_Process.protocol_command "build_session"
   251   Isabelle_Process.protocol_command "build_session"
   252     (fn [args_yxml] =>
   252     (fn [args_yxml] =>
   253         let
   253         let
   254           val args = decode_args true args_yxml;
   254           val args = decode_args true args_yxml;
   255           val (rc, errs) =
   255           fun exec e =
   256             Future.interruptible_task (fn () => (build_session args; (0, []))) () handle exn =>
   256             if can Theory.get_pure () then
   257               ((1, Runtime.exn_message_list exn) handle _ (*sic!*) => (2, ["CRASHED"]));
   257               Isabelle_Thread.fork
       
   258                 {name = "build_session", stack_limit = NONE, interrupts = false} e
       
   259               |> ignore
       
   260             else e ();
   258         in
   261         in
   259           (rc, errs)
   262           exec (fn () =>
       
   263             (Future.interruptible_task (fn () => (build_session args; (0, []))) () handle exn =>
       
   264               ((1, Runtime.exn_message_list exn) handle _ (*sic!*) => (2, ["CRASHED"])))
   260           |> let open XML.Encode in pair int (list string) end
   265           |> let open XML.Encode in pair int (list string) end
   261           |> Output.protocol_message Markup.build_session_finished
   266           |> Output.protocol_message Markup.build_session_finished)
   262         end
   267         end
   263       | _ => raise Match);
   268       | _ => raise Match);
   264 
   269 
   265 end;
   270 end;