# HG changeset patch
# User wenzelm
# Date 1223578403 -7200
# Node ID a6065ce44984df4fbdbdfe7049b6ba9a79e65165
# Parent  675270d2d304cf78a68e7fb99ca0cef6db688ab5
added enabled;

diff -r 675270d2d304 -r a6065ce44984 src/Pure/ML-Systems/multithreading.ML
--- a/src/Pure/ML-Systems/multithreading.ML	Thu Oct 09 20:53:22 2008 +0200
+++ b/src/Pure/ML-Systems/multithreading.ML	Thu Oct 09 20:53:23 2008 +0200
@@ -19,6 +19,7 @@
   val available: bool
   val max_threads: int ref
   val max_threads_value: unit -> int
+  val enabled: unit -> bool
   val no_interrupts: Thread.threadAttribute list
   val regular_interrupts: Thread.threadAttribute list
   val with_attributes: Thread.threadAttribute list ->
@@ -38,6 +39,7 @@
 val available = false;
 val max_threads = ref (1: int);
 fun max_threads_value () = 1: int;
+fun enabled () = false;
 
 val no_interrupts =
   [Thread.EnableBroadcastInterrupt false, Thread.InterruptState Thread.InterruptDefer];