welcome: actually check for ChangeLog.gz;
authorwenzelm
Mon, 25 Feb 2008 17:27:41 +0100
changeset 26134 3b499feded50
parent 26133 8ea867ad9a48
child 26135 01f4e5d21eaf
welcome: actually check for ChangeLog.gz; tuned structure Distribution;
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 *)