src/Pure/Concurrent/simple_thread.ML
author wenzelm
Thu Oct 09 20:53:17 2008 +0200 (2008-10-09)
changeset 28550 422e9bd169ac
parent 28241 de20fccf6509
child 28577 bd2456e0d944
permissions -rw-r--r--
added fail-safe interrupt;
wenzelm@28241
     1
(*  Title:      Pure/Concurrent/simple_thread.ML
wenzelm@28241
     2
    ID:         $Id$
wenzelm@28241
     3
    Author:     Makarius
wenzelm@28241
     4
wenzelm@28241
     5
Simplified thread fork interface.
wenzelm@28241
     6
*)
wenzelm@28241
     7
wenzelm@28241
     8
signature SIMPLE_THREAD =
wenzelm@28241
     9
sig
wenzelm@28241
    10
  val fork: bool -> (unit -> unit) -> Thread.thread
wenzelm@28550
    11
  val interrupt: Thread.thread -> unit
wenzelm@28241
    12
end;
wenzelm@28241
    13
wenzelm@28241
    14
structure SimpleThread: SIMPLE_THREAD =
wenzelm@28241
    15
struct
wenzelm@28241
    16
wenzelm@28241
    17
fun fork interrupts body =
wenzelm@28241
    18
  Thread.fork (fn () => exception_trace (fn () => body ()),
wenzelm@28241
    19
    if interrupts then Multithreading.regular_interrupts else Multithreading.no_interrupts);
wenzelm@28241
    20
wenzelm@28550
    21
fun interrupt thread = Thread.interrupt thread handle Thread _ => ();
wenzelm@28550
    22
wenzelm@28241
    23
end;