equal
deleted
inserted
replaced
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 let |
20 let |
21 val _ = |
21 val _ = |
22 Output.error_msg (ML_Compiler.exn_message exn) |
22 ML_Compiler.exn_error_message exn |
23 handle _ => Output.error_msg "Exception raised, but failed to print details!"; |
23 handle _ => Output.error_message "Exception raised, but failed to print details!"; |
24 in if Exn.is_interrupt exn then 130 else 1 end; |
24 in if Exn.is_interrupt exn then 130 else 1 end; |
25 in if rc = 0 then () else exit rc end) (); |
25 in if rc = 0 then () else exit rc end) (); |
26 |
26 |
27 fun tool0 body = tool (fn () => (body (); 0)); |
27 fun tool0 body = tool (fn () => (body (); 0)); |
28 |
28 |