# HG changeset patch
# User wenzelm
# Date 1477318615 -7200
# Node ID c1db9e3fe0e2356940c8257d86c840db697e8389
# Parent  6694bd2b9b676e4a9b3b2cd824fe4770f9bec01b# Parent  68ace7f3d78f9665ed6eb8ab4744183055616f50
merged

diff -r 6694bd2b9b67 -r c1db9e3fe0e2 Admin/Release/CHECKLIST
--- 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
diff -r 6694bd2b9b67 -r c1db9e3fe0e2 Admin/build
--- 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
diff -r 6694bd2b9b67 -r c1db9e3fe0e2 Admin/components/bundled-windows
--- 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
diff -r 6694bd2b9b67 -r c1db9e3fe0e2 Admin/components/components.sha1
--- 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
diff -r 6694bd2b9b67 -r c1db9e3fe0e2 Admin/components/main
--- 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
diff -r 6694bd2b9b67 -r c1db9e3fe0e2 Admin/lib/Tools/makedist
--- 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"
-
diff -r 6694bd2b9b67 -r c1db9e3fe0e2 src/Pure/Admin/build_history.scala
--- 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)
       }
diff -r 6694bd2b9b67 -r c1db9e3fe0e2 src/Pure/Admin/build_release.scala
--- 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()
diff -r 6694bd2b9b67 -r c1db9e3fe0e2 src/Pure/Admin/check_sources.scala
--- 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)
diff -r 6694bd2b9b67 -r c1db9e3fe0e2 src/Pure/Admin/news.scala
--- /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)
+}
diff -r 6694bd2b9b67 -r c1db9e3fe0e2 src/Pure/Concurrent/consumer_thread.scala
--- 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
diff -r 6694bd2b9b67 -r c1db9e3fe0e2 src/Pure/Concurrent/counter.scala
--- 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.
diff -r 6694bd2b9b67 -r c1db9e3fe0e2 src/Pure/Concurrent/event_timer.scala
--- 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.
diff -r 6694bd2b9b67 -r c1db9e3fe0e2 src/Pure/Concurrent/future.scala
--- 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.
diff -r 6694bd2b9b67 -r c1db9e3fe0e2 src/Pure/Concurrent/mailbox.scala
--- 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,
diff -r 6694bd2b9b67 -r c1db9e3fe0e2 src/Pure/Concurrent/standard_thread.scala
--- 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.
diff -r 6694bd2b9b67 -r c1db9e3fe0e2 src/Pure/Concurrent/synchronized.scala
--- 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.
diff -r 6694bd2b9b67 -r c1db9e3fe0e2 src/Pure/GUI/color_value.scala
--- 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.
diff -r 6694bd2b9b67 -r c1db9e3fe0e2 src/Pure/GUI/gui_thread.scala
--- 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).
diff -r 6694bd2b9b67 -r c1db9e3fe0e2 src/Pure/GUI/popup.scala
--- 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.
diff -r 6694bd2b9b67 -r c1db9e3fe0e2 src/Pure/General/bytes.scala
--- 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.
diff -r 6694bd2b9b67 -r c1db9e3fe0e2 src/Pure/General/exn.scala
--- 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).
diff -r 6694bd2b9b67 -r c1db9e3fe0e2 src/Pure/General/graph.scala
--- 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.
diff -r 6694bd2b9b67 -r c1db9e3fe0e2 src/Pure/General/linear_set.scala
--- 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
 
diff -r 6694bd2b9b67 -r c1db9e3fe0e2 src/Pure/General/multi_map.scala
--- 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.
diff -r 6694bd2b9b67 -r c1db9e3fe0e2 src/Pure/General/output.scala
--- 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.
diff -r 6694bd2b9b67 -r c1db9e3fe0e2 src/Pure/General/properties.scala
--- 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.
diff -r 6694bd2b9b67 -r c1db9e3fe0e2 src/Pure/General/sha1.scala
--- 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).
diff -r 6694bd2b9b67 -r c1db9e3fe0e2 src/Pure/General/time.scala
--- 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.
diff -r 6694bd2b9b67 -r c1db9e3fe0e2 src/Pure/General/untyped.scala
--- 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.
diff -r 6694bd2b9b67 -r c1db9e3fe0e2 src/Pure/General/word.scala
--- 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.
diff -r 6694bd2b9b67 -r c1db9e3fe0e2 src/Pure/PIDE/document_id.scala
--- 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.
diff -r 6694bd2b9b67 -r c1db9e3fe0e2 src/Pure/PIDE/markup.scala
--- 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.
diff -r 6694bd2b9b67 -r c1db9e3fe0e2 src/Pure/PIDE/markup_tree.scala
--- 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
 
diff -r 6694bd2b9b67 -r c1db9e3fe0e2 src/Pure/PIDE/text.scala
--- 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
 
diff -r 6694bd2b9b67 -r c1db9e3fe0e2 src/Pure/PIDE/xml.scala
--- 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.
diff -r 6694bd2b9b67 -r c1db9e3fe0e2 src/Pure/PIDE/yxml.scala
--- 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
diff -r 6694bd2b9b67 -r c1db9e3fe0e2 src/Pure/ROOT.scala
--- 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.
diff -r 6694bd2b9b67 -r c1db9e3fe0e2 src/Pure/System/isabelle_tool.scala
--- 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,
diff -r 6694bd2b9b67 -r c1db9e3fe0e2 src/Pure/System/platform.scala
--- 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.
diff -r 6694bd2b9b67 -r c1db9e3fe0e2 src/Pure/System/utf8.scala
--- 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.
diff -r 6694bd2b9b67 -r c1db9e3fe0e2 src/Pure/Tools/news.scala
--- 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() }
-  }
-}
diff -r 6694bd2b9b67 -r c1db9e3fe0e2 src/Pure/build-jars
--- 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"
diff -r 6694bd2b9b67 -r c1db9e3fe0e2 src/Pure/library.scala
--- 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.
diff -r 6694bd2b9b67 -r c1db9e3fe0e2 src/Tools/jEdit/src/Isabelle.props
--- 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