# HG changeset patch
# User wenzelm
# Date 1197145206 -3600
# Node ID 72e71bcf42391cb61bd0a713a56e0628935577e3
# Parent  655453e635c443c03cb7effa527cfdf15d36abe6
secure_main: enforces terminator, to gain robustness;

diff -r 655453e635c4 -r 72e71bcf4239 src/Pure/Isar/outer_syntax.ML
--- a/src/Pure/Isar/outer_syntax.ML	Sat Dec 08 21:20:05 2007 +0100
+++ b/src/Pure/Isar/outer_syntax.ML	Sat Dec 08 21:20:06 2007 +0100
@@ -328,14 +328,14 @@
 
 (* main loop *)
 
-fun gen_loop secure terminated =
+fun gen_loop secure do_terminate =
  (CRITICAL (fn () => ML_Context.set_context NONE);
-  Toplevel.loop secure (isar terminated));
+  Toplevel.loop secure (isar do_terminate));
 
-fun gen_main secure terminated =
+fun gen_main secure do_terminate =
  (Toplevel.init_state ();
   writeln (Session.welcome ());
-  gen_loop secure terminated);
+  gen_loop secure do_terminate);
 
 structure Isar =
 struct
@@ -354,7 +354,7 @@
   fun loop () = gen_loop (Secure.is_secure ()) false;
   fun sync_main () = gen_main (Secure.is_secure ()) true;
   fun sync_loop () = gen_loop (Secure.is_secure ()) true;
-  fun secure_main () = gen_main true false;
+  fun secure_main () = gen_main true true;
   val toplevel = Toplevel.program;
 end;