src/Pure/Isar/outer_syntax.ML

       val goal: unit -> thm list * thm
       val main: unit -> unit
       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;
 
 signature OUTER_SYNTAX =

 
 (** the read-eval-print loop **)
 
 (* main loop *)
 
-fun gen_loop term =
+fun gen_loop secure terminated =
  (CRITICAL (fn () => ML_Context.set_context NONE);
-  Toplevel.loop (isar term));
-
-fun gen_main term =
+  Toplevel.loop secure (isar terminated));
+
+fun gen_main secure terminated =
  (Toplevel.init_state ();
   writeln (Session.welcome ());
-  gen_loop term);
+  gen_loop secure terminated);
 
 structure Isar =
 struct
   val state = Toplevel.get_state;
   val exn = Toplevel.exn;

 
   fun goal () =
     #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;
 
 end;