# HG changeset patch
# User wenzelm
# Date 1477304172 -7200
# Node ID 865b39487b5ddc1a831a13d2c0506b96bd736bef
# Parent  6a9816764b3798dec329d2d8a2361a19cd3c4e27
discontinued unused / untested distinction of separate PIDE modules;

diff -r 6a9816764b37 -r 865b39487b5d Admin/Release/CHECKLIST
--- a/Admin/Release/CHECKLIST	Mon Oct 24 12:01:36 2016 +0200
+++ b/Admin/Release/CHECKLIST	Mon Oct 24 12:16:12 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 6a9816764b37 -r 865b39487b5d Admin/build
--- a/Admin/build	Mon Oct 24 12:01:36 2016 +0200
+++ b/Admin/build	Mon Oct 24 12:16:12 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 6a9816764b37 -r 865b39487b5d src/Pure/Concurrent/consumer_thread.scala
--- a/src/Pure/Concurrent/consumer_thread.scala	Mon Oct 24 12:01:36 2016 +0200
+++ b/src/Pure/Concurrent/consumer_thread.scala	Mon Oct 24 12:16:12 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 6a9816764b37 -r 865b39487b5d src/Pure/Concurrent/counter.scala
--- a/src/Pure/Concurrent/counter.scala	Mon Oct 24 12:01:36 2016 +0200
+++ b/src/Pure/Concurrent/counter.scala	Mon Oct 24 12:16:12 2016 +0200
@@ -1,5 +1,4 @@
 /*  Title:      Pure/Concurrent/counter.scala
-    Module:     PIDE
     Author:     Makarius
 
 Synchronized counter for unique identifiers < 0.
diff -r 6a9816764b37 -r 865b39487b5d src/Pure/Concurrent/event_timer.scala
--- a/src/Pure/Concurrent/event_timer.scala	Mon Oct 24 12:01:36 2016 +0200
+++ b/src/Pure/Concurrent/event_timer.scala	Mon Oct 24 12:16:12 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 6a9816764b37 -r 865b39487b5d src/Pure/Concurrent/future.scala
--- a/src/Pure/Concurrent/future.scala	Mon Oct 24 12:01:36 2016 +0200
+++ b/src/Pure/Concurrent/future.scala	Mon Oct 24 12:16:12 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 6a9816764b37 -r 865b39487b5d src/Pure/Concurrent/mailbox.scala
--- a/src/Pure/Concurrent/mailbox.scala	Mon Oct 24 12:01:36 2016 +0200
+++ b/src/Pure/Concurrent/mailbox.scala	Mon Oct 24 12:16:12 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 6a9816764b37 -r 865b39487b5d src/Pure/Concurrent/standard_thread.scala
--- a/src/Pure/Concurrent/standard_thread.scala	Mon Oct 24 12:01:36 2016 +0200
+++ b/src/Pure/Concurrent/standard_thread.scala	Mon Oct 24 12:16:12 2016 +0200
@@ -1,5 +1,4 @@
 /*  Title:      Pure/Concurrent/standard_thread.scala
-    Module:     PIDE
     Author:     Makarius
 
 Standard thread operations.
diff -r 6a9816764b37 -r 865b39487b5d src/Pure/Concurrent/synchronized.scala
--- a/src/Pure/Concurrent/synchronized.scala	Mon Oct 24 12:01:36 2016 +0200
+++ b/src/Pure/Concurrent/synchronized.scala	Mon Oct 24 12:16:12 2016 +0200
@@ -1,5 +1,4 @@
 /*  Title:      Pure/Concurrent/synchronized.scala
-    Module:     PIDE
     Author:     Makarius
 
 Synchronized variables.
diff -r 6a9816764b37 -r 865b39487b5d src/Pure/GUI/color_value.scala
--- a/src/Pure/GUI/color_value.scala	Mon Oct 24 12:01:36 2016 +0200
+++ b/src/Pure/GUI/color_value.scala	Mon Oct 24 12:16:12 2016 +0200
@@ -1,5 +1,4 @@
 /*  Title:      Pure/GUI/color_value.scala
-    Module:     PIDE-GUI
     Author:     Makarius
 
 Cached color values.
diff -r 6a9816764b37 -r 865b39487b5d src/Pure/GUI/gui_thread.scala
--- a/src/Pure/GUI/gui_thread.scala	Mon Oct 24 12:01:36 2016 +0200
+++ b/src/Pure/GUI/gui_thread.scala	Mon Oct 24 12:16:12 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 6a9816764b37 -r 865b39487b5d src/Pure/GUI/popup.scala
--- a/src/Pure/GUI/popup.scala	Mon Oct 24 12:01:36 2016 +0200
+++ b/src/Pure/GUI/popup.scala	Mon Oct 24 12:16:12 2016 +0200
@@ -1,5 +1,4 @@
 /*  Title:      Pure/GUI/popup.scala
-    Module:     PIDE-GUI
     Author:     Makarius
 
 Popup within layered pane.
diff -r 6a9816764b37 -r 865b39487b5d src/Pure/General/bytes.scala
--- a/src/Pure/General/bytes.scala	Mon Oct 24 12:01:36 2016 +0200
+++ b/src/Pure/General/bytes.scala	Mon Oct 24 12:16:12 2016 +0200
@@ -1,5 +1,4 @@
 /*  Title:      Pure/General/bytes.scala
-    Module:     PIDE
     Author:     Makarius
 
 Immutable byte vectors versus UTF8 strings.
diff -r 6a9816764b37 -r 865b39487b5d src/Pure/General/exn.scala
--- a/src/Pure/General/exn.scala	Mon Oct 24 12:01:36 2016 +0200
+++ b/src/Pure/General/exn.scala	Mon Oct 24 12:16:12 2016 +0200
@@ -1,5 +1,4 @@
 /*  Title:      Pure/General/exn.scala
-    Module:     PIDE
     Author:     Makarius
 
 Support for exceptions (arbitrary throwables).
diff -r 6a9816764b37 -r 865b39487b5d src/Pure/General/graph.scala
--- a/src/Pure/General/graph.scala	Mon Oct 24 12:01:36 2016 +0200
+++ b/src/Pure/General/graph.scala	Mon Oct 24 12:16:12 2016 +0200
@@ -1,5 +1,4 @@
 /*  Title:      Pure/General/graph.scala
-    Module:     PIDE
     Author:     Makarius
 
 Directed graphs.
diff -r 6a9816764b37 -r 865b39487b5d src/Pure/General/linear_set.scala
--- a/src/Pure/General/linear_set.scala	Mon Oct 24 12:01:36 2016 +0200
+++ b/src/Pure/General/linear_set.scala	Mon Oct 24 12:16:12 2016 +0200
@@ -1,5 +1,4 @@
 /*  Title:      Pure/General/linear_set.scala
-    Module:     PIDE
     Author:     Makarius
     Author:     Fabian Immler, TU Munich
 
diff -r 6a9816764b37 -r 865b39487b5d src/Pure/General/multi_map.scala
--- a/src/Pure/General/multi_map.scala	Mon Oct 24 12:01:36 2016 +0200
+++ b/src/Pure/General/multi_map.scala	Mon Oct 24 12:16:12 2016 +0200
@@ -1,5 +1,4 @@
 /*  Title:      Pure/General/multi_map.scala
-    Module:     PIDE
     Author:     Makarius
 
 Maps with multiple entries per key.
diff -r 6a9816764b37 -r 865b39487b5d src/Pure/General/output.scala
--- a/src/Pure/General/output.scala	Mon Oct 24 12:01:36 2016 +0200
+++ b/src/Pure/General/output.scala	Mon Oct 24 12:16:12 2016 +0200
@@ -1,5 +1,4 @@
 /*  Title:      Pure/General/output.scala
-    Module:     PIDE
     Author:     Makarius
 
 Isabelle output channels.
diff -r 6a9816764b37 -r 865b39487b5d src/Pure/General/properties.scala
--- a/src/Pure/General/properties.scala	Mon Oct 24 12:01:36 2016 +0200
+++ b/src/Pure/General/properties.scala	Mon Oct 24 12:16:12 2016 +0200
@@ -1,5 +1,4 @@
 /*  Title:      Pure/General/properties.scala
-    Module:     PIDE
     Author:     Makarius
 
 Property lists.
diff -r 6a9816764b37 -r 865b39487b5d src/Pure/General/sha1.scala
--- a/src/Pure/General/sha1.scala	Mon Oct 24 12:01:36 2016 +0200
+++ b/src/Pure/General/sha1.scala	Mon Oct 24 12:16:12 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 6a9816764b37 -r 865b39487b5d src/Pure/General/time.scala
--- a/src/Pure/General/time.scala	Mon Oct 24 12:01:36 2016 +0200
+++ b/src/Pure/General/time.scala	Mon Oct 24 12:16:12 2016 +0200
@@ -1,5 +1,4 @@
 /*  Title:      Pure/General/time.scala
-    Module:     PIDE
     Author:     Makarius
 
 Time based on milliseconds.
diff -r 6a9816764b37 -r 865b39487b5d src/Pure/General/untyped.scala
--- a/src/Pure/General/untyped.scala	Mon Oct 24 12:01:36 2016 +0200
+++ b/src/Pure/General/untyped.scala	Mon Oct 24 12:16:12 2016 +0200
@@ -1,5 +1,4 @@
 /*  Title:      Pure/General/untyped.scala
-    Module:     PIDE
     Author:     Makarius
 
 Untyped, unscoped, unchecked access to JVM objects.
diff -r 6a9816764b37 -r 865b39487b5d src/Pure/General/word.scala
--- a/src/Pure/General/word.scala	Mon Oct 24 12:01:36 2016 +0200
+++ b/src/Pure/General/word.scala	Mon Oct 24 12:16:12 2016 +0200
@@ -1,5 +1,4 @@
 /*  Title:      Pure/General/word.scala
-    Module:     PIDE
     Author:     Makarius
 
 Support for words within Unicode text.
diff -r 6a9816764b37 -r 865b39487b5d src/Pure/PIDE/document_id.scala
--- a/src/Pure/PIDE/document_id.scala	Mon Oct 24 12:01:36 2016 +0200
+++ b/src/Pure/PIDE/document_id.scala	Mon Oct 24 12:16:12 2016 +0200
@@ -1,5 +1,4 @@
 /*  Title:      Pure/PIDE/document_id.scala
-    Module:     PIDE
     Author:     Makarius
 
 Unique identifiers for document structure.
diff -r 6a9816764b37 -r 865b39487b5d src/Pure/PIDE/markup.scala
--- a/src/Pure/PIDE/markup.scala	Mon Oct 24 12:01:36 2016 +0200
+++ b/src/Pure/PIDE/markup.scala	Mon Oct 24 12:16:12 2016 +0200
@@ -1,5 +1,4 @@
 /*  Title:      Pure/PIDE/markup.scala
-    Module:     PIDE
     Author:     Makarius
 
 Quasi-abstract markup elements.
diff -r 6a9816764b37 -r 865b39487b5d src/Pure/PIDE/markup_tree.scala
--- a/src/Pure/PIDE/markup_tree.scala	Mon Oct 24 12:01:36 2016 +0200
+++ b/src/Pure/PIDE/markup_tree.scala	Mon Oct 24 12:16:12 2016 +0200
@@ -1,5 +1,4 @@
 /*  Title:      Pure/PIDE/markup_tree.scala
-    Module:     PIDE
     Author:     Fabian Immler, TU Munich
     Author:     Makarius
 
diff -r 6a9816764b37 -r 865b39487b5d src/Pure/PIDE/text.scala
--- a/src/Pure/PIDE/text.scala	Mon Oct 24 12:01:36 2016 +0200
+++ b/src/Pure/PIDE/text.scala	Mon Oct 24 12:16:12 2016 +0200
@@ -1,5 +1,4 @@
 /*  Title:      Pure/PIDE/text.scala
-    Module:     PIDE
     Author:     Fabian Immler, TU Munich
     Author:     Makarius
 
diff -r 6a9816764b37 -r 865b39487b5d src/Pure/PIDE/xml.scala
--- a/src/Pure/PIDE/xml.scala	Mon Oct 24 12:01:36 2016 +0200
+++ b/src/Pure/PIDE/xml.scala	Mon Oct 24 12:16:12 2016 +0200
@@ -1,5 +1,4 @@
 /*  Title:      Pure/PIDE/xml.scala
-    Module:     PIDE
     Author:     Makarius
 
 Untyped XML trees and basic data representation.
diff -r 6a9816764b37 -r 865b39487b5d src/Pure/PIDE/yxml.scala
--- a/src/Pure/PIDE/yxml.scala	Mon Oct 24 12:01:36 2016 +0200
+++ b/src/Pure/PIDE/yxml.scala	Mon Oct 24 12:16:12 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 6a9816764b37 -r 865b39487b5d src/Pure/ROOT.scala
--- a/src/Pure/ROOT.scala	Mon Oct 24 12:01:36 2016 +0200
+++ b/src/Pure/ROOT.scala	Mon Oct 24 12:16:12 2016 +0200
@@ -1,5 +1,4 @@
 /*  Title:      Pure/ROOT.scala
-    Module:     PIDE
     Author:     Makarius
 
 Root of isabelle package.
diff -r 6a9816764b37 -r 865b39487b5d src/Pure/System/platform.scala
--- a/src/Pure/System/platform.scala	Mon Oct 24 12:01:36 2016 +0200
+++ b/src/Pure/System/platform.scala	Mon Oct 24 12:16:12 2016 +0200
@@ -1,5 +1,4 @@
 /*  Title:      Pure/System/platform.scala
-    Module:     PIDE
     Author:     Makarius
 
 Raw platform identification.
diff -r 6a9816764b37 -r 865b39487b5d src/Pure/System/utf8.scala
--- a/src/Pure/System/utf8.scala	Mon Oct 24 12:01:36 2016 +0200
+++ b/src/Pure/System/utf8.scala	Mon Oct 24 12:16:12 2016 +0200
@@ -1,5 +1,4 @@
 /*  Title:      Pure/System/utf8.scala
-    Module:     PIDE
     Author:     Makarius
 
 Variations on UTF-8.
diff -r 6a9816764b37 -r 865b39487b5d src/Pure/build-jars
--- a/src/Pure/build-jars	Mon Oct 24 12:01:36 2016 +0200
+++ b/src/Pure/build-jars	Mon Oct 24 12:16:12 2016 +0200
@@ -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
@@ -269,15 +251,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 6a9816764b37 -r 865b39487b5d src/Pure/library.scala
--- a/src/Pure/library.scala	Mon Oct 24 12:01:36 2016 +0200
+++ b/src/Pure/library.scala	Mon Oct 24 12:16:12 2016 +0200
@@ -1,5 +1,4 @@
 /*  Title:      Pure/library.scala
-    Module:     PIDE
     Author:     Makarius
 
 Basic library.