equal
deleted
inserted
replaced
26 Thread.fork |
26 Thread.fork |
27 (fn () => |
27 (fn () => |
28 Runtime.debugging NONE body () handle exn => |
28 Runtime.debugging NONE body () handle exn => |
29 if Exn.is_interrupt exn then () |
29 if Exn.is_interrupt exn then () |
30 else writeln ("## INTERNAL ERROR ##\n" ^ Runtime.exn_message exn), |
30 else writeln ("## INTERNAL ERROR ##\n" ^ Runtime.exn_message exn), |
31 Simple_Thread.attributes interrupts); |
31 Simple_Thread.attributes {stack_limit = NONE, interrupts = interrupts}); |
32 |
32 |
33 val message_store_limit = 20 |
33 val message_store_limit = 20 |
34 val message_display_limit = 10 |
34 val message_display_limit = 10 |
35 |
35 |
36 fun implode_message (workers, work) = |
36 fun implode_message (workers, work) = |