# HG changeset patch
# User wenzelm
# Date 1208176127 -7200
# Node ID 99f5407c05ef36888479e150688f68a4d6de2955
# Parent  454d11701fa453517a1c9ada67d0784e36010a6e
Isar.toplevel_loop: separate init/welcome flag;

diff -r 454d11701fa4 -r 99f5407c05ef src/Pure/Isar/isar.ML
--- a/src/Pure/Isar/isar.ML	Sun Apr 13 16:40:08 2008 +0200
+++ b/src/Pure/Isar/isar.ML	Mon Apr 14 14:28:47 2008 +0200
@@ -15,7 +15,7 @@
   val >>> : Toplevel.transition list -> unit
   val init: unit -> unit
   val crashes: exn list ref
-  val toplevel_loop: {init: bool, sync: bool, secure: bool} -> unit
+  val toplevel_loop: {init: bool, welcome: bool, sync: bool, secure: bool} -> unit
   val loop: unit -> unit
   val main: unit -> unit
 end;
@@ -81,15 +81,18 @@
 
 in
 
-fun toplevel_loop {init = do_init, sync, secure} =
+fun toplevel_loop {init = do_init, welcome, sync, secure} =
  (Context.set_thread_data NONE;
-  if do_init then (init (); writeln (Session.welcome ())) else ();
+  if do_init then init () else ();
+  if welcome then writeln (Session.welcome ()) else ();
   uninterruptible (fn _ => fn () => raw_loop secure (OuterSyntax.isar sync)) ());
 
 end;
 
-fun loop () = toplevel_loop {init = false, sync = false, secure = Secure.is_secure ()};
-fun main () = toplevel_loop {init = true, sync = false, secure = Secure.is_secure ()};
+fun loop () =
+  toplevel_loop {init = false, welcome = false, sync = false, secure = Secure.is_secure ()};
+fun main () =
+  toplevel_loop {init = true, welcome = true, sync = false, secure = Secure.is_secure ()};
 
 end;
 
diff -r 454d11701fa4 -r 99f5407c05ef src/Pure/ProofGeneral/proof_general_emacs.ML
--- a/src/Pure/ProofGeneral/proof_general_emacs.ML	Sun Apr 13 16:40:08 2008 +0200
+++ b/src/Pure/ProofGeneral/proof_general_emacs.ML	Mon Apr 14 14:28:47 2008 +0200
@@ -297,6 +297,6 @@
           set initialized);
         sync_thy_loader ();
        change print_mode (update (op =) proof_generalN);
-       Isar.toplevel_loop {init = true, sync = true, secure = Secure.is_secure ()});
+       Isar.toplevel_loop {init = true, welcome = true, sync = true, secure = Secure.is_secure ()});
 
 end;
diff -r 454d11701fa4 -r 99f5407c05ef src/Pure/Tools/isabelle_process.ML
--- a/src/Pure/Tools/isabelle_process.ML	Sun Apr 13 16:40:08 2008 +0200
+++ b/src/Pure/Tools/isabelle_process.ML	Mon Apr 14 14:28:47 2008 +0200
@@ -155,7 +155,7 @@
  (change print_mode (update (op =) isabelle_processN);
   setup_channels ();
   init_message ();
-  Isar.toplevel_loop {init = true, sync = true, secure = true});
+  Isar.toplevel_loop {init = true, welcome = false, sync = true, secure = true});
 
 end;