equal
deleted
inserted
replaced
234 (* future job: fill result *) |
234 (* future job: fill result *) |
235 |
235 |
236 fun future_job group (e: unit -> 'a) = |
236 fun future_job group (e: unit -> 'a) = |
237 let |
237 let |
238 val result = ref (NONE: 'a Exn.result option); |
238 val result = ref (NONE: 'a Exn.result option); |
239 val job = Multithreading.with_attributes (Thread.getAttributes ()) |
239 val job = Multithreading.with_attributes Multithreading.restricted_interrupts |
240 (fn _ => fn ok => |
240 (fn _ => fn ok => |
241 let |
241 let |
242 val res = if ok then Exn.capture e () else Exn.Exn Exn.Interrupt; |
242 val res = if ok then Exn.capture e () else Exn.Exn Exn.Interrupt; |
243 val _ = result := SOME res; |
243 val _ = result := SOME res; |
244 val res_ok = |
244 val res_ok = |