1.1 --- a/Admin/components/components.sha1 Thu Jul 24 13:01:49 2014 +0200
1.2 +++ b/Admin/components/components.sha1 Thu Jul 24 17:58:29 2014 +0200
1.3 @@ -79,6 +79,7 @@
1.4 d4688ddaf83037ca43b5bf271325fc53ae70e3aa scala-2.10.4.tar.gz
1.5 44d12297a78988ffd34363535e6a8e0d94c1d8b5 scala-2.11.0.tar.gz
1.6 14f20de82b25215a5e055631fb147356400625e6 scala-2.11.1.tar.gz
1.7 +4fe9590d08e55760b86755d3fab750e90ac6c380 scala-2.11.2.tar.gz
1.8 b447017e81600cc5e30dd61b5d4962f6da01aa80 scala-2.8.1.final.tar.gz
1.9 5659440f6b86db29f0c9c0de7249b7e24a647126 scala-2.9.2.tar.gz
1.10 43b5afbcad575ab6817d2289756ca22fd2ef43a9 spass-3.8ds.tar.gz
2.1 --- a/Admin/components/main Thu Jul 24 13:01:49 2014 +0200
2.2 +++ b/Admin/components/main Thu Jul 24 17:58:29 2014 +0200
2.3 @@ -9,7 +9,7 @@
2.4 jortho-1.0-2
2.5 kodkodi-1.5.2
2.6 polyml-5.5.2
2.7 -scala-2.11.1
2.8 +scala-2.11.2
2.9 spass-3.8ds
2.10 z3-3.2-1
2.11 z3-4.3.2pre-1
3.1 --- a/Admin/isatest/settings/mac-poly64-M4 Thu Jul 24 13:01:49 2014 +0200
3.2 +++ b/Admin/isatest/settings/mac-poly64-M4 Thu Jul 24 17:58:29 2014 +0200
3.3 @@ -8,7 +8,8 @@
3.4 ML_HOME="$POLYML_HOME/$ML_PLATFORM"
3.5 ML_OPTIONS="-H 2000 --gcthreads 4"
3.6
3.7 -ISABELLE_GHC=ghc
3.8 +#FIXME disabled due to polyml-5.4.1 compiler crash in Quickcheck_Lattice_Examples.thy
3.9 +#ISABELLE_GHC=ghc
3.10
3.11 ISABELLE_HOME_USER=~/isabelle-mac-poly64-M4
3.12
4.1 --- a/Admin/isatest/settings/mac-poly64-M8 Thu Jul 24 13:01:49 2014 +0200
4.2 +++ b/Admin/isatest/settings/mac-poly64-M8 Thu Jul 24 17:58:29 2014 +0200
4.3 @@ -8,7 +8,8 @@
4.4 ML_HOME="$POLYML_HOME/$ML_PLATFORM"
4.5 ML_OPTIONS="-H 2000 --gcthreads 8"
4.6
4.7 -ISABELLE_GHC=ghc
4.8 +#FIXME disabled due to polyml-5.4.1 compiler crash in Quickcheck_Lattice_Examples.thy
4.9 +#ISABELLE_GHC=ghc
4.10
4.11 ISABELLE_HOME_USER=~/isabelle-mac-poly64-M8
4.12
5.1 --- a/Admin/lib/Tools/makedist Thu Jul 24 13:01:49 2014 +0200
5.2 +++ b/Admin/lib/Tools/makedist Thu Jul 24 17:58:29 2014 +0200
5.3 @@ -23,6 +23,7 @@
5.4 echo "Usage: isabelle $PRG [OPTIONS] [VERSION]"
5.5 echo
5.6 echo " Options are:"
5.7 + echo " -O official release (not release-candidate)"
5.8 echo " -d DIR global directory prefix (default: \"$DISTPREFIX\")"
5.9 echo " -j INT maximum number of parallel jobs (default 1)"
5.10 echo " -r RELEASE proper release with name"
5.11 @@ -53,12 +54,16 @@
5.12
5.13 # options
5.14
5.15 +OFFICIAL_RELEASE="false"
5.16 JOBS=""
5.17 RELEASE=""
5.18
5.19 while getopts "d:j:r:" OPT
5.20 do
5.21 case "$OPT" in
5.22 + O)
5.23 + OFFICIAL_RELEASE="true"
5.24 + ;;
5.25 d)
5.26 DISTPREFIX="$OPTARG"
5.27 ;;
5.28 @@ -143,14 +148,23 @@
5.29 echo "This is a snapshot of Isabelle/${IDENT} from the repository."
5.30 echo
5.31 } >ANNOUNCE
5.32 +fi
5.33 +
5.34 +if [ -n "$RELEASE" -a "$OFFICIAL_RELEASE" = true ]; then
5.35 + IS_OFFICIAL="true"
5.36 else
5.37 - perl -pi -e "s,val is_official = false,val is_official = true,g" src/Pure/ROOT.ML
5.38 + IS_OFFICIAL="false"
5.39 fi
5.40
5.41 +perl -pi \
5.42 + -e "s,val is_identified = false,val is_identified = true,g;" \
5.43 + -e "s,val is_official = false,val is_official = ${IS_OFFICIAL},g;" \
5.44 + src/Pure/ROOT.ML src/Pure/ROOT.scala
5.45 +
5.46 perl -pi -e "s,ISABELLE_ID=\"\",ISABELLE_ID=\"$IDENT\",g" lib/scripts/getsettings
5.47 perl -pi -e "s,ISABELLE_IDENTIFIER=\"\",ISABELLE_IDENTIFIER=\"$DISTNAME\",g" lib/scripts/getsettings
5.48 perl -pi -e "s,{ISABELLE},$DISTNAME,g" lib/html/library_index_header.template
5.49 -perl -pi -e "s,unidentified repository version,$DISTVERSION,g" src/Pure/ROOT.ML lib/Tools/version
5.50 +perl -pi -e "s,unidentified repository version,$DISTVERSION,g" src/Pure/ROOT.ML src/Pure/ROOT.scala lib/Tools/version
5.51 perl -pi -e "s,some unidentified repository version of Isabelle,$DISTVERSION,g" README
5.52
5.53 mkdir -p contrib
6.1 --- a/NEWS Thu Jul 24 13:01:49 2014 +0200
6.2 +++ b/NEWS Thu Jul 24 17:58:29 2014 +0200
6.3 @@ -64,7 +64,7 @@
6.4
6.5 *** Prover IDE -- Isabelle/Scala/jEdit ***
6.6
6.7 -* Improved Document panel: simplied interaction where every single
6.8 +* Improved Document panel: simplified interaction where every single
6.9 mouse click (re)opens document via desktop environment or as jEdit
6.10 buffer.
6.11
6.12 @@ -596,7 +596,7 @@
6.13
6.14 INCOMPATIBILITY.
6.15
6.16 -* Fact collections add_ac and mult_ac are considered old-fashined.
6.17 +* Fact collections add_ac and mult_ac are considered old-fashioned.
6.18 Prefer ac_simps instead, or specify rules
6.19 (add|mult).(assoc|commute|left_commute) individually.
6.20
6.21 @@ -1048,7 +1048,6 @@
6.22 of TeX Live from Cygwin.
6.23
6.24
6.25 -
6.26 New in Isabelle2013-2 (December 2013)
6.27 -------------------------------------
6.28
7.1 --- a/src/HOL/Library/Quickcheck_Types.thy Thu Jul 24 13:01:49 2014 +0200
7.2 +++ b/src/HOL/Library/Quickcheck_Types.thy Thu Jul 24 17:58:29 2014 +0200
7.3 @@ -4,7 +4,7 @@
7.4 *)
7.5
7.6 theory Quickcheck_Types
7.7 -imports "../Main"
7.8 +imports Main
7.9 begin
7.10
7.11 text {*
8.1 --- a/src/HOL/Quickcheck_Examples/Completeness.thy Thu Jul 24 13:01:49 2014 +0200
8.2 +++ b/src/HOL/Quickcheck_Examples/Completeness.thy Thu Jul 24 17:58:29 2014 +0200
8.3 @@ -6,7 +6,7 @@
8.4 header {* Proving completeness of exhaustive generators *}
8.5
8.6 theory Completeness
8.7 -imports "../Main"
8.8 +imports Main
8.9 begin
8.10
8.11 subsection {* Preliminaries *}
9.1 --- a/src/HOL/Quickcheck_Examples/Quickcheck_Examples.thy Thu Jul 24 13:01:49 2014 +0200
9.2 +++ b/src/HOL/Quickcheck_Examples/Quickcheck_Examples.thy Thu Jul 24 17:58:29 2014 +0200
9.3 @@ -6,7 +6,7 @@
9.4 header {* Examples for the 'quickcheck' command *}
9.5
9.6 theory Quickcheck_Examples
9.7 -imports "../Complex_Main" "~~/src/HOL/Library/Dlist" "~~/src/HOL/Library/DAList_Multiset"
9.8 +imports Complex_Main "~~/src/HOL/Library/Dlist" "~~/src/HOL/Library/DAList_Multiset"
9.9 begin
9.10
9.11 text {*
10.1 --- a/src/HOL/ROOT Thu Jul 24 13:01:49 2014 +0200
10.2 +++ b/src/HOL/ROOT Thu Jul 24 17:58:29 2014 +0200
10.3 @@ -38,6 +38,7 @@
10.4 Product_Lexorder
10.5 Product_Order
10.6 Finite_Lattice
10.7 + Quickcheck_Types
10.8 (*data refinements and dependent applications*)
10.9 AList_Mapping
10.10 Code_Binary_Nat
10.11 @@ -52,7 +53,6 @@
10.12 (*legacy tools*)
10.13 Refute
10.14 Old_Recdef
10.15 - Quickcheck_Types
10.16 theories [condition = ISABELLE_FULL_TEST]
10.17 Sum_of_Squares_Remote
10.18 document_files "root.bib" "root.tex"
11.1 --- a/src/Pure/PIDE/document.ML Thu Jul 24 13:01:49 2014 +0200
11.2 +++ b/src/Pure/PIDE/document.ML Thu Jul 24 17:58:29 2014 +0200
11.3 @@ -72,7 +72,7 @@
11.4 visible_last = try List.last command_ids,
11.5 overlays = Inttab.make_list overlays};
11.6
11.7 -val no_header = ("", Thy_Header.make ("", Position.none) [] [], []);
11.8 +val no_header: node_header = ("", Thy_Header.make ("", Position.none) [] [], []);
11.9 val no_perspective = make_perspective (false, [], []);
11.10
11.11 val empty_node = make_node (no_header, no_perspective, Entries.empty, NONE);
12.1 --- a/src/Pure/PIDE/session.ML Thu Jul 24 13:01:49 2014 +0200
12.2 +++ b/src/Pure/PIDE/session.ML Thu Jul 24 17:58:29 2014 +0200
12.3 @@ -26,7 +26,7 @@
12.4 fun name () = "Isabelle/" ^ #name (! session);
12.5
12.6 fun welcome () =
12.7 - if Distribution.is_official then
12.8 + if Distribution.is_identified then
12.9 "Welcome to " ^ name () ^ " (" ^ Distribution.version ^ ")"
12.10 else "Unofficial version of " ^ name () ^ " (" ^ Distribution.version ^ ")";
12.11
13.1 --- a/src/Pure/PIDE/session.scala Thu Jul 24 13:01:49 2014 +0200
13.2 +++ b/src/Pure/PIDE/session.scala Thu Jul 24 17:58:29 2014 +0200
13.3 @@ -562,6 +562,9 @@
13.4 if (global_state.value.is_assigned(change.previous))
13.5 handle_change(change)
13.6 else postponed_changes.store(change)
13.7 +
13.8 + case bad =>
13.9 + if (verbose) Output.warning("Ignoring bad message: " + bad.toString)
13.10 }
13.11 true
13.12 //}}}
14.1 --- a/src/Pure/ROOT.ML Thu Jul 24 13:01:49 2014 +0200
14.2 +++ b/src/Pure/ROOT.ML Thu Jul 24 17:58:29 2014 +0200
14.3 @@ -5,6 +5,7 @@
14.4 structure Distribution = (*filled-in by makedist*)
14.5 struct
14.6 val version = "unidentified repository version";
14.7 + val is_identified = false;
14.8 val is_official = false;
14.9 end;
14.10
15.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
15.2 +++ b/src/Pure/ROOT.scala Thu Jul 24 17:58:29 2014 +0200
15.3 @@ -0,0 +1,17 @@
15.4 +/* Title: Pure/ROOT.scala
15.5 + Module: PIDE
15.6 + Author: Makarius
15.7 +
15.8 +Root of isabelle package.
15.9 +*/
15.10 +
15.11 +package object isabelle extends isabelle.Basic_Library
15.12 +{
15.13 + object Distribution /*filled-in by makedist*/
15.14 + {
15.15 + val version = "unidentified repository version"
15.16 + val is_identified = false
15.17 + val is_official = false
15.18 + }
15.19 +}
15.20 +
16.1 --- a/src/Pure/build-jars Thu Jul 24 13:01:49 2014 +0200
16.2 +++ b/src/Pure/build-jars Thu Jul 24 17:58:29 2014 +0200
16.3 @@ -16,6 +16,14 @@
16.4 Concurrent/mailbox.scala
16.5 Concurrent/simple_thread.scala
16.6 Concurrent/synchronized.scala
16.7 + GUI/color_value.scala
16.8 + GUI/gui.scala
16.9 + GUI/gui_thread.scala
16.10 + GUI/html5_panel.scala
16.11 + GUI/jfx_thread.scala
16.12 + GUI/popup.scala
16.13 + GUI/system_dialog.scala
16.14 + GUI/wrap_panel.scala
16.15 General/antiquote.scala
16.16 General/bytes.scala
16.17 General/completion.scala
16.18 @@ -36,18 +44,10 @@
16.19 General/symbol.scala
16.20 General/time.scala
16.21 General/timing.scala
16.22 + General/untyped.scala
16.23 General/url.scala
16.24 - General/untyped.scala
16.25 General/word.scala
16.26 General/xz_file.scala
16.27 - GUI/color_value.scala
16.28 - GUI/gui.scala
16.29 - GUI/gui_thread.scala
16.30 - GUI/html5_panel.scala
16.31 - GUI/jfx_thread.scala
16.32 - GUI/popup.scala
16.33 - GUI/system_dialog.scala
16.34 - GUI/wrap_panel.scala
16.35 Isar/keyword.scala
16.36 Isar/outer_syntax.scala
16.37 Isar/parse.scala
16.38 @@ -67,6 +67,7 @@
16.39 PIDE/text.scala
16.40 PIDE/xml.scala
16.41 PIDE/yxml.scala
16.42 + ROOT.scala
16.43 System/command_line.scala
16.44 System/invoke_scala.scala
16.45 System/isabelle_charset.scala
16.46 @@ -83,10 +84,10 @@
16.47 Thy/thy_header.scala
16.48 Thy/thy_info.scala
16.49 Thy/thy_syntax.scala
16.50 + Tools/build.scala
16.51 + Tools/build_console.scala
16.52 + Tools/build_doc.scala
16.53 Tools/check_source.scala
16.54 - Tools/build.scala
16.55 - Tools/build_doc.scala
16.56 - Tools/build_console.scala
16.57 Tools/doc.scala
16.58 Tools/keywords.scala
16.59 Tools/main.scala
16.60 @@ -95,7 +96,6 @@
16.61 Tools/simplifier_trace.scala
16.62 Tools/task_statistics.scala
16.63 library.scala
16.64 - package.scala
16.65 term.scala
16.66 term_xml.scala
16.67 "../Tools/Graphview/src/graph_panel.scala"
17.1 --- a/src/Pure/package.scala Thu Jul 24 13:01:49 2014 +0200
17.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
17.3 @@ -1,11 +0,0 @@
17.4 -/* Title: Pure/package.scala
17.5 - Module: PIDE
17.6 - Author: Makarius
17.7 -
17.8 -Toplevel isabelle package.
17.9 -*/
17.10 -
17.11 -package object isabelle extends isabelle.Basic_Library
17.12 -{
17.13 -}
17.14 -
18.1 --- a/src/Tools/jEdit/src/plugin.scala Thu Jul 24 13:01:49 2014 +0200
18.2 +++ b/src/Tools/jEdit/src/plugin.scala Thu Jul 24 17:58:29 2014 +0200
18.3 @@ -309,6 +309,13 @@
18.4 case msg: EditorStarted =>
18.5 PIDE.session.start("Isabelle", Isabelle_Logic.session_args())
18.6
18.7 + if (Distribution.is_identified && !Distribution.is_official) {
18.8 + GUI.warning_dialog(jEdit.getActiveView, "Isabelle release candidate for testing",
18.9 + "This is " + Distribution.version +".",
18.10 + "It is for testing only, not for production use.")
18.11 + }
18.12 +
18.13 +
18.14 case msg: BufferUpdate
18.15 if msg.getWhat == BufferUpdate.LOADED ||
18.16 msg.getWhat == BufferUpdate.PROPERTIES_CHANGED ||