--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Concurrent/isabelle_thread.ML Sun Apr 05 13:05:40 2020 +0200
@@ -0,0 +1,76 @@
+(* Title: Pure/Concurrent/isabelle_thread.ML
+ Author: Makarius
+
+Isabelle-specific thread management.
+*)
+
+signature ISABELLE_THREAD =
+sig
+ val is_self: Thread.thread -> bool
+ val get_name: unit -> string option
+ val the_name: unit -> string
+ type params = {name: string, stack_limit: int option, interrupts: bool}
+ val attributes: params -> Thread.threadAttribute list
+ val fork: params -> (unit -> unit) -> Thread.thread
+ val join: Thread.thread -> unit
+ val interrupt_unsynchronized: Thread.thread -> unit
+end;
+
+structure Isabelle_Thread: ISABELLE_THREAD =
+struct
+
+(* self *)
+
+fun is_self thread = Thread.equal (Thread.self (), thread);
+
+
+(* unique name *)
+
+local
+ val name_var = Thread_Data.var () : string Thread_Data.var;
+ val count = Counter.make ();
+in
+
+fun get_name () = Thread_Data.get name_var;
+
+fun the_name () =
+ (case get_name () of
+ NONE => raise Fail "Unknown thread name"
+ | SOME name => name);
+
+fun set_name base =
+ Thread_Data.put name_var (SOME (base ^ "/" ^ string_of_int (count ())));
+
+end;
+
+
+(* fork *)
+
+type params = {name: string, stack_limit: int option, interrupts: bool};
+
+fun attributes ({stack_limit, interrupts, ...}: params) =
+ Thread.MaximumMLStack stack_limit ::
+ Thread_Attributes.convert_attributes
+ (if interrupts then Thread_Attributes.public_interrupts else Thread_Attributes.no_interrupts);
+
+fun fork (params: params) body =
+ Thread.fork (fn () =>
+ Exn.trace General.exnMessage tracing (fn () =>
+ (set_name (#name params); body ())
+ handle exn => if Exn.is_interrupt exn then () (*sic!*) else Exn.reraise exn),
+ attributes params);
+
+
+(* join *)
+
+fun join thread =
+ while Thread.isActive thread
+ do OS.Process.sleep (seconds 0.1);
+
+
+(* interrupt *)
+
+fun interrupt_unsynchronized thread =
+ Thread.interrupt thread handle Thread _ => ();
+
+end;