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