# HG changeset patch
# User wenzelm
# Date 999204601 -7200
# Node ID d54301357129bbbba43516fe052b4f61841a9017
# Parent  168dbdaedb71ecd958ae62c6a2d518514cb29787
export name;

diff -r 168dbdaedb71 -r d54301357129 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 *)