# HG changeset patch
# User wenzelm
# Date 910606173 -3600
# Node ID 4eea84a9427d3f91751372c19c388c1cc5313232
# Parent  cbc106ddcc83eba04d45a06a809793fd44c3bf13
fake interrupt handler;

diff -r cbc106ddcc83 -r 4eea84a9427d src/Pure/ML-Systems/polyml.ML
--- a/src/Pure/ML-Systems/polyml.ML	Mon Nov 09 11:08:42 1998 +0100
+++ b/src/Pure/ML-Systems/polyml.ML	Mon Nov 09 11:09:33 1998 +0100
@@ -21,9 +21,9 @@
 fun startTiming() = System.processtime ();
 
 (*Finish timing and return string*)
-fun endTiming before = 
-  "User + GC: " ^ 
-  makestring (real (System.processtime () - before) / 10.0) ^ 
+fun endTiming before =
+  "User + GC: " ^
+  makestring (real (System.processtime () - before) / 10.0) ^
   " secs";
 
 
@@ -65,6 +65,14 @@
 
 
 
+(** interrupts **)      (*Note: may get into race conditions*)
+
+fun mask_interrupt f x = f x;
+fun unmask_interrupt f x = f x;
+fun exhibit_interrupt f x = f x;
+
+
+
 (** OS related **)
 
 local
@@ -96,7 +104,7 @@
 (* file handling *)
 
 (*get time of last modification; if file doesn't exist return an empty string*)
-fun file_info "" = ""		(* FIXME !? *)
+fun file_info "" = ""           (* FIXME !? *)
   | file_info name = Int.toString (System.filedate name) handle _ => "";
 
 structure OS =