src/Pure/Isar/toplevel.ML
changeset 7602 2c0f407f80ce
parent 7501 76ed51454609
child 7612 ba11b5db431a
     1.1 --- a/src/Pure/Isar/toplevel.ML	Sat Sep 25 13:08:54 1999 +0200
     1.2 +++ b/src/Pure/Isar/toplevel.ML	Sat Sep 25 13:17:38 1999 +0200
     1.3 @@ -441,14 +441,6 @@
     1.4        Position.T * (Symbol.symbol, (string, unit) Source.source) Source.source)
     1.5            Source.source) Source.source) Source.source) Source.source;
     1.6  
     1.7 -fun transform_interrupt_isar f x =
     1.8 -  let val y = ref (None: (transition * isar) option option);
     1.9 -  in exhibit_interrupt (fn () => y := Some (f x)) (); the (! y) end;
    1.10 -
    1.11 -fun get_interruptible src =
    1.12 -  Some (transform_interrupt_isar Source.get_single src)
    1.13 -    handle Interrupt => None;
    1.14 -
    1.15  
    1.16  (* apply transformers to global state *)
    1.17  
    1.18 @@ -462,8 +454,12 @@
    1.19          check_stale state'; print_exn exn_info;
    1.20          true));
    1.21  
    1.22 +(*Note: this is for Poly/ML only, we really do not intend to exhibit
    1.23 +  interrupts here*)
    1.24 +fun get_interrupt src = Some (Source.get_single src) handle Interrupt => None;
    1.25 +
    1.26  fun raw_loop src =
    1.27 -  (case get_interruptible (Source.set_prompt (prompt_state (get_state ())) src) of
    1.28 +  (case get_interrupt (Source.set_prompt (prompt_state (get_state ())) src) of
    1.29      None => (writeln "\nInterrupt."; raw_loop src)
    1.30    | Some None => ()
    1.31    | Some (Some (tr, src')) => if >> tr then raw_loop src' else ());