equal
deleted
inserted
replaced
48 |
48 |
49 type params = {name: string, stack_limit: int option, interrupts: bool}; |
49 type params = {name: string, stack_limit: int option, interrupts: bool}; |
50 |
50 |
51 fun attributes ({stack_limit, interrupts, ...}: params) = |
51 fun attributes ({stack_limit, interrupts, ...}: params) = |
52 Thread.MaximumMLStack stack_limit :: |
52 Thread.MaximumMLStack stack_limit :: |
53 (if interrupts then Thread_Attributes.public_interrupts else Thread_Attributes.no_interrupts); |
53 Thread_Attributes.convert_attributes |
|
54 (if interrupts then Thread_Attributes.public_interrupts else Thread_Attributes.no_interrupts); |
54 |
55 |
55 fun fork (params: params) body = |
56 fun fork (params: params) body = |
56 Thread.fork (fn () => |
57 Thread.fork (fn () => |
57 Exn.trace General.exnMessage tracing (fn () => |
58 Exn.trace General.exnMessage tracing (fn () => |
58 (set_name (#name params); body ()) |
59 (set_name (#name params); body ()) |