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