src/Pure/Concurrent/simple_thread.ML
author haftmann
Tue, 23 Sep 2008 18:11:44 +0200
changeset 28337 93964076e7b8
parent 28241 de20fccf6509
child 28550 422e9bd169ac
permissions -rw-r--r--
case default fallback for NBE
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
28241
de20fccf6509 Simplified thread fork interface.
wenzelm
parents:
diff changeset
     1
(*  Title:      Pure/Concurrent/simple_thread.ML
de20fccf6509 Simplified thread fork interface.
wenzelm
parents:
diff changeset
     2
    ID:         $Id$
de20fccf6509 Simplified thread fork interface.
wenzelm
parents:
diff changeset
     3
    Author:     Makarius
de20fccf6509 Simplified thread fork interface.
wenzelm
parents:
diff changeset
     4
de20fccf6509 Simplified thread fork interface.
wenzelm
parents:
diff changeset
     5
Simplified thread fork interface.
de20fccf6509 Simplified thread fork interface.
wenzelm
parents:
diff changeset
     6
*)
de20fccf6509 Simplified thread fork interface.
wenzelm
parents:
diff changeset
     7
de20fccf6509 Simplified thread fork interface.
wenzelm
parents:
diff changeset
     8
signature SIMPLE_THREAD =
de20fccf6509 Simplified thread fork interface.
wenzelm
parents:
diff changeset
     9
sig
de20fccf6509 Simplified thread fork interface.
wenzelm
parents:
diff changeset
    10
  val fork: bool -> (unit -> unit) -> Thread.thread
de20fccf6509 Simplified thread fork interface.
wenzelm
parents:
diff changeset
    11
end;
de20fccf6509 Simplified thread fork interface.
wenzelm
parents:
diff changeset
    12
de20fccf6509 Simplified thread fork interface.
wenzelm
parents:
diff changeset
    13
structure SimpleThread: SIMPLE_THREAD =
de20fccf6509 Simplified thread fork interface.
wenzelm
parents:
diff changeset
    14
struct
de20fccf6509 Simplified thread fork interface.
wenzelm
parents:
diff changeset
    15
de20fccf6509 Simplified thread fork interface.
wenzelm
parents:
diff changeset
    16
fun fork interrupts body =
de20fccf6509 Simplified thread fork interface.
wenzelm
parents:
diff changeset
    17
  Thread.fork (fn () => exception_trace (fn () => body ()),
de20fccf6509 Simplified thread fork interface.
wenzelm
parents:
diff changeset
    18
    if interrupts then Multithreading.regular_interrupts else Multithreading.no_interrupts);
de20fccf6509 Simplified thread fork interface.
wenzelm
parents:
diff changeset
    19
de20fccf6509 Simplified thread fork interface.
wenzelm
parents:
diff changeset
    20
end;