Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
get_interrupt: special handling of IO.io now in ML-Systems/smlnj-basis-compat.ML;
authorwenzelm
Tue, 20 Sep 2005 14:03:42 +0200
changeset 17513 0393718c2f1c
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 file | annotate | diff | comparison | revisions 
--- a/src/Pure/Isar/toplevel.ML	Tue Sep 20 14:03:41 2005 +0200
+++ b/src/Pure/Isar/toplevel.ML	Tue Sep 20 14:03:42 2005 +0200
@@ -642,11 +642,8 @@
 fun >>> [] = ()
   | >>> (tr :: trs) = if >> tr then >>> trs else ();
 
-(*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 _ => NONE;
+(*Spurious interrupts ahead!  Race condition?*)
+fun get_interrupt src = SOME (Source.get_single src) handle Interrupt => NONE;
 
 fun raw_loop src =
   (case get_interrupt (Source.set_prompt (prompt_state (get_state ())) src) of
isabelle