discontinued unused / untested distinction of separate PIDE modules;
authorwenzelm
Mon Oct 24 12:16:12 2016 +0200 (2016-10-24 ago)
changeset 64370865b39487b5d
parent 64369 6a9816764b37
child 64371 213cf4215b40
discontinued unused / untested distinction of separate PIDE modules;
Admin/Release/CHECKLIST
Admin/build
src/Pure/Concurrent/consumer_thread.scala
src/Pure/Concurrent/counter.scala
src/Pure/Concurrent/event_timer.scala
src/Pure/Concurrent/future.scala
src/Pure/Concurrent/mailbox.scala
src/Pure/Concurrent/standard_thread.scala
src/Pure/Concurrent/synchronized.scala
src/Pure/GUI/color_value.scala
src/Pure/GUI/gui_thread.scala
src/Pure/GUI/popup.scala
src/Pure/General/bytes.scala
src/Pure/General/exn.scala
src/Pure/General/graph.scala
src/Pure/General/linear_set.scala
src/Pure/General/multi_map.scala
src/Pure/General/output.scala
src/Pure/General/properties.scala
src/Pure/General/sha1.scala
src/Pure/General/time.scala
src/Pure/General/untyped.scala
src/Pure/General/word.scala
src/Pure/PIDE/document_id.scala
src/Pure/PIDE/markup.scala
src/Pure/PIDE/markup_tree.scala
src/Pure/PIDE/text.scala
src/Pure/PIDE/xml.scala
src/Pure/PIDE/yxml.scala
src/Pure/ROOT.scala
src/Pure/System/platform.scala
src/Pure/System/utf8.scala
src/Pure/build-jars
src/Pure/library.scala
     1.1 --- a/Admin/Release/CHECKLIST	Mon Oct 24 12:01:36 2016 +0200
     1.2 +++ b/Admin/Release/CHECKLIST	Mon Oct 24 12:16:12 2016 +0200
     1.3 @@ -36,9 +36,6 @@
     1.4  
     1.5  - HTML library: check theory dependencies (PDF);
     1.6  
     1.7 -- test separate compilation of Isabelle/Scala PIDE sources:
     1.8 -    Admin/build jars_test
     1.9 -
    1.10  - test Isabelle/jEdit:
    1.11      . print buffer
    1.12      . on single-core
     2.1 --- a/Admin/build	Mon Oct 24 12:01:36 2016 +0200
     2.2 +++ b/Admin/build	Mon Oct 24 12:16:12 2016 +0200
     2.3 @@ -26,7 +26,6 @@
     2.4      all             all modules below
     2.5      browser         graph browser
     2.6      jars            Isabelle/Scala
     2.7 -    jars_test       test separate build of jars
     2.8      jars_fresh      fresh build of jars
     2.9  
    2.10  EOF
    2.11 @@ -86,7 +85,6 @@
    2.12      browser) build_browser;;
    2.13      jars) build_jars;;
    2.14      jars_fresh) build_jars -f;;
    2.15 -    jars_test) build_jars -t;;
    2.16      *) fail "Bad module $MODULE"
    2.17    esac
    2.18  done
     3.1 --- a/src/Pure/Concurrent/consumer_thread.scala	Mon Oct 24 12:01:36 2016 +0200
     3.2 +++ b/src/Pure/Concurrent/consumer_thread.scala	Mon Oct 24 12:16:12 2016 +0200
     3.3 @@ -1,5 +1,4 @@
     3.4  /*  Title:      Pure/Concurrent/consumer_thread.scala
     3.5 -    Module:     PIDE
     3.6      Author:     Makarius
     3.7  
     3.8  Consumer thread with unbounded queueing of requests, and optional
     4.1 --- a/src/Pure/Concurrent/counter.scala	Mon Oct 24 12:01:36 2016 +0200
     4.2 +++ b/src/Pure/Concurrent/counter.scala	Mon Oct 24 12:16:12 2016 +0200
     4.3 @@ -1,5 +1,4 @@
     4.4  /*  Title:      Pure/Concurrent/counter.scala
     4.5 -    Module:     PIDE
     4.6      Author:     Makarius
     4.7  
     4.8  Synchronized counter for unique identifiers < 0.
     5.1 --- a/src/Pure/Concurrent/event_timer.scala	Mon Oct 24 12:01:36 2016 +0200
     5.2 +++ b/src/Pure/Concurrent/event_timer.scala	Mon Oct 24 12:16:12 2016 +0200
     5.3 @@ -1,5 +1,4 @@
     5.4  /*  Title:      Pure/Concurrent/event_timer.scala
     5.5 -    Module:     PIDE
     5.6      Author:     Makarius
     5.7  
     5.8  Initiate event after given point in time.
     6.1 --- a/src/Pure/Concurrent/future.scala	Mon Oct 24 12:01:36 2016 +0200
     6.2 +++ b/src/Pure/Concurrent/future.scala	Mon Oct 24 12:16:12 2016 +0200
     6.3 @@ -1,5 +1,4 @@
     6.4  /*  Title:      Pure/Concurrent/future.scala
     6.5 -    Module:     PIDE
     6.6      Author:     Makarius
     6.7  
     6.8  Value-oriented parallel execution via futures and promises.
     7.1 --- a/src/Pure/Concurrent/mailbox.scala	Mon Oct 24 12:01:36 2016 +0200
     7.2 +++ b/src/Pure/Concurrent/mailbox.scala	Mon Oct 24 12:16:12 2016 +0200
     7.3 @@ -1,5 +1,4 @@
     7.4  /*  Title:      Pure/Concurrent/mailbox.scala
     7.5 -    Module:     PIDE
     7.6      Author:     Makarius
     7.7  
     7.8  Message exchange via mailbox, with multiple senders (non-blocking,
     8.1 --- a/src/Pure/Concurrent/standard_thread.scala	Mon Oct 24 12:01:36 2016 +0200
     8.2 +++ b/src/Pure/Concurrent/standard_thread.scala	Mon Oct 24 12:16:12 2016 +0200
     8.3 @@ -1,5 +1,4 @@
     8.4  /*  Title:      Pure/Concurrent/standard_thread.scala
     8.5 -    Module:     PIDE
     8.6      Author:     Makarius
     8.7  
     8.8  Standard thread operations.
     9.1 --- a/src/Pure/Concurrent/synchronized.scala	Mon Oct 24 12:01:36 2016 +0200
     9.2 +++ b/src/Pure/Concurrent/synchronized.scala	Mon Oct 24 12:16:12 2016 +0200
     9.3 @@ -1,5 +1,4 @@
     9.4  /*  Title:      Pure/Concurrent/synchronized.scala
     9.5 -    Module:     PIDE
     9.6      Author:     Makarius
     9.7  
     9.8  Synchronized variables.
    10.1 --- a/src/Pure/GUI/color_value.scala	Mon Oct 24 12:01:36 2016 +0200
    10.2 +++ b/src/Pure/GUI/color_value.scala	Mon Oct 24 12:16:12 2016 +0200
    10.3 @@ -1,5 +1,4 @@
    10.4  /*  Title:      Pure/GUI/color_value.scala
    10.5 -    Module:     PIDE-GUI
    10.6      Author:     Makarius
    10.7  
    10.8  Cached color values.
    11.1 --- a/src/Pure/GUI/gui_thread.scala	Mon Oct 24 12:01:36 2016 +0200
    11.2 +++ b/src/Pure/GUI/gui_thread.scala	Mon Oct 24 12:16:12 2016 +0200
    11.3 @@ -1,5 +1,4 @@
    11.4  /*  Title:      Pure/GUI/gui_thread.scala
    11.5 -    Module:     PIDE-GUI
    11.6      Author:     Makarius
    11.7  
    11.8  Evaluation within the GUI thread (for AWT/Swing).
    12.1 --- a/src/Pure/GUI/popup.scala	Mon Oct 24 12:01:36 2016 +0200
    12.2 +++ b/src/Pure/GUI/popup.scala	Mon Oct 24 12:16:12 2016 +0200
    12.3 @@ -1,5 +1,4 @@
    12.4  /*  Title:      Pure/GUI/popup.scala
    12.5 -    Module:     PIDE-GUI
    12.6      Author:     Makarius
    12.7  
    12.8  Popup within layered pane.
    13.1 --- a/src/Pure/General/bytes.scala	Mon Oct 24 12:01:36 2016 +0200
    13.2 +++ b/src/Pure/General/bytes.scala	Mon Oct 24 12:16:12 2016 +0200
    13.3 @@ -1,5 +1,4 @@
    13.4  /*  Title:      Pure/General/bytes.scala
    13.5 -    Module:     PIDE
    13.6      Author:     Makarius
    13.7  
    13.8  Immutable byte vectors versus UTF8 strings.
    14.1 --- a/src/Pure/General/exn.scala	Mon Oct 24 12:01:36 2016 +0200
    14.2 +++ b/src/Pure/General/exn.scala	Mon Oct 24 12:16:12 2016 +0200
    14.3 @@ -1,5 +1,4 @@
    14.4  /*  Title:      Pure/General/exn.scala
    14.5 -    Module:     PIDE
    14.6      Author:     Makarius
    14.7  
    14.8  Support for exceptions (arbitrary throwables).
    15.1 --- a/src/Pure/General/graph.scala	Mon Oct 24 12:01:36 2016 +0200
    15.2 +++ b/src/Pure/General/graph.scala	Mon Oct 24 12:16:12 2016 +0200
    15.3 @@ -1,5 +1,4 @@
    15.4  /*  Title:      Pure/General/graph.scala
    15.5 -    Module:     PIDE
    15.6      Author:     Makarius
    15.7  
    15.8  Directed graphs.
    16.1 --- a/src/Pure/General/linear_set.scala	Mon Oct 24 12:01:36 2016 +0200
    16.2 +++ b/src/Pure/General/linear_set.scala	Mon Oct 24 12:16:12 2016 +0200
    16.3 @@ -1,5 +1,4 @@
    16.4  /*  Title:      Pure/General/linear_set.scala
    16.5 -    Module:     PIDE
    16.6      Author:     Makarius
    16.7      Author:     Fabian Immler, TU Munich
    16.8  
    17.1 --- a/src/Pure/General/multi_map.scala	Mon Oct 24 12:01:36 2016 +0200
    17.2 +++ b/src/Pure/General/multi_map.scala	Mon Oct 24 12:16:12 2016 +0200
    17.3 @@ -1,5 +1,4 @@
    17.4  /*  Title:      Pure/General/multi_map.scala
    17.5 -    Module:     PIDE
    17.6      Author:     Makarius
    17.7  
    17.8  Maps with multiple entries per key.
    18.1 --- a/src/Pure/General/output.scala	Mon Oct 24 12:01:36 2016 +0200
    18.2 +++ b/src/Pure/General/output.scala	Mon Oct 24 12:16:12 2016 +0200
    18.3 @@ -1,5 +1,4 @@
    18.4  /*  Title:      Pure/General/output.scala
    18.5 -    Module:     PIDE
    18.6      Author:     Makarius
    18.7  
    18.8  Isabelle output channels.
    19.1 --- a/src/Pure/General/properties.scala	Mon Oct 24 12:01:36 2016 +0200
    19.2 +++ b/src/Pure/General/properties.scala	Mon Oct 24 12:16:12 2016 +0200
    19.3 @@ -1,5 +1,4 @@
    19.4  /*  Title:      Pure/General/properties.scala
    19.5 -    Module:     PIDE
    19.6      Author:     Makarius
    19.7  
    19.8  Property lists.
    20.1 --- a/src/Pure/General/sha1.scala	Mon Oct 24 12:01:36 2016 +0200
    20.2 +++ b/src/Pure/General/sha1.scala	Mon Oct 24 12:16:12 2016 +0200
    20.3 @@ -1,5 +1,4 @@
    20.4  /*  Title:      Pure/General/sha1.scala
    20.5 -    Module:     PIDE
    20.6      Author:     Makarius
    20.7  
    20.8  Digest strings according to SHA-1 (see RFC 3174).
    21.1 --- a/src/Pure/General/time.scala	Mon Oct 24 12:01:36 2016 +0200
    21.2 +++ b/src/Pure/General/time.scala	Mon Oct 24 12:16:12 2016 +0200
    21.3 @@ -1,5 +1,4 @@
    21.4  /*  Title:      Pure/General/time.scala
    21.5 -    Module:     PIDE
    21.6      Author:     Makarius
    21.7  
    21.8  Time based on milliseconds.
    22.1 --- a/src/Pure/General/untyped.scala	Mon Oct 24 12:01:36 2016 +0200
    22.2 +++ b/src/Pure/General/untyped.scala	Mon Oct 24 12:16:12 2016 +0200
    22.3 @@ -1,5 +1,4 @@
    22.4  /*  Title:      Pure/General/untyped.scala
    22.5 -    Module:     PIDE
    22.6      Author:     Makarius
    22.7  
    22.8  Untyped, unscoped, unchecked access to JVM objects.
    23.1 --- a/src/Pure/General/word.scala	Mon Oct 24 12:01:36 2016 +0200
    23.2 +++ b/src/Pure/General/word.scala	Mon Oct 24 12:16:12 2016 +0200
    23.3 @@ -1,5 +1,4 @@
    23.4  /*  Title:      Pure/General/word.scala
    23.5 -    Module:     PIDE
    23.6      Author:     Makarius
    23.7  
    23.8  Support for words within Unicode text.
    24.1 --- a/src/Pure/PIDE/document_id.scala	Mon Oct 24 12:01:36 2016 +0200
    24.2 +++ b/src/Pure/PIDE/document_id.scala	Mon Oct 24 12:16:12 2016 +0200
    24.3 @@ -1,5 +1,4 @@
    24.4  /*  Title:      Pure/PIDE/document_id.scala
    24.5 -    Module:     PIDE
    24.6      Author:     Makarius
    24.7  
    24.8  Unique identifiers for document structure.
    25.1 --- a/src/Pure/PIDE/markup.scala	Mon Oct 24 12:01:36 2016 +0200
    25.2 +++ b/src/Pure/PIDE/markup.scala	Mon Oct 24 12:16:12 2016 +0200
    25.3 @@ -1,5 +1,4 @@
    25.4  /*  Title:      Pure/PIDE/markup.scala
    25.5 -    Module:     PIDE
    25.6      Author:     Makarius
    25.7  
    25.8  Quasi-abstract markup elements.
    26.1 --- a/src/Pure/PIDE/markup_tree.scala	Mon Oct 24 12:01:36 2016 +0200
    26.2 +++ b/src/Pure/PIDE/markup_tree.scala	Mon Oct 24 12:16:12 2016 +0200
    26.3 @@ -1,5 +1,4 @@
    26.4  /*  Title:      Pure/PIDE/markup_tree.scala
    26.5 -    Module:     PIDE
    26.6      Author:     Fabian Immler, TU Munich
    26.7      Author:     Makarius
    26.8  
    27.1 --- a/src/Pure/PIDE/text.scala	Mon Oct 24 12:01:36 2016 +0200
    27.2 +++ b/src/Pure/PIDE/text.scala	Mon Oct 24 12:16:12 2016 +0200
    27.3 @@ -1,5 +1,4 @@
    27.4  /*  Title:      Pure/PIDE/text.scala
    27.5 -    Module:     PIDE
    27.6      Author:     Fabian Immler, TU Munich
    27.7      Author:     Makarius
    27.8  
    28.1 --- a/src/Pure/PIDE/xml.scala	Mon Oct 24 12:01:36 2016 +0200
    28.2 +++ b/src/Pure/PIDE/xml.scala	Mon Oct 24 12:16:12 2016 +0200
    28.3 @@ -1,5 +1,4 @@
    28.4  /*  Title:      Pure/PIDE/xml.scala
    28.5 -    Module:     PIDE
    28.6      Author:     Makarius
    28.7  
    28.8  Untyped XML trees and basic data representation.
    29.1 --- a/src/Pure/PIDE/yxml.scala	Mon Oct 24 12:01:36 2016 +0200
    29.2 +++ b/src/Pure/PIDE/yxml.scala	Mon Oct 24 12:16:12 2016 +0200
    29.3 @@ -1,5 +1,4 @@
    29.4  /*  Title:      Pure/PIDE/yxml.scala
    29.5 -    Module:     PIDE
    29.6      Author:     Makarius
    29.7  
    29.8  Efficient text representation of XML trees.  Suitable for direct
    30.1 --- a/src/Pure/ROOT.scala	Mon Oct 24 12:01:36 2016 +0200
    30.2 +++ b/src/Pure/ROOT.scala	Mon Oct 24 12:16:12 2016 +0200
    30.3 @@ -1,5 +1,4 @@
    30.4  /*  Title:      Pure/ROOT.scala
    30.5 -    Module:     PIDE
    30.6      Author:     Makarius
    30.7  
    30.8  Root of isabelle package.
    31.1 --- a/src/Pure/System/platform.scala	Mon Oct 24 12:01:36 2016 +0200
    31.2 +++ b/src/Pure/System/platform.scala	Mon Oct 24 12:16:12 2016 +0200
    31.3 @@ -1,5 +1,4 @@
    31.4  /*  Title:      Pure/System/platform.scala
    31.5 -    Module:     PIDE
    31.6      Author:     Makarius
    31.7  
    31.8  Raw platform identification.
    32.1 --- a/src/Pure/System/utf8.scala	Mon Oct 24 12:01:36 2016 +0200
    32.2 +++ b/src/Pure/System/utf8.scala	Mon Oct 24 12:16:12 2016 +0200
    32.3 @@ -1,5 +1,4 @@
    32.4  /*  Title:      Pure/System/utf8.scala
    32.5 -    Module:     PIDE
    32.6      Author:     Makarius
    32.7  
    32.8  Variations on UTF-8.
    33.1 --- a/src/Pure/build-jars	Mon Oct 24 12:01:36 2016 +0200
    33.2 +++ b/src/Pure/build-jars	Mon Oct 24 12:16:12 2016 +0200
    33.3 @@ -166,7 +166,6 @@
    33.4    echo
    33.5    echo "  Options are:"
    33.6    echo "    -f           fresh build"
    33.7 -  echo "    -t           test separate compilation of PIDE"
    33.8    echo
    33.9    exit 1
   33.10  }
   33.11 @@ -185,17 +184,13 @@
   33.12  # options
   33.13  
   33.14  FRESH=""
   33.15 -TEST_PIDE=""
   33.16  
   33.17 -while getopts "ft" OPT
   33.18 +while getopts "f" OPT
   33.19  do
   33.20    case "$OPT" in
   33.21      f)
   33.22        FRESH=true
   33.23        ;;
   33.24 -    t)
   33.25 -      TEST_PIDE=true
   33.26 -      ;;
   33.27      \?)
   33.28        usage
   33.29        ;;
   33.30 @@ -215,19 +210,6 @@
   33.31  TARGET_DIR="$ISABELLE_HOME/lib/classes"
   33.32  TARGET="$TARGET_DIR/Pure.jar"
   33.33  
   33.34 -declare -a PIDE_SOURCES=()
   33.35 -declare -a PURE_SOURCES=()
   33.36 -
   33.37 -for DEP in "${SOURCES[@]}"
   33.38 -do
   33.39 -  if grep "Module:.*PIDE" "$DEP" >/dev/null
   33.40 -  then
   33.41 -    PIDE_SOURCES["${#PIDE_SOURCES[@]}"]="$DEP"
   33.42 -  else
   33.43 -    PURE_SOURCES["${#PURE_SOURCES[@]}"]="$DEP"
   33.44 -  fi
   33.45 -done
   33.46 -
   33.47  declare -a UPDATED=()
   33.48  
   33.49  if [ -n "$FRESH" ]; then
   33.50 @@ -269,15 +251,8 @@
   33.51      classpath classes
   33.52      export CLASSPATH="$(platform_path "$ISABELLE_CLASSPATH")"
   33.53  
   33.54 -    if [ "$TEST_PIDE" = true ]; then
   33.55 -      isabelle_scala scalac $SCALAC_OPTIONS "${PIDE_SOURCES[@]}" || \
   33.56 -        fail "Failed to compile PIDE sources"
   33.57 -      isabelle_scala scalac $SCALAC_OPTIONS "${PURE_SOURCES[@]}" || \
   33.58 -        fail "Failed to compile Pure sources"
   33.59 -    else
   33.60 -      isabelle_scala scalac $SCALAC_OPTIONS "${PIDE_SOURCES[@]}" "${PURE_SOURCES[@]}" || \
   33.61 -        fail "Failed to compile sources"
   33.62 -    fi
   33.63 +    isabelle_scala scalac $SCALAC_OPTIONS "${SOURCES[@]}" || \
   33.64 +      fail "Failed to compile sources"
   33.65    ) || exit "$?"
   33.66  
   33.67    mkdir -p "$TARGET_DIR" || fail "Failed to create directory $TARGET_DIR"
    34.1 --- a/src/Pure/library.scala	Mon Oct 24 12:01:36 2016 +0200
    34.2 +++ b/src/Pure/library.scala	Mon Oct 24 12:16:12 2016 +0200
    34.3 @@ -1,5 +1,4 @@
    34.4  /*  Title:      Pure/library.scala
    34.5 -    Module:     PIDE
    34.6      Author:     Makarius
    34.7  
    34.8  Basic library.