# HG changeset patch
# User paulson
# Date 1126863529 -7200
# Node ID c2efacfe8ab8703fea0116a59267f1e6e9508e20
# Parent  4cf2e7980529ec1078e89faf44c6630af0920eb3
catching exception Io

diff -r 4cf2e7980529 -r c2efacfe8ab8 src/Pure/Isar/toplevel.ML
--- a/src/Pure/Isar/toplevel.ML	Fri Sep 16 02:20:50 2005 +0200
+++ b/src/Pure/Isar/toplevel.ML	Fri Sep 16 11:38:49 2005 +0200
@@ -638,9 +638,11 @@
 fun >>> [] = ()
   | >>> (tr :: trs) = if >> tr then >>> trs else ();
 
-(*Note: this is for Poly/ML only, we really do not intend to exhibit
-  interrupts here*)
-fun get_interrupt src = SOME (Source.get_single src) handle Interrupt => NONE;
+(*Note: we really do not intend to exhibit interrupts here.
+  Poly/ML needs exception Interrupt to be handled. SML/NJ needs IO to be handled.*)
+fun get_interrupt src = SOME (Source.get_single src) 
+                        handle Interrupt => NONE
+                             | IO.Io _ => get_interrupt src;
 
 fun raw_loop src =
   (case get_interrupt (Source.set_prompt (prompt_state (get_state ())) src) of