--- 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;
--- 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;
--- 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;