# HG changeset patch
# User wenzelm
# Date 1196804967 -3600
# Node ID 05ee7d85912e264452c31454ad6c1095fe3b38e6
# Parent  d6b898681fc7c48f88b0799ff007bfe9e0c21082
added Isar.secure_main;
pass Secure.is_secure to Toplevel.loop;

diff -r d6b898681fc7 -r 05ee7d85912e src/Pure/Isar/outer_syntax.ML
--- a/src/Pure/Isar/outer_syntax.ML	Tue Dec 04 22:49:26 2007 +0100
+++ b/src/Pure/Isar/outer_syntax.ML	Tue Dec 04 22:49:27 2007 +0100
@@ -19,6 +19,7 @@
       val loop: unit -> unit
       val sync_main: unit -> unit
       val sync_loop: unit -> unit
+      val secure_main: unit -> unit
       val toplevel: (unit -> 'a) -> 'a
     end;
 end;
@@ -319,14 +320,14 @@
 
 (* main loop *)
 
-fun gen_loop term =
+fun gen_loop secure terminated =
  (CRITICAL (fn () => ML_Context.set_context NONE);
-  Toplevel.loop (isar term));
+  Toplevel.loop secure (isar terminated));
 
-fun gen_main term =
+fun gen_main secure terminated =
  (Toplevel.init_state ();
   writeln (Session.welcome ());
-  gen_loop term);
+  gen_loop secure terminated);
 
 structure Isar =
 struct
@@ -341,10 +342,11 @@
     #2 (Proof.get_goal (Toplevel.proof_of (state ())))
       handle Toplevel.UNDEF => error "No goal present";
 
-  fun main () = gen_main false;
-  fun loop () = gen_loop false;
-  fun sync_main () = gen_main true;
-  fun sync_loop () = gen_loop true;
+  fun main () = gen_main (Secure.is_secure ()) false;
+  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;
   val toplevel = Toplevel.program;
 end;