# HG changeset patch
# User wenzelm
# Date 1160415427 -7200
# Node ID 74910a189f1ddb8a37aa52a4779e92e30d982f24
# Parent  2a39f21257729d8023a095d79904d4c560c04e35
loop: disallow exit in secure mode;

diff -r 2a39f2125772 -r 74910a189f1d src/Pure/Isar/toplevel.ML
--- a/src/Pure/Isar/toplevel.ML	Mon Oct 09 19:37:06 2006 +0200
+++ b/src/Pure/Isar/toplevel.ML	Mon Oct 09 19:37:07 2006 +0200
@@ -703,11 +703,17 @@
 (*Spurious interrupts ahead!  Race condition?*)
 fun get_interrupt src = SOME (Source.get_single src) handle Interrupt => NONE;
 
+fun warn_secure () =
+  let val secure = Secure.is_secure ()
+  in if secure then warning "Cannot exit to ML in secure mode" else (); secure end;
+
 fun raw_loop src =
   (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 ());
+  | SOME NONE => if warn_secure () then quit () else ()
+  | SOME (SOME (tr, src')) =>
+      if >> tr orelse warn_secure () then raw_loop src'
+      else ());
 
 fun loop src = ignore_interrupt raw_loop src;