added welcome;

--- a/src/Pure/Isar/isar_cmd.ML	Fri Sep 03 18:16:54 1999 +0200
+++ b/src/Pure/Isar/isar_cmd.ML	Fri Sep 03 18:17:51 1999 +0200
@@ -7,9 +7,10 @@
 
 signature ISAR_CMD =
 sig
+  val welcome: Toplevel.transition -> Toplevel.transition
+  val init_toplevel: Toplevel.transition -> Toplevel.transition
   val exit: Toplevel.transition -> Toplevel.transition
   val quit: Toplevel.transition -> Toplevel.transition
-  val init_toplevel: Toplevel.transition -> Toplevel.transition
   val touch_all_thys: Toplevel.transition -> Toplevel.transition
   val touch_thy: string -> Toplevel.transition -> Toplevel.transition
   val remove_thy: string -> Toplevel.transition -> Toplevel.transition
@@ -49,7 +50,10 @@
 struct
 
 
-(* variations on exit *)
+(* variations on init / exit *)
+
+val init_toplevel = Toplevel.imperative (fn () => raise Toplevel.RESTART);
+val welcome = Toplevel.imperative (writeln o Session.welcome);
 
 val exit = Toplevel.keep (fn state =>
   (Context.set_context (try Toplevel.theory_of state);
@@ -58,8 +62,6 @@
 
 val quit = Toplevel.imperative quit;
 
-val init_toplevel = Toplevel.imperative (fn () => raise Toplevel.RESTART);
-
 
 (* touch theories *)
 

--- a/src/Pure/Isar/isar_syn.ML	Fri Sep 03 18:16:54 1999 +0200
+++ b/src/Pure/Isar/isar_syn.ML	Fri Sep 03 18:17:51 1999 +0200
@@ -559,6 +559,10 @@
   OuterSyntax.improper_command "init_toplevel" "restart Isar toplevel loop" K.control
     (Scan.succeed IsarCmd.init_toplevel);
 
+val welcomeP =
+  OuterSyntax.improper_command "welcome" "print welcome message" K.control
+    (Scan.succeed IsarCmd.welcome);
+
 
 
 (** the Pure outer syntax **)
@@ -599,7 +603,7 @@
   (*system commands*)
   cdP, pwdP, use_thyP, use_thy_onlyP, update_thyP, update_thy_onlyP,
   touch_thyP, touch_all_thysP, remove_thyP, prP, disable_prP,
-  enable_prP, commitP, quitP, exitP, init_toplevelP];
+  enable_prP, commitP, quitP, exitP, init_toplevelP, welcomeP];
 
 
 end;