--- a/src/Pure/Isar/session.ML Thu Feb 21 21:31:51 2008 +0100
+++ b/src/Pure/Isar/session.ML Thu Feb 21 21:31:52 2008 +0100
@@ -36,7 +36,11 @@
| str_of elems = space_implode "/" elems;
fun name () = "Isabelle/" ^ str_of (path ());
-fun welcome () = "Welcome to " ^ name () ^ " (" ^ version ^ ")";
+
+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 "");
(* add_path *)
--- a/src/Pure/ProofGeneral/proof_general_pgip.ML Thu Feb 21 21:31:51 2008 +0100
+++ b/src/Pure/ProofGeneral/proof_general_pgip.ML Thu Feb 21 21:31:52 2008 +0100
@@ -451,7 +451,7 @@
val proverinfo =
Proverinfo { name = "Isabelle",
- version = version,
+ version = Distribution.version,
instance = Session.name(),
descr = "The Isabelle/Isar theorem prover",
url = wwwpage,
--- a/src/Pure/ROOT.ML Thu Feb 21 21:31:51 2008 +0100
+++ b/src/Pure/ROOT.ML Thu Feb 21 21:31:52 2008 +0100
@@ -4,7 +4,12 @@
Pure Isabelle.
*)
-val version = "Isabelle repository version"; (*filled in automatically!*)
+structure Distribution = (*filled-in by makedist*)
+struct
+ val version = "Isabelle repository version";
+ val is_unofficial = false;
+ val has_changelog = false;
+end;
(*if true then some tools will OMIT some proofs*)
val quick_and_dirty = ref false;
--- a/src/Pure/Thy/html.ML Thu Feb 21 21:31:51 2008 +0100
+++ b/src/Pure/Thy/html.ML Thu Feb 21 21:31:52 2008 +0100
@@ -314,7 +314,7 @@
\<html>\n\
\<head>\n\
\<meta http-equiv=\"Content-Type\" content=\"text/html; charset=" ^ ! charset ^ "\">\n\
- \<title>" ^ plain (title ^ " (" ^ version ^ ")") ^ "</title>\n\
+ \<title>" ^ plain (title ^ " (" ^ Distribution.version ^ ")") ^ "</title>\n\
\<link rel=\"stylesheet\" type=\"text/css\" href=\"isabelle.css\">\n\
\</head>\n\
\\n\