# HG changeset patch
# User wenzelm
# Date 938258258 -7200
# Node ID 2c0f407f80cec931fa6b5e60cd2c16569cccc1a9
# Parent  c568799bf21be5bec6a24eb1d9967a7508fb5146
avoid interrupts of read loop;

diff -r c568799bf21b -r 2c0f407f80ce src/Pure/Isar/toplevel.ML
--- a/src/Pure/Isar/toplevel.ML	Sat Sep 25 13:08:54 1999 +0200
+++ b/src/Pure/Isar/toplevel.ML	Sat Sep 25 13:17:38 1999 +0200
@@ -441,14 +441,6 @@
       Position.T * (Symbol.symbol, (string, unit) Source.source) Source.source)
           Source.source) Source.source) Source.source) Source.source;
 
-fun transform_interrupt_isar f x =
-  let val y = ref (None: (transition * isar) option option);
-  in exhibit_interrupt (fn () => y := Some (f x)) (); the (! y) end;
-
-fun get_interruptible src =
-  Some (transform_interrupt_isar Source.get_single src)
-    handle Interrupt => None;
-
 
 (* apply transformers to global state *)
 
@@ -462,8 +454,12 @@
         check_stale state'; print_exn exn_info;
         true));
 
+(*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;
+
 fun raw_loop src =
-  (case get_interruptible (Source.set_prompt (prompt_state (get_state ())) src) of
+  (case get_interrupt (Source.set_prompt (prompt_state (get_state ())) src) of
     None => (writeln "\nInterrupt."; raw_loop src)
   | Some None => ()
   | Some (Some (tr, src')) => if >> tr then raw_loop src' else ());