# HG changeset patch
# User wenzelm
# Date 1127217874 -7200
# Node ID 1d7771a659f61eca6e28481090371b5161b6ec72
# Parent  0393718c2f1cbd8c0a0cbd8df40397453bf3685d
TextIO.inputLine: handle IO.Io, assuming it stems from a signal;

diff -r 0393718c2f1c -r 1d7771a659f6 src/Pure/ML-Systems/smlnj-basis-compat.ML
--- a/src/Pure/ML-Systems/smlnj-basis-compat.ML	Tue Sep 20 14:03:42 2005 +0200
+++ b/src/Pure/ML-Systems/smlnj-basis-compat.ML	Tue Sep 20 14:04:34 2005 +0200
@@ -4,14 +4,16 @@
 
 Compatibility file for Standard ML of New Jersey 110.44 or later. Here
 signatures that have changed to adhere to the SML Basis Library are
-changed back to their old values. So much for standards...
+changed back to their old values.
 *)
 
 structure TextIO =
 struct
-open TextIO
-fun inputLine is =
-    case TextIO.inputLine is of
-	SOME str => str
-      | NONE => ""
-end;
\ No newline at end of file
+  open TextIO;
+
+  fun inputLine is =
+    (case TextIO.inputLine is of
+      SOME str => str
+    | NONE => "")
+    handle IO.Io _ => raise Interrupt;
+end;