# HG changeset patch
# User wenzelm
# Date 1203956861 -3600
# Node ID 3b499feded50fa7f0e333a71cd7768df0e10c95e
# Parent  8ea867ad9a4827c39d7365b787414477363e36a2
welcome: actually check for ChangeLog.gz;
tuned structure Distribution;

diff -r 8ea867ad9a48 -r 3b499feded50 src/Pure/Isar/session.ML
--- a/src/Pure/Isar/session.ML	Mon Feb 25 17:27:38 2008 +0100
+++ b/src/Pure/Isar/session.ML	Mon Feb 25 17:27:41 2008 +0100
@@ -37,10 +37,14 @@
 
 fun name () = "Isabelle/" ^ str_of (path ());
 
+val log = Path.explode "$ISABELLE_HOME/src/ChangeLog.gz";
+
 fun welcome () =
-  (if Distribution.is_unofficial then "Unofficial version of " else "Welcome to ") ^
-    name () ^ " (" ^ Distribution.version ^ ")" ^
-  (if Distribution.has_changelog then "\nSee ChangeLog.gz for details" else "");
+  if Distribution.is_official then
+    "Welcome to " ^ name () ^ " (" ^ Distribution.version ^ ")"
+  else
+    "Unofficial version of " ^ name () ^ " (" ^ Distribution.version ^ ")" ^
+    (if File.exists log then "\nSee " ^ Path.implode (Path.expand log) ^ " for details" else "");
 
 
 (* add_path *)