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