--- 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
--- 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
--- 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
--- 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
--- 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
--- 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)
-------------------------------------
--- 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 {*
--- 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 *}
--- 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 {*
--- 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"
--- 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);
--- 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 ^ ")";
--- 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
//}}}
--- 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;
--- /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
+ }
+}
+
--- 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"
--- 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
-{
-}
-
--- 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 ||