# HG changeset patch
# User wenzelm
# Date 1221572252 -7200
# Node ID de20fccf65096c3ab97f61be59fbdfe8ef7c50cd
# Parent  444d1e8ae496f810cb72c0e3c53e6df0449ebd9c
Simplified thread fork interface.

diff -r 444d1e8ae496 -r de20fccf6509 src/Pure/Concurrent/simple_thread.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Concurrent/simple_thread.ML	Tue Sep 16 15:37:32 2008 +0200
@@ -0,0 +1,20 @@
+(*  Title:      Pure/Concurrent/simple_thread.ML
+    ID:         $Id$
+    Author:     Makarius
+
+Simplified thread fork interface.
+*)
+
+signature SIMPLE_THREAD =
+sig
+  val fork: bool -> (unit -> unit) -> Thread.thread
+end;
+
+structure SimpleThread: SIMPLE_THREAD =
+struct
+
+fun fork interrupts body =
+  Thread.fork (fn () => exception_trace (fn () => body ()),
+    if interrupts then Multithreading.regular_interrupts else Multithreading.no_interrupts);
+
+end;