equal
deleted
inserted
replaced
15 |
15 |
16 fun tool body = |
16 fun tool body = |
17 uninterruptible (fn restore_attributes => fn () => |
17 uninterruptible (fn restore_attributes => fn () => |
18 let val rc = |
18 let val rc = |
19 restore_attributes body () handle exn => |
19 restore_attributes body () handle exn => |
20 (Output.error_msg (ML_Compiler.exn_message exn); if Exn.is_interrupt exn then 130 else 1); |
20 let |
|
21 val _ = |
|
22 Output.error_msg (ML_Compiler.exn_message exn) |
|
23 handle _ => Output.error_msg "Exception raised, but failed to print details!"; |
|
24 in if Exn.is_interrupt exn then 130 else 1 end; |
21 in if rc = 0 then () else exit rc end) (); |
25 in if rc = 0 then () else exit rc end) (); |
22 |
26 |
23 fun tool0 body = tool (fn () => (body (); 0)); |
27 fun tool0 body = tool (fn () => (body (); 0)); |
24 |
28 |
25 end; |
29 end; |