src/Pure/build-jars

added new vcg based on existentially quantified while-rule

#!/usr/bin/env bash
#
# Author: Makarius
#
# build-jars - build Isabelle/Scala
#
# Requires proper Isabelle settings environment.

## sources

declare -a SOURCES=(
  Concurrent/consumer_thread.scala
  Concurrent/counter.scala
  Concurrent/event_timer.scala
  Concurrent/future.scala
  Concurrent/mailbox.scala
  Concurrent/par_list.scala
  Concurrent/standard_thread.scala
  Concurrent/synchronized.scala
  GUI/color_value.scala
  GUI/gui.scala
  GUI/gui_thread.scala
  GUI/html5_panel.scala
  GUI/jfx_gui.scala
  GUI/popup.scala
  GUI/wrap_panel.scala
  General/antiquote.scala
  General/bytes.scala
  General/completion.scala
  General/exn.scala
  General/file.scala
  General/graph.scala
  General/graph_display.scala
  General/graphics_file.scala
  General/linear_set.scala
  General/long_name.scala
  General/multi_map.scala
  General/output.scala
  General/path.scala
  General/position.scala
  General/pretty.scala
  General/properties.scala
  General/scan.scala
  General/sha1.scala
  General/symbol.scala
  General/time.scala
  General/timing.scala
  General/untyped.scala
  General/url.scala
  General/word.scala
  General/xz_file.scala
  Isar/keyword.scala
  Isar/outer_syntax.scala
  Isar/parse.scala
  Isar/token.scala
  ML/ml_lex.scala
  ML/ml_syntax.scala
  PIDE/batch_session.scala
  PIDE/command.scala
  PIDE/command_span.scala
  PIDE/document.scala
  PIDE/document_id.scala
  PIDE/editor.scala
  PIDE/markup.scala
  PIDE/markup_tree.scala
  PIDE/protocol.scala
  PIDE/protocol_message.scala
  PIDE/prover.scala
  PIDE/query_operation.scala
  PIDE/resources.scala
  PIDE/session.scala
  PIDE/text.scala
  PIDE/xml.scala
  PIDE/yxml.scala
  ROOT.scala
  System/bash.scala
  System/command_line.scala
  System/cygwin.scala
  System/distribution.scala
  System/getopts.scala
  System/invoke_scala.scala
  System/isabelle_charset.scala
  System/isabelle_process.scala
  System/isabelle_system.scala
  System/isabelle_tool.scala
  System/options.scala
  System/platform.scala
  System/posix_interrupt.scala
  System/process_result.scala
  System/progress.scala
  System/system_channel.scala
  System/utf8.scala
  Thy/html.scala
  Thy/present.scala
  Thy/sessions.scala
  Thy/thy_header.scala
  Thy/thy_info.scala
  Thy/thy_syntax.scala
  Tools/bibtex.scala
  Tools/build.scala
  Tools/build_doc.scala
  Tools/check_keywords.scala
  Tools/check_sources.scala
  Tools/ci_profile.scala
  Tools/debugger.scala
  Tools/doc.scala
  Tools/main.scala
  Tools/ml_console.scala
  Tools/ml_process.scala
  Tools/ml_statistics.scala
  Tools/news.scala
  Tools/print_operation.scala
  Tools/simplifier_trace.scala
  Tools/task_statistics.scala
  Tools/update_cartouches.scala
  Tools/update_header.scala
  Tools/update_then.scala
  Tools/update_theorems.scala
  library.scala
  term.scala
  term_xml.scala
  "../Tools/Graphview/graph_file.scala"
  "../Tools/Graphview/graph_panel.scala"
  "../Tools/Graphview/graphview.scala"
  "../Tools/Graphview/layout.scala"
  "../Tools/Graphview/main_panel.scala"
  "../Tools/Graphview/metrics.scala"
  "../Tools/Graphview/model.scala"
  "../Tools/Graphview/mutator.scala"
  "../Tools/Graphview/mutator_dialog.scala"
  "../Tools/Graphview/mutator_event.scala"
  "../Tools/Graphview/popups.scala"
  "../Tools/Graphview/shapes.scala"
  "../Tools/Graphview/tree_panel.scala"
)


## diagnostics

PRG="$(basename "$0")"

function usage()
{
  echo
  echo "Usage: isabelle $PRG [OPTIONS]"
  echo
  echo "  Options are:"
  echo "    -f           fresh build"
  echo "    -t           test separate compilation of PIDE"
  echo
  exit 1
}

function fail()
{
  echo "$1" >&2
  exit 2
}

[ -z "$ISABELLE_HOME" ] && fail "Missing Isabelle settings environment"


## process command line

# options

FRESH=""
TEST_PIDE=""

while getopts "ft" OPT
do
  case "$OPT" in
    f)
      FRESH=true
      ;;
    t)
      TEST_PIDE=true
      ;;
    \?)
      usage
      ;;
  esac
done

shift $(($OPTIND - 1))


# args

[ "$#" -ne 0 ] && usage


## build

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
  OUTDATED=true
else
  OUTDATED=false
  if [ ! -e "$TARGET" ]; then
    OUTDATED=true
  else
    for DEP in "${SOURCES[@]}"
    do
      [ ! -e "$DEP" ] && fail "Missing file: $DEP"
      [ "$DEP" -nt "$TARGET" ] && {
        OUTDATED=true
        UPDATED["${#UPDATED[@]}"]="$DEP"
      }
    done
  fi
fi

if [ "$OUTDATED" = true ]
then
  echo "### Building Isabelle/Scala ..."

  [ "${#UPDATED[@]}" -gt 0 ] && {
    echo "Changed files:"
    for FILE in "${UPDATED[@]}"
    do
      echo "  $FILE"
    done
  }

  rm -rf classes && mkdir classes

  SCALAC_OPTIONS="$ISABELLE_SCALA_BUILD_OPTIONS -d classes"

  (
    classpath "$JAVA_HOME/lib/jfxrt.jar"
    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
  ) || exit "$?"

  mkdir -p "$TARGET_DIR" || fail "Failed to create directory $TARGET_DIR"

  pushd classes >/dev/null

  CHARSET_SERVICE="META-INF/services/java.nio.charset.spi.CharsetProvider"
  mkdir -p "$(dirname "$CHARSET_SERVICE")"
  echo isabelle.Isabelle_Charset_Provider > "$CHARSET_SERVICE"

  cp "$ISABELLE_HOME/lib/logo/isabelle_transparent-32.gif" isabelle/.
  cp "$ISABELLE_HOME/lib/logo/isabelle_transparent.gif" isabelle/.

  isabelle_jdk jar cfe "$(platform_path "$TARGET")" isabelle.Main META-INF isabelle || \
    fail "Failed to produce $TARGET"

  popd >/dev/null

  rm -rf classes
fi