--- a/Admin/Release/CHECKLIST Mon Oct 24 14:32:07 2016 +0100
+++ b/Admin/Release/CHECKLIST Mon Oct 24 16:16:55 2016 +0200
@@ -36,9 +36,6 @@
- HTML library: check theory dependencies (PDF);
-- test separate compilation of Isabelle/Scala PIDE sources:
- Admin/build jars_test
-
- test Isabelle/jEdit:
. print buffer
. on single-core
--- a/Admin/build Mon Oct 24 14:32:07 2016 +0100
+++ b/Admin/build Mon Oct 24 16:16:55 2016 +0200
@@ -26,7 +26,6 @@
all all modules below
browser graph browser
jars Isabelle/Scala
- jars_test test separate build of jars
jars_fresh fresh build of jars
EOF
@@ -86,7 +85,6 @@
browser) build_browser;;
jars) build_jars;;
jars_fresh) build_jars -f;;
- jars_test) build_jars -t;;
*) fail "Bad module $MODULE"
esac
done
--- a/Admin/components/bundled-windows Mon Oct 24 14:32:07 2016 +0100
+++ b/Admin/components/bundled-windows Mon Oct 24 16:16:55 2016 +0200
@@ -1,3 +1,3 @@
#additional components to be bundled for release
-cygwin-20161022
+cygwin-20161024
windows_app-20150821
--- a/Admin/components/components.sha1 Mon Oct 24 14:32:07 2016 +0100
+++ b/Admin/components/components.sha1 Mon Oct 24 16:16:55 2016 +0200
@@ -26,6 +26,7 @@
056b843d5a3b69ecf8a52c06f2ce6e696dd275f9 cygwin-20151221.tar.gz
44f3a530f727e43a9413226c2423c9ca3e4c0cf5 cygwin-20161002.tar.gz
dd56dd16d861fc6e1a008bf5e9da6f33ed6eb820 cygwin-20161022.tar.gz
+d9ad7aae99d54e3b9813151712eb88a441613f04 cygwin-20161024.tar.gz
0fe549949a025d65d52d6deca30554de8fca3b6e e-1.5.tar.gz
2e293256a134eb8e5b1a283361b15eb812fbfbf1 e-1.6-1.tar.gz
e1919e72416cbd7ac8de5455caba8901acc7b44d e-1.6-2.tar.gz
@@ -102,6 +103,7 @@
b5f7115384c167559211768eb5fe98138864473b jedit_build-20151023.tar.gz
8ba7b6791be788f316427cdcd805daeaa6935190 jedit_build-20151124.tar.gz
c70c5a6c565d435a09a8639f8afd3de360708e1c jedit_build-20160330.tar.gz
+d4e1496c257659cf15458d718f4663cdd95a404e jedit_build-20161024.tar.gz
0bd2bc2d9a491ba5fc8dd99df27c04f11a72e8fa jfreechart-1.0.14-1.tar.gz
8122526f1fc362ddae1a328bdbc2152853186fee jfreechart-1.0.14.tar.gz
c8a19a36adf6cefa779d85f22ded2f4654e68ea5 jortho-1.0-1.tar.gz
--- a/Admin/components/main Mon Oct 24 14:32:07 2016 +0100
+++ b/Admin/components/main Mon Oct 24 16:16:55 2016 +0200
@@ -6,7 +6,7 @@
Haskabelle-2015
isabelle_fonts-20160830
jdk-8u112
-jedit_build-20160330
+jedit_build-20161024
jfreechart-1.0.14-1
jortho-1.0-2
kodkodi-1.5.2
--- a/Admin/lib/Tools/makedist Mon Oct 24 14:32:07 2016 +0100
+++ b/Admin/lib/Tools/makedist Mon Oct 24 16:16:55 2016 +0200
@@ -197,9 +197,9 @@
rm -rf src
mv src.orig src
-rm -rf Admin browser_info heaps
+./bin/isabelle news
-./bin/isabelle java isabelle.NEWS
+rm -rf Admin browser_info heaps
rmdir "$USER_HOME/.isabelle/${DISTNAME}-build"
rmdir "$USER_HOME/.isabelle/${DISTNAME}"
@@ -244,4 +244,3 @@
rm -f Isabelle && ln -sf "$DISTNAME" Isabelle
rm -rf "${DISTNAME}-old"
-
--- a/src/Pure/Admin/build_history.scala Mon Oct 24 14:32:07 2016 +0100
+++ b/src/Pure/Admin/build_history.scala Mon Oct 24 16:16:55 2016 +0200
@@ -173,10 +173,12 @@
if (first_build) {
other_isabelle.resolve_components(verbose)
+
+ if (fresh)
+ Isabelle_System.rm_tree(other_isabelle.isabelle_home + Path.explode("lib/classes"))
other_isabelle.bash(
"env PATH=\"" + File.bash_path(Path.explode("~~/lib/dummy_stty").expand) + ":$PATH\" " +
- "bin/isabelle jedit -b" + (if (fresh) " -f" else ""),
- redirect = true, echo = verbose).check
+ "bin/isabelle jedit -b", redirect = true, echo = verbose).check
Isabelle_System.rm_tree(isabelle_base_log)
}
--- a/src/Pure/Admin/build_release.scala Mon Oct 24 14:32:07 2016 +0100
+++ b/src/Pure/Admin/build_release.scala Mon Oct 24 16:16:55 2016 +0200
@@ -49,6 +49,8 @@
{
/* release info */
+ Isabelle_System.mkdirs(base_dir)
+
val release_info =
{
val date = Date.now()
--- a/src/Pure/Admin/check_sources.scala Mon Oct 24 14:32:07 2016 +0100
+++ b/src/Pure/Admin/check_sources.scala Mon Oct 24 16:16:55 2016 +0200
@@ -41,7 +41,7 @@
Output.warning("CR character" + Position.here(file_pos))
if (Word.bidi_detect(content))
- Output.warning("Bidirectional Unicode text " + Position.here(file_pos))
+ Output.warning("Bidirectional Unicode text" + Position.here(file_pos))
}
def check_hg(root: Path)
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Admin/news.scala Mon Oct 24 16:16:55 2016 +0200
@@ -0,0 +1,37 @@
+/* Title: Pure/Admin/news.scala
+ Author: Makarius
+
+Support for the NEWS file.
+*/
+
+package isabelle
+
+
+object NEWS
+{
+ /* generate HTML version */
+
+ def generate_html()
+ {
+ val target = Path.explode("~~/doc")
+
+ File.write(target + Path.explode("NEWS.html"),
+ HTML.begin_document("NEWS") +
+ "\n<div class=\"source\">\n<pre class=\"source\">" +
+ HTML.output(Symbol.decode(File.read(Path.explode("~~/NEWS")))) +
+ "</pre>\n" +
+ HTML.end_document)
+
+ for (font <- Path.split(Isabelle_System.getenv_strict("ISABELLE_FONTS")))
+ File.copy(font, target)
+
+ File.copy(Path.explode("~~/etc/isabelle.css"), target)
+ }
+
+
+ /* Isabelle tool wrapper */
+
+ val isabelle_tool =
+ Isabelle_Tool("news", "generate HTML version of the NEWS file",
+ _ => generate_html(), admin = true)
+}
--- a/src/Pure/Concurrent/consumer_thread.scala Mon Oct 24 14:32:07 2016 +0100
+++ b/src/Pure/Concurrent/consumer_thread.scala Mon Oct 24 16:16:55 2016 +0200
@@ -1,5 +1,4 @@
/* Title: Pure/Concurrent/consumer_thread.scala
- Module: PIDE
Author: Makarius
Consumer thread with unbounded queueing of requests, and optional
--- a/src/Pure/Concurrent/counter.scala Mon Oct 24 14:32:07 2016 +0100
+++ b/src/Pure/Concurrent/counter.scala Mon Oct 24 16:16:55 2016 +0200
@@ -1,5 +1,4 @@
/* Title: Pure/Concurrent/counter.scala
- Module: PIDE
Author: Makarius
Synchronized counter for unique identifiers < 0.
--- a/src/Pure/Concurrent/event_timer.scala Mon Oct 24 14:32:07 2016 +0100
+++ b/src/Pure/Concurrent/event_timer.scala Mon Oct 24 16:16:55 2016 +0200
@@ -1,5 +1,4 @@
/* Title: Pure/Concurrent/event_timer.scala
- Module: PIDE
Author: Makarius
Initiate event after given point in time.
--- a/src/Pure/Concurrent/future.scala Mon Oct 24 14:32:07 2016 +0100
+++ b/src/Pure/Concurrent/future.scala Mon Oct 24 16:16:55 2016 +0200
@@ -1,5 +1,4 @@
/* Title: Pure/Concurrent/future.scala
- Module: PIDE
Author: Makarius
Value-oriented parallel execution via futures and promises.
--- a/src/Pure/Concurrent/mailbox.scala Mon Oct 24 14:32:07 2016 +0100
+++ b/src/Pure/Concurrent/mailbox.scala Mon Oct 24 16:16:55 2016 +0200
@@ -1,5 +1,4 @@
/* Title: Pure/Concurrent/mailbox.scala
- Module: PIDE
Author: Makarius
Message exchange via mailbox, with multiple senders (non-blocking,
--- a/src/Pure/Concurrent/standard_thread.scala Mon Oct 24 14:32:07 2016 +0100
+++ b/src/Pure/Concurrent/standard_thread.scala Mon Oct 24 16:16:55 2016 +0200
@@ -1,5 +1,4 @@
/* Title: Pure/Concurrent/standard_thread.scala
- Module: PIDE
Author: Makarius
Standard thread operations.
--- a/src/Pure/Concurrent/synchronized.scala Mon Oct 24 14:32:07 2016 +0100
+++ b/src/Pure/Concurrent/synchronized.scala Mon Oct 24 16:16:55 2016 +0200
@@ -1,5 +1,4 @@
/* Title: Pure/Concurrent/synchronized.scala
- Module: PIDE
Author: Makarius
Synchronized variables.
--- a/src/Pure/GUI/color_value.scala Mon Oct 24 14:32:07 2016 +0100
+++ b/src/Pure/GUI/color_value.scala Mon Oct 24 16:16:55 2016 +0200
@@ -1,5 +1,4 @@
/* Title: Pure/GUI/color_value.scala
- Module: PIDE-GUI
Author: Makarius
Cached color values.
--- a/src/Pure/GUI/gui_thread.scala Mon Oct 24 14:32:07 2016 +0100
+++ b/src/Pure/GUI/gui_thread.scala Mon Oct 24 16:16:55 2016 +0200
@@ -1,5 +1,4 @@
/* Title: Pure/GUI/gui_thread.scala
- Module: PIDE-GUI
Author: Makarius
Evaluation within the GUI thread (for AWT/Swing).
--- a/src/Pure/GUI/popup.scala Mon Oct 24 14:32:07 2016 +0100
+++ b/src/Pure/GUI/popup.scala Mon Oct 24 16:16:55 2016 +0200
@@ -1,5 +1,4 @@
/* Title: Pure/GUI/popup.scala
- Module: PIDE-GUI
Author: Makarius
Popup within layered pane.
--- a/src/Pure/General/bytes.scala Mon Oct 24 14:32:07 2016 +0100
+++ b/src/Pure/General/bytes.scala Mon Oct 24 16:16:55 2016 +0200
@@ -1,5 +1,4 @@
/* Title: Pure/General/bytes.scala
- Module: PIDE
Author: Makarius
Immutable byte vectors versus UTF8 strings.
--- a/src/Pure/General/exn.scala Mon Oct 24 14:32:07 2016 +0100
+++ b/src/Pure/General/exn.scala Mon Oct 24 16:16:55 2016 +0200
@@ -1,5 +1,4 @@
/* Title: Pure/General/exn.scala
- Module: PIDE
Author: Makarius
Support for exceptions (arbitrary throwables).
--- a/src/Pure/General/graph.scala Mon Oct 24 14:32:07 2016 +0100
+++ b/src/Pure/General/graph.scala Mon Oct 24 16:16:55 2016 +0200
@@ -1,5 +1,4 @@
/* Title: Pure/General/graph.scala
- Module: PIDE
Author: Makarius
Directed graphs.
--- a/src/Pure/General/linear_set.scala Mon Oct 24 14:32:07 2016 +0100
+++ b/src/Pure/General/linear_set.scala Mon Oct 24 16:16:55 2016 +0200
@@ -1,5 +1,4 @@
/* Title: Pure/General/linear_set.scala
- Module: PIDE
Author: Makarius
Author: Fabian Immler, TU Munich
--- a/src/Pure/General/multi_map.scala Mon Oct 24 14:32:07 2016 +0100
+++ b/src/Pure/General/multi_map.scala Mon Oct 24 16:16:55 2016 +0200
@@ -1,5 +1,4 @@
/* Title: Pure/General/multi_map.scala
- Module: PIDE
Author: Makarius
Maps with multiple entries per key.
--- a/src/Pure/General/output.scala Mon Oct 24 14:32:07 2016 +0100
+++ b/src/Pure/General/output.scala Mon Oct 24 16:16:55 2016 +0200
@@ -1,5 +1,4 @@
/* Title: Pure/General/output.scala
- Module: PIDE
Author: Makarius
Isabelle output channels.
--- a/src/Pure/General/properties.scala Mon Oct 24 14:32:07 2016 +0100
+++ b/src/Pure/General/properties.scala Mon Oct 24 16:16:55 2016 +0200
@@ -1,5 +1,4 @@
/* Title: Pure/General/properties.scala
- Module: PIDE
Author: Makarius
Property lists.
--- a/src/Pure/General/sha1.scala Mon Oct 24 14:32:07 2016 +0100
+++ b/src/Pure/General/sha1.scala Mon Oct 24 16:16:55 2016 +0200
@@ -1,5 +1,4 @@
/* Title: Pure/General/sha1.scala
- Module: PIDE
Author: Makarius
Digest strings according to SHA-1 (see RFC 3174).
--- a/src/Pure/General/time.scala Mon Oct 24 14:32:07 2016 +0100
+++ b/src/Pure/General/time.scala Mon Oct 24 16:16:55 2016 +0200
@@ -1,5 +1,4 @@
/* Title: Pure/General/time.scala
- Module: PIDE
Author: Makarius
Time based on milliseconds.
--- a/src/Pure/General/untyped.scala Mon Oct 24 14:32:07 2016 +0100
+++ b/src/Pure/General/untyped.scala Mon Oct 24 16:16:55 2016 +0200
@@ -1,5 +1,4 @@
/* Title: Pure/General/untyped.scala
- Module: PIDE
Author: Makarius
Untyped, unscoped, unchecked access to JVM objects.
--- a/src/Pure/General/word.scala Mon Oct 24 14:32:07 2016 +0100
+++ b/src/Pure/General/word.scala Mon Oct 24 16:16:55 2016 +0200
@@ -1,5 +1,4 @@
/* Title: Pure/General/word.scala
- Module: PIDE
Author: Makarius
Support for words within Unicode text.
--- a/src/Pure/PIDE/document_id.scala Mon Oct 24 14:32:07 2016 +0100
+++ b/src/Pure/PIDE/document_id.scala Mon Oct 24 16:16:55 2016 +0200
@@ -1,5 +1,4 @@
/* Title: Pure/PIDE/document_id.scala
- Module: PIDE
Author: Makarius
Unique identifiers for document structure.
--- a/src/Pure/PIDE/markup.scala Mon Oct 24 14:32:07 2016 +0100
+++ b/src/Pure/PIDE/markup.scala Mon Oct 24 16:16:55 2016 +0200
@@ -1,5 +1,4 @@
/* Title: Pure/PIDE/markup.scala
- Module: PIDE
Author: Makarius
Quasi-abstract markup elements.
--- a/src/Pure/PIDE/markup_tree.scala Mon Oct 24 14:32:07 2016 +0100
+++ b/src/Pure/PIDE/markup_tree.scala Mon Oct 24 16:16:55 2016 +0200
@@ -1,5 +1,4 @@
/* Title: Pure/PIDE/markup_tree.scala
- Module: PIDE
Author: Fabian Immler, TU Munich
Author: Makarius
--- a/src/Pure/PIDE/text.scala Mon Oct 24 14:32:07 2016 +0100
+++ b/src/Pure/PIDE/text.scala Mon Oct 24 16:16:55 2016 +0200
@@ -1,5 +1,4 @@
/* Title: Pure/PIDE/text.scala
- Module: PIDE
Author: Fabian Immler, TU Munich
Author: Makarius
--- a/src/Pure/PIDE/xml.scala Mon Oct 24 14:32:07 2016 +0100
+++ b/src/Pure/PIDE/xml.scala Mon Oct 24 16:16:55 2016 +0200
@@ -1,5 +1,4 @@
/* Title: Pure/PIDE/xml.scala
- Module: PIDE
Author: Makarius
Untyped XML trees and basic data representation.
--- a/src/Pure/PIDE/yxml.scala Mon Oct 24 14:32:07 2016 +0100
+++ b/src/Pure/PIDE/yxml.scala Mon Oct 24 16:16:55 2016 +0200
@@ -1,5 +1,4 @@
/* Title: Pure/PIDE/yxml.scala
- Module: PIDE
Author: Makarius
Efficient text representation of XML trees. Suitable for direct
--- a/src/Pure/ROOT.scala Mon Oct 24 14:32:07 2016 +0100
+++ b/src/Pure/ROOT.scala Mon Oct 24 16:16:55 2016 +0200
@@ -1,5 +1,4 @@
/* Title: Pure/ROOT.scala
- Module: PIDE
Author: Makarius
Root of isabelle package.
--- a/src/Pure/System/isabelle_tool.scala Mon Oct 24 14:32:07 2016 +0100
+++ b/src/Pure/System/isabelle_tool.scala Mon Oct 24 16:16:55 2016 +0200
@@ -105,6 +105,7 @@
Check_Sources.isabelle_tool,
Doc.isabelle_tool,
ML_Process.isabelle_tool,
+ NEWS.isabelle_tool,
Options.isabelle_tool,
Profiling_Report.isabelle_tool,
Remote_DMG.isabelle_tool,
--- a/src/Pure/System/platform.scala Mon Oct 24 14:32:07 2016 +0100
+++ b/src/Pure/System/platform.scala Mon Oct 24 16:16:55 2016 +0200
@@ -1,5 +1,4 @@
/* Title: Pure/System/platform.scala
- Module: PIDE
Author: Makarius
Raw platform identification.
--- a/src/Pure/System/utf8.scala Mon Oct 24 14:32:07 2016 +0100
+++ b/src/Pure/System/utf8.scala Mon Oct 24 16:16:55 2016 +0200
@@ -1,5 +1,4 @@
/* Title: Pure/System/utf8.scala
- Module: PIDE
Author: Makarius
Variations on UTF-8.
--- a/src/Pure/Tools/news.scala Mon Oct 24 14:32:07 2016 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,38 +0,0 @@
-/* Title: Pure/Tools/news.scala
- Author: Makarius
-
-Support for the NEWS file.
-*/
-
-package isabelle
-
-
-object NEWS
-{
- /* generate HTML version */
-
- def generate_html()
- {
- val target = Path.explode("~~/doc")
-
- File.write(target + Path.explode("NEWS.html"),
- HTML.begin_document("NEWS") +
- "\n<div class=\"source\">\n<pre class=\"source\">" +
- HTML.output(Symbol.decode(File.read(Path.explode("~~/NEWS")))) +
- "</pre>\n" +
- HTML.end_document)
-
- for (font <- Path.split(Isabelle_System.getenv_strict("ISABELLE_FONTS")))
- File.copy(font, target)
-
- File.copy(Path.explode("~~/etc/isabelle.css"), target)
- }
-
-
- /* command line entry point */
-
- def main(args: Array[String])
- {
- Command_Line.tool0 { generate_html() }
- }
-}
--- a/src/Pure/build-jars Mon Oct 24 14:32:07 2016 +0100
+++ b/src/Pure/build-jars Mon Oct 24 16:16:55 2016 +0200
@@ -18,6 +18,7 @@
Admin/ci_api.scala
Admin/ci_profile.scala
Admin/isabelle_cronjob.scala
+ Admin/news.scala
Admin/other_isabelle.scala
Admin/remote_dmg.scala
Concurrent/consumer_thread.scala
@@ -127,7 +128,6 @@
Tools/ml_console.scala
Tools/ml_process.scala
Tools/ml_statistics.scala
- Tools/news.scala
Tools/print_operation.scala
Tools/profiling_report.scala
Tools/simplifier_trace.scala
@@ -166,7 +166,6 @@
echo
echo " Options are:"
echo " -f fresh build"
- echo " -t test separate compilation of PIDE"
echo
exit 1
}
@@ -185,17 +184,13 @@
# options
FRESH=""
-TEST_PIDE=""
-while getopts "ft" OPT
+while getopts "f" OPT
do
case "$OPT" in
f)
FRESH=true
;;
- t)
- TEST_PIDE=true
- ;;
\?)
usage
;;
@@ -215,19 +210,6 @@
TARGET_DIR="$ISABELLE_HOME/lib/classes"
TARGET="$TARGET_DIR/Pure.jar"
-declare -a PIDE_SOURCES=()
-declare -a PURE_SOURCES=()
-
-for DEP in "${SOURCES[@]}"
-do
- if grep "Module:.*PIDE" "$DEP" >/dev/null
- then
- PIDE_SOURCES["${#PIDE_SOURCES[@]}"]="$DEP"
- else
- PURE_SOURCES["${#PURE_SOURCES[@]}"]="$DEP"
- fi
-done
-
declare -a UPDATED=()
if [ -n "$FRESH" ]; then
@@ -260,6 +242,7 @@
done
}
+ rm -f "$TARGET"
rm -rf classes && mkdir classes
SCALAC_OPTIONS="$ISABELLE_SCALA_BUILD_OPTIONS -d classes"
@@ -269,15 +252,8 @@
classpath classes
export CLASSPATH="$(platform_path "$ISABELLE_CLASSPATH")"
- if [ "$TEST_PIDE" = true ]; then
- isabelle_scala scalac $SCALAC_OPTIONS "${PIDE_SOURCES[@]}" || \
- fail "Failed to compile PIDE sources"
- isabelle_scala scalac $SCALAC_OPTIONS "${PURE_SOURCES[@]}" || \
- fail "Failed to compile Pure sources"
- else
- isabelle_scala scalac $SCALAC_OPTIONS "${PIDE_SOURCES[@]}" "${PURE_SOURCES[@]}" || \
- fail "Failed to compile sources"
- fi
+ isabelle_scala scalac $SCALAC_OPTIONS "${SOURCES[@]}" || \
+ fail "Failed to compile sources"
) || exit "$?"
mkdir -p "$TARGET_DIR" || fail "Failed to create directory $TARGET_DIR"
--- a/src/Pure/library.scala Mon Oct 24 14:32:07 2016 +0100
+++ b/src/Pure/library.scala Mon Oct 24 16:16:55 2016 +0200
@@ -1,5 +1,4 @@
/* Title: Pure/library.scala
- Module: PIDE
Author: Makarius
Basic library.
--- a/src/Tools/jEdit/src/Isabelle.props Mon Oct 24 14:32:07 2016 +0100
+++ b/src/Tools/jEdit/src/Isabelle.props Mon Oct 24 16:16:55 2016 +0200
@@ -5,7 +5,7 @@
#identification
plugin.isabelle.jedit.Plugin.name=Isabelle
plugin.isabelle.jedit.Plugin.author=Johannes Hölzl, Lars Hupel, Fabian Immler, Markus Kaiser, Makarius Wenzel
-plugin.isabelle.jedit.Plugin.version=7.0
+plugin.isabelle.jedit.Plugin.version=8.0
plugin.isabelle.jedit.Plugin.description=Isabelle Prover IDE
#system parameters