src/Pure/Concurrent/standard_thread.ML
author wenzelm
Wed Apr 06 16:33:33 2016 +0200 (2016-04-06)
changeset 62889 99c7f31615c2
parent 62505 9e2a65912111
child 62923 3a122e1e352a
permissions -rw-r--r--
clarified modules;
tuned signature;
     1 (*  Title:      Pure/Concurrent/standard_thread.ML
     2     Author:     Makarius
     3 
     4 Standard thread operations.
     5 *)
     6 
     7 signature STANDARD_THREAD =
     8 sig
     9   val is_self: Thread.thread -> bool
    10   val get_name: unit -> string option
    11   val the_name: unit -> string
    12   type params = {name: string, stack_limit: int option, interrupts: bool}
    13   val attributes: params -> Thread.threadAttribute list
    14   val fork: params -> (unit -> unit) -> Thread.thread
    15   val join: Thread.thread -> unit
    16   val interrupt_unsynchronized: Thread.thread -> unit
    17 end;
    18 
    19 structure Standard_Thread: STANDARD_THREAD =
    20 struct
    21 
    22 (* self *)
    23 
    24 fun is_self thread = Thread.equal (Thread.self (), thread);
    25 
    26 
    27 (* unique name *)
    28 
    29 local
    30   val name_var = Thread_Data.var () : string Thread_Data.var;
    31   val count = Counter.make ();
    32 in
    33 
    34 fun get_name () = Thread_Data.get name_var;
    35 
    36 fun the_name () =
    37   (case get_name () of
    38     NONE => raise Fail "Unknown thread name"
    39   | SOME name => name);
    40 
    41 fun set_name base =
    42   Thread_Data.put name_var (SOME (base ^ "/" ^ string_of_int (count ())));
    43 
    44 end;
    45 
    46 
    47 (* fork *)
    48 
    49 type params = {name: string, stack_limit: int option, interrupts: bool};
    50 
    51 fun attributes ({stack_limit, interrupts, ...}: params) =
    52   Thread.MaximumMLStack stack_limit ::
    53   (if interrupts then Multithreading.public_interrupts else Multithreading.no_interrupts);
    54 
    55 fun fork (params: params) body =
    56   Thread.fork (fn () =>
    57     Exn.trace General.exnMessage tracing (fn () =>
    58       (set_name (#name params); body ())
    59         handle exn => if Exn.is_interrupt exn then () (*sic!*) else Exn.reraise exn),
    60     attributes params);
    61 
    62 
    63 (* join *)
    64 
    65 fun join thread =
    66   while Thread.isActive thread
    67   do OS.Process.sleep (seconds 0.1);
    68 
    69 
    70 (* interrupt *)
    71 
    72 fun interrupt_unsynchronized thread =
    73   Thread.interrupt thread handle Thread _ => ();
    74 
    75 end;