author | paulson |
Tue, 20 Sep 2005 13:17:32 +0200 | |
changeset 17500 | 964bad535ac6 |
parent 17499 | 5274ecba8fea |
child 17501 | acbebb72e85a |
--- a/src/Pure/Isar/toplevel.ML Tue Sep 20 10:36:33 2005 +0200 +++ b/src/Pure/Isar/toplevel.ML Tue Sep 20 13:17:32 2005 +0200 @@ -646,7 +646,7 @@ 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; + | IO.Io _ => NONE; fun raw_loop src = (case get_interrupt (Source.set_prompt (prompt_state (get_state ())) src) of