# HG changeset patch
# User wenzelm
# Date 967737599 -7200
# Node ID da6788606f54eb9cf976c61e489e3ebd1317e327
# Parent  46def28153d6e7e2c97aba74b623e8bc21e8103d
fixed make_pp;
basic interrupt handling;

diff -r 46def28153d6 -r da6788606f54 src/Pure/ML-Systems/polyml-4.0.ML
--- a/src/Pure/ML-Systems/polyml-4.0.ML	Thu Aug 31 17:25:52 2000 +0200
+++ b/src/Pure/ML-Systems/polyml-4.0.ML	Thu Aug 31 17:59:59 2000 +0200
@@ -8,7 +8,15 @@
 
 (** ML system related **)
 
-open PolyML;
+(* old Poly/ML emulation *)
+
+local
+  val orig_exit = exit;
+in
+  open PolyML;
+  val exit = orig_exit;
+  fun quit () = exit 0;
+end;
 
 
 (* restore old-style character / string functions *)
@@ -43,13 +51,9 @@
 
 (* toplevel pretty printing (see also Pure/install_pp.ML) *)
 
-fun make_pp path pprint = ();
-fun install_pp _ = ();
-(* FIXME
-fun make_pp _ pprint (str, blk, brk, en) obj =
+fun make_pp _ pprint (str, blk, brk, en) _ _ obj =
   pprint obj (str, fn ind => blk (ind, false), fn wd => brk (wd, 0),
     fn () => brk (99999, 0), en);
-*)
 
 
 (* ML command execution -- 'eval' *)
@@ -90,11 +94,36 @@
 
 
 
-(** interrupts **)      (*Note: may get into race conditions*)
+(** interrupts **)
+
+local
+
+datatype 'a result =
+  Result of 'a |
+  Exn of exn;
+
+fun capture f x = Result (f x) handle exn => Exn exn;
+
+fun release (Result x) = x
+  | release (Exn exn) = raise exn;
+
 
-fun mask_interrupt f x = f x;
-fun unmask_interrupt f x = f x;
-fun exhibit_interrupt f x = f x;
+val sig_int = 2;
+
+fun change_signal new_handler f x =
+  let
+    (*RACE wrt. other signals*)
+    val old_handler = Signal.signal (sig_int, new_handler);
+    val result = capture f x;
+    val _ = Signal.signal (sig_int, old_handler);
+  in release result end;
+
+in
+
+fun mask_interrupt f = change_signal Signal.SIG_IGN f;
+fun exhibit_interrupt f = change_signal Signal.SIG_DFL f;
+
+end;