Exn.is_interrupt: include interrupts that have passed through the IO layer;
authorwenzelm
Thu Sep 09 17:38:45 2010 +0200 (2010-09-09 ago)
changeset 392339a0c67d4517a
parent 39232 69c6d3e87660
child 39234 d76a2fd129b5
Exn.is_interrupt: include interrupts that have passed through the IO layer;
src/Pure/General/exn.ML
src/Pure/ML-Systems/smlnj.ML
     1.1 --- a/src/Pure/General/exn.ML	Thu Sep 09 17:20:27 2010 +0200
     1.2 +++ b/src/Pure/General/exn.ML	Thu Sep 09 17:38:45 2010 +0200
     1.3 @@ -51,6 +51,7 @@
     1.4  fun interrupt () = raise Interrupt;
     1.5  
     1.6  fun is_interrupt Interrupt = true
     1.7 +  | is_interrupt (IO.Io {cause = Interrupt, ...}) = true
     1.8    | is_interrupt _ = false;
     1.9  
    1.10  val interrupt_exn = Exn Interrupt;
     2.1 --- a/src/Pure/ML-Systems/smlnj.ML	Thu Sep 09 17:20:27 2010 +0200
     2.2 +++ b/src/Pure/ML-Systems/smlnj.ML	Thu Sep 09 17:38:45 2010 +0200
     2.3 @@ -159,16 +159,6 @@
     2.4  end;
     2.5  
     2.6  
     2.7 -(* basis library fixes *)
     2.8 -
     2.9 -structure TextIO =
    2.10 -struct
    2.11 -  open TextIO;
    2.12 -  fun inputLine is = TextIO.inputLine is
    2.13 -    handle IO.Io _ => Exn.interrupt ();
    2.14 -end;
    2.15 -
    2.16 -
    2.17  
    2.18  (** OS related **)
    2.19