export name;
authorwenzelm
Thu, 30 Aug 2001 22:50:01 +0200
changeset 11509 d54301357129
parent 11508 168dbdaedb71
child 11510 c6dd19025abe
export name;
src/Pure/Isar/session.ML
--- a/src/Pure/Isar/session.ML	Thu Aug 30 17:49:46 2001 +0200
+++ b/src/Pure/Isar/session.ML	Thu Aug 30 22:50:01 2001 +0200
@@ -8,6 +8,7 @@
 
 signature SESSION =
 sig
+  val name: unit -> string
   val welcome: unit -> string
   val use_dir:
     string list -> bool -> bool -> string -> string -> string -> string -> string -> unit
@@ -35,7 +36,8 @@
 fun str_of [] = pure
   | str_of elems = space_implode "/" elems;
 
-fun welcome () = "Welcome to Isabelle/" ^ str_of (path ()) ^ " (" ^ version ^ ")";
+fun name () = "Isabelle/" ^ str_of (path ());
+fun welcome () = "Welcome to " ^ name () ^ " (" ^ version ^ ")";
 
 
 (* add_path *)