equal
deleted
inserted
replaced
253 let |
253 let |
254 val args = decode_args true args_yxml; |
254 val args = decode_args true args_yxml; |
255 fun exec e = |
255 fun exec e = |
256 if can Theory.get_pure () then |
256 if can Theory.get_pure () then |
257 Isabelle_Thread.fork |
257 Isabelle_Thread.fork |
258 {name = "build_session", stack_limit = NONE, interrupts = false} e |
258 {name = "build_session", stack_limit = Isabelle_Thread.stack_limit (), |
|
259 interrupts = false} e |
259 |> ignore |
260 |> ignore |
260 else e (); |
261 else e (); |
261 in |
262 in |
262 exec (fn () => |
263 exec (fn () => |
263 (Future.interruptible_task (fn () => (build_session args; (0, []))) () handle exn => |
264 (Future.interruptible_task (fn () => (build_session args; (0, []))) () handle exn => |