# HG changeset patch
# User webertj
# Date 1138389444 -3600
# Node ID 1a904aebfef0dde09deee484a5a7addf46e4eb61
# Parent  fc35dcc2558bdc3fd49fb8db9881d7d50fe5d368
interrupt_timeout for Poly replaced by stub

diff -r fc35dcc2558b -r 1a904aebfef0 src/Pure/ML-Systems/polyml-interrupt-timeout.ML
--- a/src/Pure/ML-Systems/polyml-interrupt-timeout.ML	Fri Jan 27 19:05:24 2006 +0100
+++ b/src/Pure/ML-Systems/polyml-interrupt-timeout.ML	Fri Jan 27 20:17:24 2006 +0100
@@ -6,6 +6,7 @@
 Bounded time execution (similar to SML/NJ's TimeLimit structure) for Poly/ML.
 *)
 
+(* FIXME: this code appears to disable signal handling in child databases altogether (?)
 local
 
   val alarm_active = ref false;
@@ -21,8 +22,6 @@
 
 in
 
-  (* Time.time -> ('a -> 'b) -> 'a -> 'b *)
-
   fun interrupt_timeout time f x =
   let
     fun deactivate_alarm () = (
@@ -42,3 +41,7 @@
   end;
 
 end;
+*)
+
+fun interrupt_timeout time f x =
+  f x;
diff -r fc35dcc2558b -r 1a904aebfef0 src/Pure/ML-Systems/polyml.ML
--- a/src/Pure/ML-Systems/polyml.ML	Fri Jan 27 19:05:24 2006 +0100
+++ b/src/Pure/ML-Systems/polyml.ML	Fri Jan 27 20:17:24 2006 +0100
@@ -62,12 +62,14 @@
 
 (* bounded time execution *)
 
-(* FIXME proper implementation for Cygwin available? *)
+(* FIXME proper implementation available? *)
 fun interrupt_timeout time f x =
   f x;
 
+(*
 unless_cygwin
   use "ML-Systems/polyml-interrupt-timeout.ML";
+*)
 
 
 (* prompts *)