# HG changeset patch
# User wenzelm
# Date 1406217509 -7200
# Node ID 4b247a7586c92324bf4746a3ad760822129f2135
# Parent  5bc43a73d768d00b67b3ff0487d75ba734abbd14# Parent  e7fe592ee089357e596cd6249acdb077b985e21a
merged

diff -r 5bc43a73d768 -r 4b247a7586c9 Admin/components/components.sha1
--- a/Admin/components/components.sha1	Thu Jul 24 13:01:49 2014 +0200
+++ b/Admin/components/components.sha1	Thu Jul 24 17:58:29 2014 +0200
@@ -79,6 +79,7 @@
 d4688ddaf83037ca43b5bf271325fc53ae70e3aa  scala-2.10.4.tar.gz
 44d12297a78988ffd34363535e6a8e0d94c1d8b5  scala-2.11.0.tar.gz
 14f20de82b25215a5e055631fb147356400625e6  scala-2.11.1.tar.gz
+4fe9590d08e55760b86755d3fab750e90ac6c380  scala-2.11.2.tar.gz
 b447017e81600cc5e30dd61b5d4962f6da01aa80  scala-2.8.1.final.tar.gz
 5659440f6b86db29f0c9c0de7249b7e24a647126  scala-2.9.2.tar.gz
 43b5afbcad575ab6817d2289756ca22fd2ef43a9  spass-3.8ds.tar.gz
diff -r 5bc43a73d768 -r 4b247a7586c9 Admin/components/main
--- a/Admin/components/main	Thu Jul 24 13:01:49 2014 +0200
+++ b/Admin/components/main	Thu Jul 24 17:58:29 2014 +0200
@@ -9,7 +9,7 @@
 jortho-1.0-2
 kodkodi-1.5.2
 polyml-5.5.2
-scala-2.11.1
+scala-2.11.2
 spass-3.8ds
 z3-3.2-1
 z3-4.3.2pre-1
diff -r 5bc43a73d768 -r 4b247a7586c9 Admin/isatest/settings/mac-poly64-M4
--- a/Admin/isatest/settings/mac-poly64-M4	Thu Jul 24 13:01:49 2014 +0200
+++ b/Admin/isatest/settings/mac-poly64-M4	Thu Jul 24 17:58:29 2014 +0200
@@ -8,7 +8,8 @@
   ML_HOME="$POLYML_HOME/$ML_PLATFORM"
   ML_OPTIONS="-H 2000 --gcthreads 4"
 
-ISABELLE_GHC=ghc
+#FIXME disabled due to polyml-5.4.1 compiler crash in Quickcheck_Lattice_Examples.thy
+#ISABELLE_GHC=ghc
 
 ISABELLE_HOME_USER=~/isabelle-mac-poly64-M4
 
diff -r 5bc43a73d768 -r 4b247a7586c9 Admin/isatest/settings/mac-poly64-M8
--- a/Admin/isatest/settings/mac-poly64-M8	Thu Jul 24 13:01:49 2014 +0200
+++ b/Admin/isatest/settings/mac-poly64-M8	Thu Jul 24 17:58:29 2014 +0200
@@ -8,7 +8,8 @@
   ML_HOME="$POLYML_HOME/$ML_PLATFORM"
   ML_OPTIONS="-H 2000 --gcthreads 8"
 
-ISABELLE_GHC=ghc
+#FIXME disabled due to polyml-5.4.1 compiler crash in Quickcheck_Lattice_Examples.thy
+#ISABELLE_GHC=ghc
 
 ISABELLE_HOME_USER=~/isabelle-mac-poly64-M8
 
diff -r 5bc43a73d768 -r 4b247a7586c9 Admin/lib/Tools/makedist
--- a/Admin/lib/Tools/makedist	Thu Jul 24 13:01:49 2014 +0200
+++ b/Admin/lib/Tools/makedist	Thu Jul 24 17:58:29 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 5bc43a73d768 -r 4b247a7586c9 NEWS
--- a/NEWS	Thu Jul 24 13:01:49 2014 +0200
+++ b/NEWS	Thu Jul 24 17:58:29 2014 +0200
@@ -64,7 +64,7 @@
 
 *** Prover IDE -- Isabelle/Scala/jEdit ***
 
-* Improved Document panel: simplied interaction where every single
+* Improved Document panel: simplified interaction where every single
 mouse click (re)opens document via desktop environment or as jEdit
 buffer.
 
