src/Tools/jEdit/lib/Tools/jedit

quickcheck-random compilation also indicates if the counterexample is potentially spurious or not

#!/usr/bin/env bash
#
# Author: Makarius
#
# DESCRIPTION: Isabelle/jEdit interface wrapper


## sources

declare -a SOURCES=(
  "src/dockable.scala"
  "src/document_model.scala"
  "src/document_view.scala"
  "src/html_panel.scala"
  "src/isabelle_encoding.scala"
  "src/isabelle_hyperlinks.scala"
  "src/isabelle_options.scala"
  "src/isabelle_rendering.scala"
  "src/isabelle_sidekick.scala"
  "src/jedit_thy_load.scala"
  "src/output_dockable.scala"
  "src/plugin.scala"
  "src/protocol_dockable.scala"
  "src/raw_output_dockable.scala"
  "src/scala_console.scala"
  "src/session_dockable.scala"
  "src/text_area_painter.scala"
  "src/token_markup.scala"
)

declare -a RESOURCES=(
  "src/actions.xml"
  "src/dockables.xml"
  "src/Isabelle.props"
  "src/services.xml"
)


## diagnostics

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

function usage()
{
  echo
  echo "Usage: isabelle $PRG [OPTIONS] [FILES ...]"
  echo
  echo "  Options are:"
  echo "    -J OPTION    add JVM runtime option"
  echo "                 (default JEDIT_JAVA_OPTIONS=$JEDIT_JAVA_OPTIONS)"
  echo "    -b           build only"
  echo "    -d           enable debugger"
  echo "    -f           fresh build"
  echo "    -j OPTION    add jEdit runtime option"
  echo "                 (default JEDIT_OPTIONS=$JEDIT_OPTIONS)"
  echo "    -l NAME      logic image name (default ISABELLE_LOGIC=$ISABELLE_LOGIC)"
  echo "    -m MODE      add print mode for output"
  echo
  echo "Start jEdit with Isabelle plugin setup and opens theory FILES"
  echo "(default Scratch.thy)."
  echo
  exit 1
}

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

function failed()
{
  fail "Failed!"
}


## process command line

# options

BUILD_ONLY=false
BUILD_JARS="jars"
JEDIT_LOGIC="$ISABELLE_LOGIC"
JEDIT_PRINT_MODE=""

function getoptions()
{
  OPTIND=1
  while getopts "J:bdfj:l:m:" OPT
  do
    case "$OPT" in
      J)
        JAVA_ARGS["${#JAVA_ARGS[@]}"]="$OPTARG"
        ;;
      b)
        BUILD_ONLY=true
        ;;
      d)
        JAVA_ARGS["${#JAVA_ARGS[@]}"]="-Xdebug"
        JAVA_ARGS["${#JAVA_ARGS[@]}"]="-Xrunjdwp:transport=dt_socket,server=y,suspend=n"
        ;;
      f)
        BUILD_JARS="jars_fresh"
        ;;
      j)
        ARGS["${#ARGS[@]}"]="$OPTARG"
        ;;
      l)
        JEDIT_LOGIC="$OPTARG"
        ;;
      m)
        if [ -z "$JEDIT_PRINT_MODE" ]; then
          JEDIT_PRINT_MODE="$OPTARG"
        else
          JEDIT_PRINT_MODE="$JEDIT_PRINT_MODE,$OPTARG"
        fi
        ;;
      \?)
        usage
        ;;
    esac
  done
}

declare -a JAVA_ARGS; eval "JAVA_ARGS=($JEDIT_JAVA_OPTIONS $JEDIT_SYSTEM_OPTIONS)"
[ -n "$SCALA_HOME" ] && JAVA_ARGS["${#JAVA_ARGS[@]}"]="-Dscala.home=$SCALA_HOME"

declare -a ARGS; eval "ARGS=($JEDIT_OPTIONS)"

declare -a OPTIONS; eval "OPTIONS=($ISABELLE_JEDIT_OPTIONS)"
getoptions "${OPTIONS[@]}"

getoptions "$@"
shift $(($OPTIND - 1))


# args

if [ "$#" -eq 0 ]; then
  ARGS["${#ARGS[@]}"]="Scratch.thy"
else
  while [ "$#" -gt 0 ]; do
    ARGS["${#ARGS[@]}"]="$(jvmpath "$1")"
    shift
  done
fi


## dependencies

[ -e "$ISABELLE_HOME/Admin/build" ] && \
  { "$ISABELLE_HOME/Admin/build" "$BUILD_JARS" || exit $?; }

PURE_JAR="$ISABELLE_HOME/lib/classes/ext/Pure.jar"

pushd "$JEDIT_HOME" >/dev/null || failed

JEDIT_JAR="$ISABELLE_JEDIT_BUILD_HOME/contrib/$ISABELLE_JEDIT_BUILD_VERSION/jedit.jar"

JEDIT_JARS=(
  "$ISABELLE_JEDIT_BUILD_HOME/contrib/Console.jar"
  "$ISABELLE_JEDIT_BUILD_HOME/contrib/ErrorList.jar"
  "$ISABELLE_JEDIT_BUILD_HOME/contrib/Hyperlinks.jar"
  "$ISABELLE_JEDIT_BUILD_HOME/contrib/SideKick.jar"
  "$ISABELLE_JEDIT_BUILD_HOME/contrib/cobra.jar"
  "$ISABELLE_JEDIT_BUILD_HOME/contrib/js.jar"
)

