more elaborate structure Distribution (filled-in by makedist);
authorwenzelm
Thu Feb 21 21:31:52 2008 +0100 (2008-02-21)
changeset 26109c69c3559355b
parent 26108 46f4e4cd3b69
child 26110 06eacfd8dd9f
more elaborate structure Distribution (filled-in by makedist);
src/Pure/Isar/session.ML
src/Pure/ProofGeneral/proof_general_pgip.ML
src/Pure/ROOT.ML
src/Pure/Thy/html.ML
     1.1 --- a/src/Pure/Isar/session.ML	Thu Feb 21 21:31:51 2008 +0100
     1.2 +++ b/src/Pure/Isar/session.ML	Thu Feb 21 21:31:52 2008 +0100
     1.3 @@ -36,7 +36,11 @@
     1.4    | str_of elems = space_implode "/" elems;
     1.5  
     1.6  fun name () = "Isabelle/" ^ str_of (path ());
     1.7 -fun welcome () = "Welcome to " ^ name () ^ " (" ^ version ^ ")";
     1.8 +
     1.9 +fun welcome () =
    1.10 +  (if Distribution.is_unofficial then "Unofficial version of " else "Welcome to ") ^
    1.11 +    name () ^ " (" ^ Distribution.version ^ ")" ^
    1.12 +  (if Distribution.has_changelog then "\nSee ChangeLog.gz for details" else "");
    1.13  
    1.14  
    1.15  (* add_path *)
     2.1 --- a/src/Pure/ProofGeneral/proof_general_pgip.ML	Thu Feb 21 21:31:51 2008 +0100
     2.2 +++ b/src/Pure/ProofGeneral/proof_general_pgip.ML	Thu Feb 21 21:31:52 2008 +0100
     2.3 @@ -451,7 +451,7 @@
     2.4  
     2.5          val proverinfo =
     2.6              Proverinfo { name = "Isabelle",
     2.7 -                         version = version,
     2.8 +                         version = Distribution.version,
     2.9                           instance = Session.name(),
    2.10                           descr = "The Isabelle/Isar theorem prover",
    2.11                           url = wwwpage,
     3.1 --- a/src/Pure/ROOT.ML	Thu Feb 21 21:31:51 2008 +0100
     3.2 +++ b/src/Pure/ROOT.ML	Thu Feb 21 21:31:52 2008 +0100
     3.3 @@ -4,7 +4,12 @@
     3.4  Pure Isabelle.
     3.5  *)
     3.6  
     3.7 -val version = "Isabelle repository version";    (*filled in automatically!*)
     3.8 +structure Distribution =     (*filled-in by makedist*)
     3.9 +struct
    3.10 +  val version = "Isabelle repository version";
    3.11 +  val is_unofficial = false;
    3.12 +  val has_changelog = false;
    3.13 +end;
    3.14  
    3.15  (*if true then some tools will OMIT some proofs*)
    3.16  val quick_and_dirty = ref false;
     4.1 --- a/src/Pure/Thy/html.ML	Thu Feb 21 21:31:51 2008 +0100
     4.2 +++ b/src/Pure/Thy/html.ML	Thu Feb 21 21:31:52 2008 +0100
     4.3 @@ -314,7 +314,7 @@
     4.4    \<html>\n\
     4.5    \<head>\n\
     4.6    \<meta http-equiv=\"Content-Type\" content=\"text/html; charset=" ^ ! charset ^ "\">\n\
     4.7 -  \<title>" ^ plain (title ^ " (" ^ version ^ ")") ^ "</title>\n\
     4.8 +  \<title>" ^ plain (title ^ " (" ^ Distribution.version ^ ")") ^ "</title>\n\
     4.9    \<link rel=\"stylesheet\" type=\"text/css\" href=\"isabelle.css\">\n\
    4.10    \</head>\n\
    4.11    \\n\