src/Pure/Concurrent/simple_thread.ML
changeset 59468 fe6651760643
parent 59055 5a7157b8e870
child 60764 b610ba36e02c
equal deleted inserted replaced
59467:58c4f3e1870f 59468:fe6651760643
     5 *)
     5 *)
     6 
     6 
     7 signature SIMPLE_THREAD =
     7 signature SIMPLE_THREAD =
     8 sig
     8 sig
     9   val is_self: Thread.thread -> bool
     9   val is_self: Thread.thread -> bool
    10   val attributes: bool -> Thread.threadAttribute list
    10   type params = {stack_limit: int option, interrupts: bool}
    11   val fork: bool -> (unit -> unit) -> Thread.thread
    11   val attributes: params -> Thread.threadAttribute list
       
    12   val fork: params -> (unit -> unit) -> Thread.thread
    12   val join: Thread.thread -> unit
    13   val join: Thread.thread -> unit
    13   val interrupt_unsynchronized: Thread.thread -> unit
    14   val interrupt_unsynchronized: Thread.thread -> unit
    14 end;
    15 end;
    15 
    16 
    16 structure Simple_Thread: SIMPLE_THREAD =
    17 structure Simple_Thread: SIMPLE_THREAD =
    17 struct
    18 struct
    18 
    19 
    19 fun is_self thread = Thread.equal (Thread.self (), thread);
    20 fun is_self thread = Thread.equal (Thread.self (), thread);
    20 
    21 
    21 fun attributes interrupts =
    22 type params = {stack_limit: int option, interrupts: bool};
    22   if interrupts then Multithreading.public_interrupts else Multithreading.no_interrupts;
       
    23 
    23 
    24 fun fork interrupts body =
    24 fun attributes {stack_limit, interrupts} =
       
    25   maximum_ml_stack stack_limit @
       
    26   (if interrupts then Multithreading.public_interrupts else Multithreading.no_interrupts);
       
    27 
       
    28 fun fork params body =
    25   Thread.fork (fn () =>
    29   Thread.fork (fn () =>
    26     print_exception_trace General.exnMessage tracing (fn () =>
    30     print_exception_trace General.exnMessage tracing (fn () =>
    27       body () handle exn => if Exn.is_interrupt exn then () (*sic!*) else reraise exn),
    31       body () handle exn => if Exn.is_interrupt exn then () (*sic!*) else reraise exn),
    28     attributes interrupts);
    32     attributes params);
    29 
    33 
    30 fun join thread =
    34 fun join thread =
    31   while Thread.isActive thread
    35   while Thread.isActive thread
    32   do OS.Process.sleep (seconds 0.1);
    36   do OS.Process.sleep (seconds 0.1);
    33 
    37