src/Pure/Concurrent/simple_thread.ML
author wenzelm
Mon Oct 13 15:48:39 2008 +0200 (2008-10-13)
changeset 28577 bd2456e0d944
parent 28550 422e9bd169ac
child 29564 f8b933a62151
permissions -rw-r--r--
added generic combinator for synchronized evaluation (formerly in future.ML);
wenzelm@28241
     1
(*  Title:      Pure/Concurrent/simple_thread.ML
wenzelm@28241
     2
    ID:         $Id$
wenzelm@28241
     3
    Author:     Makarius
wenzelm@28241
     4
wenzelm@28577
     5
Simplified thread operations.
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@28577
    12
  val synchronized: string -> Mutex.mutex -> (unit -> 'a) -> 'a
wenzelm@28241
    13
end;
wenzelm@28241
    14
wenzelm@28241
    15
structure SimpleThread: SIMPLE_THREAD =
wenzelm@28241
    16
struct
wenzelm@28241
    17
wenzelm@28241
    18
fun fork interrupts body =
wenzelm@28241
    19
  Thread.fork (fn () => exception_trace (fn () => body ()),
wenzelm@28241
    20
    if interrupts then Multithreading.regular_interrupts else Multithreading.no_interrupts);
wenzelm@28241
    21
wenzelm@28550
    22
fun interrupt thread = Thread.interrupt thread handle Thread _ => ();
wenzelm@28550
    23
wenzelm@28577
    24
wenzelm@28577
    25
(* basic synchronization *)
wenzelm@28577
    26
wenzelm@28577
    27
fun synchronized name lock e = Exn.release (uninterruptible (fn restore_attributes => fn () =>
wenzelm@28577
    28
  let
wenzelm@28577
    29
    val _ =
wenzelm@28577
    30
      if Mutex.trylock lock then ()
wenzelm@28577
    31
      else
wenzelm@28577
    32
       (Multithreading.tracing 3 (fn () => name ^ ": locking ...");
wenzelm@28577
    33
        Mutex.lock lock;
wenzelm@28577
    34
        Multithreading.tracing 3 (fn () => name ^ ": ... locked"));
wenzelm@28577
    35
    val result = Exn.capture (restore_attributes e) ();
wenzelm@28577
    36
    val _ = Mutex.unlock lock;
wenzelm@28577
    37
  in result end) ());
wenzelm@28577
    38
wenzelm@28241
    39
end;