equal
deleted
inserted
replaced
701 | >>> (tr :: trs) = if >> tr then >>> trs else (); |
701 | >>> (tr :: trs) = if >> tr then >>> trs else (); |
702 |
702 |
703 (*Spurious interrupts ahead! Race condition?*) |
703 (*Spurious interrupts ahead! Race condition?*) |
704 fun get_interrupt src = SOME (Source.get_single src) handle Interrupt => NONE; |
704 fun get_interrupt src = SOME (Source.get_single src) handle Interrupt => NONE; |
705 |
705 |
|
706 fun warn_secure () = |
|
707 let val secure = Secure.is_secure () |
|
708 in if secure then warning "Cannot exit to ML in secure mode" else (); secure end; |
|
709 |
706 fun raw_loop src = |
710 fun raw_loop src = |
707 (case get_interrupt (Source.set_prompt (prompt_state (get_state ())) src) of |
711 (case get_interrupt (Source.set_prompt (prompt_state (get_state ())) src) of |
708 NONE => (writeln "\nInterrupt."; raw_loop src) |
712 NONE => (writeln "\nInterrupt."; raw_loop src) |
709 | SOME NONE => () |
713 | SOME NONE => if warn_secure () then quit () else () |
710 | SOME (SOME (tr, src')) => if >> tr then raw_loop src' else ()); |
714 | SOME (SOME (tr, src')) => |
|
715 if >> tr orelse warn_secure () then raw_loop src' |
|
716 else ()); |
711 |
717 |
712 fun loop src = ignore_interrupt raw_loop src; |
718 fun loop src = ignore_interrupt raw_loop src; |
713 |
719 |
714 end; |
720 end; |