src/Pure/Isar/toplevel.ML
changeset 17500 964bad535ac6
parent 17452 178344c74562
child 17513 0393718c2f1c
equal deleted inserted replaced
17499:5274ecba8fea 17500:964bad535ac6
   644 
   644 
   645 (*Note: we really do not intend to exhibit interrupts here.
   645 (*Note: we really do not intend to exhibit interrupts here.
   646   Poly/ML needs exception Interrupt to be handled. SML/NJ needs IO to be handled.*)
   646   Poly/ML needs exception Interrupt to be handled. SML/NJ needs IO to be handled.*)
   647 fun get_interrupt src = SOME (Source.get_single src) 
   647 fun get_interrupt src = SOME (Source.get_single src) 
   648                         handle Interrupt => NONE
   648                         handle Interrupt => NONE
   649                              | IO.Io _ => get_interrupt src;
   649                              | IO.Io _ => NONE;
   650 
   650 
   651 fun raw_loop src =
   651 fun raw_loop src =
   652   (case get_interrupt (Source.set_prompt (prompt_state (get_state ())) src) of
   652   (case get_interrupt (Source.set_prompt (prompt_state (get_state ())) src) of
   653     NONE => (writeln "\nInterrupt."; raw_loop src)
   653     NONE => (writeln "\nInterrupt."; raw_loop src)
   654   | SOME NONE => ()
   654   | SOME NONE => ()