@@ -596,7 +596,7 @@
 
 INCOMPATIBILITY.
 
-* Fact collections add_ac and mult_ac are considered old-fashined.
+* Fact collections add_ac and mult_ac are considered old-fashioned.
 Prefer ac_simps instead, or specify rules
 (add|mult).(assoc|commute|left_commute) individually.
 
@@ -1048,7 +1048,6 @@
 of TeX Live from Cygwin.
 
 
-
 New in Isabelle2013-2 (December 2013)
 -------------------------------------
 
diff -r 5bc43a73d768 -r 4b247a7586c9 src/HOL/Library/Quickcheck_Types.thy
--- a/src/HOL/Library/Quickcheck_Types.thy	Thu Jul 24 13:01:49 2014 +0200
+++ b/src/HOL/Library/Quickcheck_Types.thy	Thu Jul 24 17:58:29 2014 +0200
@@ -4,7 +4,7 @@
 *)
 
 theory Quickcheck_Types
-imports "../Main"
+imports Main
 begin
 
 text {*
diff -r 5bc43a73d768 -r 4b247a7586c9 src/HOL/Quickcheck_Examples/Completeness.thy
--- a/src/HOL/Quickcheck_Examples/Completeness.thy	Thu Jul 24 13:01:49 2014 +0200
+++ b/src/HOL/Quickcheck_Examples/Completeness.thy	Thu Jul 24 17:58:29 2014 +0200
@@ -6,7 +6,7 @@
 header {* Proving completeness of exhaustive generators *}
 
 theory Completeness
-imports "../Main"
+imports Main
 begin
 
 subsection {* Preliminaries *}
diff -r 5bc43a73d768 -r 4b247a7586c9 src/HOL/Quickcheck_Examples/Quickcheck_Examples.thy
--- a/src/HOL/Quickcheck_Examples/Quickcheck_Examples.thy	Thu Jul 24 13:01:49 2014 +0200
+++ b/src/HOL/Quickcheck_Examples/Quickcheck_Examples.thy	Thu Jul 24 17:58:29 2014 +0200
@@ -6,7 +6,7 @@
 header {* Examples for the 'quickcheck' command *}
 
 theory Quickcheck_Examples
-imports "../Complex_Main" "~~/src/HOL/Library/Dlist" "~~/src/HOL/Library/DAList_Multiset"
+imports Complex_Main "~~/src/HOL/Library/Dlist" "~~/src/HOL/Library/DAList_Multiset"
 begin
 
 text {*
diff -r 5bc43a73d768 -r 4b247a7586c9 src/HOL/ROOT
--- a/src/HOL/ROOT	Thu Jul 24 13:01:49 2014 +0200
+++ b/src/HOL/ROOT	Thu Jul 24 17:58:29 2014 +0200
@@ -38,6 +38,7 @@
     Product_Lexorder
     Product_Order
     Finite_Lattice
+    Quickcheck_Types
     (*data refinements and dependent applications*)
     AList_Mapping
     Code_Binary_Nat
@@ -52,7 +53,6 @@
     (*legacy tools*)
     Refute
     Old_Recdef
-    Quickcheck_Types
   theories [condition = ISABELLE_FULL_TEST]
     Sum_of_Squares_Remote
   document_files "root.bib" "root.tex"
diff -r 5bc43a73d768 -r 4b247a7586c9 src/Pure/PIDE/document.ML
--- a/src/Pure/PIDE/document.ML	Thu Jul 24 13:01:49 2014 +0200
+++ b/src/Pure/PIDE/document.ML	Thu Jul 24 17:58:29 2014 +0200
@@ -72,7 +72,7 @@
   visible_last = try List.last command_ids,
   overlays = Inttab.make_list overlays};
 
-val no_header = ("", Thy_Header.make ("", Position.none) [] [], []);
+val no_header: node_header = ("", Thy_Header.make ("", Position.none) [] [], []);
 val no_perspective = make_perspective (false, [], []);
 
 val empty_node = make_node (no_header, no_perspective, Entries.empty, NONE);
diff -r 5bc43a73d768 -r 4b247a7586c9 src/Pure/PIDE/session.ML
--- a/src/Pure/PIDE/session.ML	Thu Jul 24 13:01:49 2014 +0200
+++ b/src/Pure/PIDE/session.ML	Thu Jul 24 17:58:29 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 5bc43a73d768 -r 4b247a7586c9 src/Pure/PIDE/session.scala
--- a/src/Pure/PIDE/session.scala	Thu Jul 24 13:01:49 2014 +0200
+++ b/src/Pure/PIDE/session.scala	Thu Jul 24 17:58:29 2014 +0200
@@ -562,6 +562,9 @@
             if (global_state.value.is_assigned(change.previous))
               handle_change(change)
             else postponed_changes.store(change)
+
+          case bad =>
+            if (verbose) Output.warning("Ignoring bad message: " + bad.toString)
         }
         true
         //}}}
