# HG changeset patch
# User wenzelm
# Date 1203625912 -3600
# Node ID c69c3559355b5401b962e6f9a5210df8e54e5a23
# Parent 46f4e4cd3b693c5d76e7a5faebe594229e2fd5a0
more elaborate structure Distribution (filled-in by makedist);
diff -r 46f4e4cd3b69 -r c69c3559355b src/Pure/Isar/session.ML
--- 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 *)
diff -r 46f4e4cd3b69 -r c69c3559355b src/Pure/ProofGeneral/proof_general_pgip.ML
--- 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,
diff -r 46f4e4cd3b69 -r c69c3559355b src/Pure/ROOT.ML
--- 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;
diff -r 46f4e4cd3b69 -r c69c3559355b src/Pure/Thy/html.ML
--- 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 @@
\\n\
\\n\
\\n\
- \" ^ plain (title ^ " (" ^ version ^ ")") ^ "\n\
+ \" ^ plain (title ^ " (" ^ Distribution.version ^ ")") ^ "\n\
\\n\
\\n\
\\n\