equal
deleted
inserted
replaced
100 then Theory.install_pure (Thy_Info.get_theory Context.PureN) else (); |
100 then Theory.install_pure (Thy_Info.get_theory Context.PureN) else (); |
101 in () end; |
101 in () end; |
102 |
102 |
103 fun exec e = |
103 fun exec e = |
104 if can Theory.get_pure () then |
104 if can Theory.get_pure () then |
105 Isabelle_Thread.fork |
105 Isabelle_Thread.fork (Isabelle_Thread.params "build_session") e |
106 {name = "build_session", stack_limit = Isabelle_Thread.stack_limit (), |
|
107 interrupts = false} e |
|
108 |> ignore |
106 |> ignore |
109 else e (); |
107 else e (); |
110 in |
108 in |
111 exec (fn () => |
109 exec (fn () => |
112 (case Exn.capture (Future.interruptible_task build) () of |
110 (case Exn.capture (Future.interruptible_task build) () of |