src/Pure/ML-Systems/smlnj-basis-compat.ML
changeset 17514 1d7771a659f6
parent 14656 765badface6a
--- 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;