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