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