# HG changeset patch
# User wenzelm
# Date 1284046725 -7200
# Node ID 9a0c67d4517a73634a32b171edabc7c94352aa99
# Parent  69c6d3e87660610bc51186abf73479620e7bc68e
Exn.is_interrupt: include interrupts that have passed through the IO layer;

diff -r 69c6d3e87660 -r 9a0c67d4517a src/Pure/General/exn.ML
--- a/src/Pure/General/exn.ML	Thu Sep 09 17:20:27 2010 +0200
+++ b/src/Pure/General/exn.ML	Thu Sep 09 17:38:45 2010 +0200
@@ -51,6 +51,7 @@
 fun interrupt () = raise Interrupt;
 
 fun is_interrupt Interrupt = true
+  | is_interrupt (IO.Io {cause = Interrupt, ...}) = true
   | is_interrupt _ = false;
 
 val interrupt_exn = Exn Interrupt;
diff -r 69c6d3e87660 -r 9a0c67d4517a src/Pure/ML-Systems/smlnj.ML
--- a/src/Pure/ML-Systems/smlnj.ML	Thu Sep 09 17:20:27 2010 +0200
+++ b/src/Pure/ML-Systems/smlnj.ML	Thu Sep 09 17:38:45 2010 +0200
@@ -159,16 +159,6 @@
 end;
 
 
-(* basis library fixes *)
-
-structure TextIO =
-struct
-  open TextIO;
-  fun inputLine is = TextIO.inputLine is
-    handle IO.Io _ => Exn.interrupt ();
-end;
-
-
 
 (** OS related **)