# HG changeset patch
# User wenzelm
# Date 1406210096 -7200
# Node ID a43898f76ae9c4a7ed4b6834ae3601516dd3a898
# Parent  5f451a141581373dc689ed2e953a0dbf4ed500dd
further distinction of Isabelle distribution: alert for identified release candidates;

diff -r 5f451a141581 -r a43898f76ae9 Admin/lib/Tools/makedist
--- a/Admin/lib/Tools/makedist	Thu Jul 24 15:13:37 2014 +0200
+++ b/Admin/lib/Tools/makedist	Thu Jul 24 15:54:56 2014 +0200
@@ -23,6 +23,7 @@
   echo "Usage: isabelle $PRG [OPTIONS] [VERSION]"
   echo
   echo "  Options are:"
+  echo "    -O           official release (not release-candidate)"
   echo "    -d DIR       global directory prefix (default: \"$DISTPREFIX\")"
   echo "    -j INT       maximum number of parallel jobs (default 1)"
   echo "    -r RELEASE   proper release with name"
@@ -53,12 +54,16 @@
 
 # options
 
+OFFICIAL_RELEASE="false"
 JOBS=""
 RELEASE=""
 
 while getopts "d:j:r:" OPT
 do
   case "$OPT" in
+    O)
+      OFFICIAL_RELEASE="true"
+      ;;
     d)
       DISTPREFIX="$OPTARG"
       ;;
@@ -143,14 +148,23 @@
     echo "This is a snapshot of Isabelle/${IDENT} from the repository."
     echo
   } >ANNOUNCE
+fi
+
+if [ -n "$RELEASE" -a "$OFFICIAL_RELEASE" = true ]; then
+  IS_OFFICIAL="true"
 else
-  perl -pi -e "s,val is_official = false,val is_official = true,g" src/Pure/ROOT.ML
+  IS_OFFICIAL="false"
 fi
 
+perl -pi \
+  -e "s,val is_identified = false,val is_identified = true,g" \
+  -e "s,val is_official = false,val is_official = ${IS_OFFICIAL},g" \
+  src/Pure/ROOT.ML src/Pure/ROOT.scala
+
 perl -pi -e "s,ISABELLE_ID=\"\",ISABELLE_ID=\"$IDENT\",g" lib/scripts/getsettings
 perl -pi -e "s,ISABELLE_IDENTIFIER=\"\",ISABELLE_IDENTIFIER=\"$DISTNAME\",g" lib/scripts/getsettings
 perl -pi -e "s,{ISABELLE},$DISTNAME,g" lib/html/library_index_header.template
-perl -pi -e "s,unidentified repository version,$DISTVERSION,g" src/Pure/ROOT.ML lib/Tools/version
+perl -pi -e "s,unidentified repository version,$DISTVERSION,g" src/Pure/ROOT.ML src/Pure/ROOT.scala lib/Tools/version
 perl -pi -e "s,some unidentified repository version of Isabelle,$DISTVERSION,g" README
 
 mkdir -p contrib
diff -r 5f451a141581 -r a43898f76ae9 src/Pure/PIDE/session.ML
--- a/src/Pure/PIDE/session.ML	Thu Jul 24 15:13:37 2014 +0200
+++ b/src/Pure/PIDE/session.ML	Thu Jul 24 15:54:56 2014 +0200
@@ -26,7 +26,7 @@
 fun name () = "Isabelle/" ^ #name (! session);
 
 fun welcome () =
-  if Distribution.is_official then
+  if Distribution.is_identified then
     "Welcome to " ^ name () ^ " (" ^ Distribution.version ^ ")"
   else "Unofficial version of " ^ name () ^ " (" ^ Distribution.version ^ ")";
 
diff -r 5f451a141581 -r a43898f76ae9 src/Pure/ROOT.ML
--- a/src/Pure/ROOT.ML	Thu Jul 24 15:13:37 2014 +0200
+++ b/src/Pure/ROOT.ML	Thu Jul 24 15:54:56 2014 +0200
@@ -5,6 +5,7 @@
 structure Distribution =     (*filled-in by makedist*)
 struct
   val version = "unidentified repository version";
+  val is_identified = false;
   val is_official = false;
 end;
 
diff -r 5f451a141581 -r a43898f76ae9 src/Pure/ROOT.scala
--- a/src/Pure/ROOT.scala	Thu Jul 24 15:13:37 2014 +0200
+++ b/src/Pure/ROOT.scala	Thu Jul 24 15:54:56 2014 +0200
@@ -7,5 +7,11 @@
 
 package object isabelle extends isabelle.Basic_Library
 {
+  object Distribution     /*filled-in by makedist*/
+  {
+    val version = "unidentified repository version"
+    val is_identified = false
+    val is_official = false
+  }
 }
 
diff -r 5f451a141581 -r a43898f76ae9 src/Tools/jEdit/src/plugin.scala
--- a/src/Tools/jEdit/src/plugin.scala	Thu Jul 24 15:13:37 2014 +0200
+++ b/src/Tools/jEdit/src/plugin.scala	Thu Jul 24 15:54:56 2014 +0200
@@ -309,6 +309,13 @@
         case msg: EditorStarted =>
           PIDE.session.start("Isabelle", Isabelle_Logic.session_args())
 
+          if (Distribution.is_identified && !Distribution.is_official) {
+            GUI.warning_dialog(jEdit.getActiveView, "Isabelle release candidate for testing",
+              "This is " + Distribution.version +".",
+              "It is for testing only, not for production use.")
+          }
+
+
         case msg: BufferUpdate
         if msg.getWhat == BufferUpdate.LOADED ||
           msg.getWhat == BufferUpdate.PROPERTIES_CHANGED ||