# 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;