Exn.is_interrupt: include interrupts that have passed through the IO layer;

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

--- 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 **)