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 Thread_Attributes.convert_attributes |
|
54 (if interrupts then Thread_Attributes.public_interrupts else Thread_Attributes.no_interrupts); |
|
55 |
|
56 fun fork (params: params) body = |
|
57 Thread.fork (fn () => |
|
58 Exn.trace General.exnMessage tracing (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 |
|
66 fun join thread = |
|
67 while Thread.isActive thread |
|
68 do OS.Process.sleep (seconds 0.1); |
|
69 |
|
70 |
|
71 (* interrupt *) |
|
72 |
|
73 fun interrupt_unsynchronized thread = |
|
74 Thread.interrupt thread handle Thread _ => (); |
|
75 |
|
76 end; |
|