# HG changeset patch
# User wenzelm
# Date 1296925797 -3600
# Node ID 11ae688e4e3028f38d68d78624e1911d9a821d2e
# Parent  2e427f340ad1a759c71f54f4c52255ba1de7f2b8
clarified bootstrapping of structure TimeLimit;

diff -r 2e427f340ad1 -r 11ae688e4e30 src/Pure/Concurrent/time_limit.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Concurrent/time_limit.ML	Sat Feb 05 18:09:57 2011 +0100
@@ -0,0 +1,32 @@
+(*  Title:      Pure/Concurrent/time_limit.ML
+    Author:     Makarius
+
+Execution with time limit.
+*)
+
+signature TIME_LIMIT =
+sig
+  exception TimeOut
+  val timeLimit : Time.time -> ('a -> 'b) -> 'a -> 'b
+end;
+
+structure TimeLimit: TIME_LIMIT =
+struct
+
+exception TimeOut;
+
+fun timeLimit time f x = uninterruptible (fn restore_attributes => fn () =>
+  let
+    val worker = Thread.self ();
+    val timeout = Unsynchronized.ref false;
+    val watchdog = Thread.fork (fn () =>
+      (OS.Process.sleep time; timeout := true; Thread.interrupt worker), []);
+
+    val result = Exn.capture (restore_attributes f) x;
+    val was_timeout = Exn.is_interrupt_exn result andalso ! timeout;
+
+    val _ = Thread.interrupt watchdog handle Thread _ => ();
+  in if was_timeout then raise TimeOut else Exn.release result end) ();
+
+end;
+
diff -r 2e427f340ad1 -r 11ae688e4e30 src/Pure/Concurrent/time_limit_dummy.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Concurrent/time_limit_dummy.ML	Sat Feb 05 18:09:57 2011 +0100
@@ -0,0 +1,15 @@
+(*  Title:      Pure/Concurrent/time_limit_dummy.ML
+    Author:     Makarius
+
+Execution with time limit -- dummy version.
+*)
+
+structure TimeLimit: TIME_LIMIT =
+struct
+
+exception TimeOut;
+
+fun timeLimit _ f x = (warning "No timeout support on this ML platform"; f x);
+
+end;
+
diff -r 2e427f340ad1 -r 11ae688e4e30 src/Pure/IsaMakefile
--- a/src/Pure/IsaMakefile	Fri Feb 04 21:52:36 2011 +0100
+++ b/src/Pure/IsaMakefile	Sat Feb 05 18:09:57 2011 +0100
@@ -40,7 +40,6 @@
   ML-Systems/single_assignment_polyml.ML		\
   ML-Systems/smlnj.ML					\
   ML-Systems/thread_dummy.ML				\
-  ML-Systems/time_limit.ML				\
   ML-Systems/universal.ML				\
   ML-Systems/unsynchronized.ML				\
   ML-Systems/use_context.ML
@@ -69,6 +68,8 @@
   Concurrent/synchronized.ML				\
   Concurrent/synchronized_sequential.ML			\
   Concurrent/task_queue.ML				\
+  Concurrent/time_limit.ML				\
+  Concurrent/time_limit_dummy.ML			\
   General/alist.ML					\
   General/antiquote.ML					\
   General/balanced_tree.ML				\
diff -r 2e427f340ad1 -r 11ae688e4e30 src/Pure/ML-Systems/multithreading_polyml.ML
--- a/src/Pure/ML-Systems/multithreading_polyml.ML	Fri Feb 04 21:52:36 2011 +0100
+++ b/src/Pure/ML-Systems/multithreading_polyml.ML	Sat Feb 05 18:09:57 2011 +0100
@@ -8,7 +8,6 @@
 sig
   val interruptible: ('a -> 'b) -> 'a -> 'b
   val uninterruptible: ((('c -> 'd) -> 'c -> 'd) -> 'a -> 'b) -> 'a -> 'b
-  structure TimeLimit: TIME_LIMIT
 end;
 
 signature BASIC_MULTITHREADING =
@@ -118,29 +117,6 @@
   in time end;
 
 
-(* execution with time limit *)
-
-structure TimeLimit =
-struct
-
-exception TimeOut;
-
-fun timeLimit time f x = uninterruptible (fn restore_attributes => fn () =>
-  let
-    val worker = Thread.self ();
-    val timeout = ref false;
-    val watchdog = Thread.fork (fn () =>
-      (OS.Process.sleep time; timeout := true; Thread.interrupt worker), []);
-
-    val result = Exn.capture (restore_attributes f) x;
-    val was_timeout = Exn.is_interrupt_exn result andalso ! timeout;
-
-    val _ = Thread.interrupt watchdog handle Thread _ => ();
-  in if was_timeout then raise TimeOut else Exn.release result end) ();
-
-end;
-
-
 (* critical section -- may be nested within the same thread *)
 
 local
diff -r 2e427f340ad1 -r 11ae688e4e30 src/Pure/ML-Systems/polyml_common.ML
--- a/src/Pure/ML-Systems/polyml_common.ML	Fri Feb 04 21:52:36 2011 +0100
+++ b/src/Pure/ML-Systems/polyml_common.ML	Sat Feb 05 18:09:57 2011 +0100
@@ -14,7 +14,6 @@
 else use "ML-Systems/single_assignment_polyml.ML";
 
 use "ML-Systems/multithreading.ML";
-use "ML-Systems/time_limit.ML";
 use "General/timing.ML";
 use "ML-Systems/ml_pretty.ML";
 use "ML-Systems/use_context.ML";
diff -r 2e427f340ad1 -r 11ae688e4e30 src/Pure/ML-Systems/time_limit.ML
--- a/src/Pure/ML-Systems/time_limit.ML	Fri Feb 04 21:52:36 2011 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,20 +0,0 @@
-(*  Title:      Pure/ML-Systems/time_limit.ML
-    Author:     Makarius
-
-Dummy implementation of NJ's TimeLimit structure.
-*)
-
-signature TIME_LIMIT =
-sig
-  exception TimeOut
-  val timeLimit : Time.time -> ('a -> 'b) -> 'a -> 'b
-end;
-
-structure TimeLimit: TIME_LIMIT =
-struct
-
-exception TimeOut;
-fun timeLimit _ f x = f x;
-
-end;
-
diff -r 2e427f340ad1 -r 11ae688e4e30 src/Pure/ROOT.ML
--- a/src/Pure/ROOT.ML	Fri Feb 04 21:52:36 2011 +0100
+++ b/src/Pure/ROOT.ML	Sat Feb 05 18:09:57 2011 +0100
@@ -72,6 +72,10 @@
 if Multithreading.available then ()
 else use "Concurrent/synchronized_sequential.ML";
 
+use "Concurrent/time_limit.ML";
+if Multithreading.available then ()
+else use "Concurrent/time_limit_dummy.ML";
+
 if Multithreading.available
 then use "Concurrent/bash.ML"
 else use "Concurrent/bash_sequential.ML";