SCALA_JARS=(
  "$SCALA_HOME/lib/scala-compiler.jar"
  "$SCALA_HOME/lib/scala-library.jar"
  "$SCALA_HOME/lib/scala-swing.jar"
)


# target

TARGET="dist/jars/Isabelle-jEdit.jar"

declare -a UPDATED=()

if [ "$BUILD_JARS" = jars_fresh ]; then
  OUTDATED=true
else
  OUTDATED=false
  if [ ! -e "$TARGET" ]; then
    OUTDATED=true
  else
    if [ -n "$ISABELLE_JEDIT_BUILD_HOME" ]; then
      declare -a DEPS=("$JEDIT_JAR" "${JEDIT_JARS[@]}" "$PURE_JAR" "${SOURCES[@]}" "${RESOURCES[@]}")
    else
      declare -a DEPS=("$PURE_JAR" "${SOURCES[@]}" "${RESOURCES[@]}")
    fi
    for DEP in "${DEPS[@]}"
    do
      [ ! -e "$DEP" ] && fail "Missing file: $DEP"
      [ "$DEP" -nt "$TARGET" ] && {
        OUTDATED=true
        UPDATED["${#UPDATED[@]}"]="$DEP"
      }
    done
  fi
fi


# build

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

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

  [ -z "$ISABELLE_JEDIT_BUILD_HOME" ] && \
    fail "Unknown ISABELLE_JEDIT_BUILD_HOME -- missing auxiliary component"

  rm -rf dist || failed
  mkdir -p dist dist/classes || failed

  cp -pR "$ISABELLE_JEDIT_BUILD_HOME/contrib/$ISABELLE_JEDIT_BUILD_VERSION/." dist/.
  cp -pR "${RESOURCES[@]}" dist/classes/.
  cp src/jEdit.props dist/properties/.
  cp -pR src/modes/. dist/modes/.
  cp -pR "$SCALA_HOME/misc/scala-tool-support/jedit/modes/scala.xml" dist/modes/.

  perl -i -e 'while (<>) {
    if (m/NAME="javacc"/) {
      print qq,<MODE NAME="isabelle" FILE="isabelle.xml" FILE_NAME_GLOB="*.thy"/>\n\n,;
      print qq,<MODE NAME="isabelle-session" FILE="isabelle-session.xml" FILE_NAME_GLOB="session.root"/>\n\n,; }
    elsif (m/NAME="scheme"/) {
      print qq,<MODE NAME="scala" FILE="scala.xml" FILE_NAME_GLOB="*.scala" />\n\n,; }
    print; }' dist/modes/catalog

  cp -pR "${JEDIT_JARS[@]}" "$SCALA_HOME/lib/scala-compiler.jar" dist/jars/. || failed
  (
    for JAR in "$JEDIT_JAR" "${JEDIT_JARS[@]}" "$PURE_JAR" "$SCALA_HOME/lib/scala-compiler.jar"
    do
      CLASSPATH="$CLASSPATH:$JAR"
    done
    CLASSPATH="$(jvmpath "$CLASSPATH")"
    exec "$SCALA_HOME/bin/scalac" -unchecked -deprecation \
      -d dist/classes -target:jvm-1.5 "${SOURCES[@]}"
  ) || fail "Failed to compile sources"

  cd dist/classes
  jar cf "../jars/Isabelle-jEdit.jar" * || failed
  cd ../..
  rm -rf dist/classes
fi

popd >/dev/null


## main

# perspective

mkdir -p "$JEDIT_SETTINGS/DockableWindowManager"

if [ ! -e "$JEDIT_SETTINGS/perspective.xml" ]; then
  cat > "$JEDIT_SETTINGS/DockableWindowManager/perspective-view0.xml" <<EOF
<DOCKING LEFT="" TOP="" RIGHT="" BOTTOM="isabelle-session" LEFT_POS="0" TOP_POS="0" RIGHT_POS="250" BOTTOM_POS="250" />
EOF
  cat > "$JEDIT_SETTINGS/perspective.xml" <<EOF
<?xml version="1.0" encoding="UTF-8" ?>
<!DOCTYPE PERSPECTIVE SYSTEM "perspective.dtd">
<PERSPECTIVE>
<VIEW PLAIN="FALSE">
<GEOMETRY X="0" Y="35" WIDTH="1072" HEIGHT="787" EXT_STATE="0" />
</VIEW>
</PERSPECTIVE>
EOF
fi


# run

[ "$BUILD_ONLY" = true ] || {
  case "$JEDIT_LOGIC" in
    /*)
      ;;
    */*)
      JEDIT_LOGIC="$(pwd -P)/$JEDIT_LOGIC"
      ;;
  esac

  export JEDIT_LOGIC JEDIT_PRINT_MODE

  exec "$ISABELLE_TOOL" java "${JAVA_ARGS[@]}" \
    -jar "$(jvmpath "$JEDIT_HOME/dist/jedit.jar")" \
    "-settings=$(jvmpath "$JEDIT_SETTINGS")" "${ARGS[@]}"
}