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