get_interrupt: special handling of IO.io now in ML-Systems/smlnj-basis-compat.ML;
authorwenzelm
Tue Sep 20 14:03:42 2005 +0200 (2005-09-20 ago)
changeset 175130393718c2f1c
parent 17512 854d061f6c10
child 17514 1d7771a659f6
get_interrupt: special handling of IO.io now in ML-Systems/smlnj-basis-compat.ML;
src/Pure/Isar/toplevel.ML
     1.1 --- a/src/Pure/Isar/toplevel.ML	Tue Sep 20 14:03:41 2005 +0200
     1.2 +++ b/src/Pure/Isar/toplevel.ML	Tue Sep 20 14:03:42 2005 +0200
     1.3 @@ -642,11 +642,8 @@
     1.4  fun >>> [] = ()
     1.5    | >>> (tr :: trs) = if >> tr then >>> trs else ();
     1.6  
     1.7 -(*Note: we really do not intend to exhibit interrupts here.
     1.8 -  Poly/ML needs exception Interrupt to be handled. SML/NJ needs IO to be handled.*)
     1.9 -fun get_interrupt src = SOME (Source.get_single src) 
    1.10 -                        handle Interrupt => NONE
    1.11 -                             | IO.Io _ => NONE;
    1.12 +(*Spurious interrupts ahead!  Race condition?*)
    1.13 +fun get_interrupt src = SOME (Source.get_single src) handle Interrupt => NONE;
    1.14  
    1.15  fun raw_loop src =
    1.16    (case get_interrupt (Source.set_prompt (prompt_state (get_state ())) src) of