# HG changeset patch
# User wenzelm
# Date 1368647709 -7200
# Node ID d021c180e7df300c4c7f7f76dfb956f678bbad45
# Parent  45929e0e1d73b93b038ee480fff10f3a19a897a0
back to hidden welcome -- revert change 9ebf2da69b29, which appears to disturb startup protocol of PG 4.1;

diff -r 45929e0e1d73 -r d021c180e7df src/Pure/Tools/proof_general.ML
--- a/src/Pure/Tools/proof_general.ML	Wed May 15 21:46:07 2013 +0200
+++ b/src/Pure/Tools/proof_general.ML	Wed May 15 21:55:09 2013 +0200
@@ -388,9 +388,6 @@
 
 (** startup **)
 
-val welcome = Output.urgent_message o Session.welcome;
-
-
 (* init *)
 
 val proof_generalN = "ProofGeneral";
@@ -410,13 +407,14 @@
    sync_thy_loader ();
    Unsynchronized.change print_mode (update (op =) proof_generalN);
    Secure.PG_setup ();
-   welcome ();
    Isar.toplevel_loop TextIO.stdIn
-    {init = true, welcome = false, sync = true, secure = Secure.is_secure ()});
+    {init = true, welcome = true, sync = true, secure = Secure.is_secure ()});
 
 
 (* restart *)
 
+val welcome = Output.urgent_message o Session.welcome;
+
 fun restart () =
  (sync_thy_loader ();
   tell_clear_goals ();