diff -r 5bc43a73d768 -r 4b247a7586c9 src/Pure/ROOT.ML
--- a/src/Pure/ROOT.ML	Thu Jul 24 13:01:49 2014 +0200
+++ b/src/Pure/ROOT.ML	Thu Jul 24 17:58:29 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 5bc43a73d768 -r 4b247a7586c9 src/Pure/ROOT.scala
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/ROOT.scala	Thu Jul 24 17:58:29 2014 +0200
@@ -0,0 +1,17 @@
+/*  Title:      Pure/ROOT.scala
+    Module:     PIDE
+    Author:     Makarius
+
+Root of isabelle package.
+*/
+
+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 5bc43a73d768 -r 4b247a7586c9 src/Pure/build-jars
--- a/src/Pure/build-jars	Thu Jul 24 13:01:49 2014 +0200
+++ b/src/Pure/build-jars	Thu Jul 24 17:58:29 2014 +0200
@@ -16,6 +16,14 @@
   Concurrent/mailbox.scala
   Concurrent/simple_thread.scala
   Concurrent/synchronized.scala
+  GUI/color_value.scala
+  GUI/gui.scala
+  GUI/gui_thread.scala
+  GUI/html5_panel.scala
+  GUI/jfx_thread.scala
+  GUI/popup.scala
+  GUI/system_dialog.scala
+  GUI/wrap_panel.scala
   General/antiquote.scala
   General/bytes.scala
   General/completion.scala
@@ -36,18 +44,10 @@
   General/symbol.scala
   General/time.scala
   General/timing.scala
+  General/untyped.scala
   General/url.scala
-  General/untyped.scala
   General/word.scala
   General/xz_file.scala
-  GUI/color_value.scala
-  GUI/gui.scala
-  GUI/gui_thread.scala
-  GUI/html5_panel.scala
-  GUI/jfx_thread.scala
-  GUI/popup.scala
-  GUI/system_dialog.scala
-  GUI/wrap_panel.scala
   Isar/keyword.scala
   Isar/outer_syntax.scala
   Isar/parse.scala
@@ -67,6 +67,7 @@
   PIDE/text.scala
   PIDE/xml.scala
   PIDE/yxml.scala
+  ROOT.scala
   System/command_line.scala
   System/invoke_scala.scala
   System/isabelle_charset.scala
@@ -83,10 +84,10 @@
   Thy/thy_header.scala
   Thy/thy_info.scala
   Thy/thy_syntax.scala
+  Tools/build.scala
+  Tools/build_console.scala
+  Tools/build_doc.scala
   Tools/check_source.scala
-  Tools/build.scala
-  Tools/build_doc.scala
-  Tools/build_console.scala
   Tools/doc.scala
   Tools/keywords.scala
   Tools/main.scala
@@ -95,7 +96,6 @@
   Tools/simplifier_trace.scala
   Tools/task_statistics.scala
   library.scala
-  package.scala
   term.scala
   term_xml.scala
   "../Tools/Graphview/src/graph_panel.scala"
diff -r 5bc43a73d768 -r 4b247a7586c9 src/Pure/package.scala
--- a/src/Pure/package.scala	Thu Jul 24 13:01:49 2014 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,11 +0,0 @@
-/*  Title:      Pure/package.scala
-    Module:     PIDE
-    Author:     Makarius
-
-Toplevel isabelle package.
-*/
-
-package object isabelle extends isabelle.Basic_Library
-{
-}
-
diff -r 5bc43a73d768 -r 4b247a7586c9 src/Tools/jEdit/src/plugin.scala
--- a/src/Tools/jEdit/src/plugin.scala	Thu Jul 24 13:01:49 2014 +0200
+++ b/src/Tools/jEdit/src/plugin.scala	Thu Jul 24 17:58:29 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 ||