src/Tools/jEdit/lib/Tools/jedit

implicit build_dialog for Isabelle/jEdit;
clarified option -l: refer to session name, not image path;

#!/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/graphview_dockable.scala"
  "src/html_panel.scala"
  "src/hyperlink.scala"
  "src/info_dockable.scala"
  "src/isabelle.scala"
  "src/isabelle_encoding.scala"
  "src/isabelle_logic.scala"
  "src/isabelle_options.scala"
  "src/isabelle_sidekick.scala"
  "src/jedit_lib.scala"
  "src/jedit_main.scala"
  "src/jedit_options.scala"
  "src/jedit_thy_load.scala"
  "src/output_dockable.scala"
  "src/plugin.scala"
  "src/pretty_text_area.scala"
  "src/pretty_tooltip.scala"
  "src/protocol_dockable.scala"
  "src/raw_output_dockable.scala"
  "src/readme_dockable.scala"
  "src/rendering.scala"
  "src/rich_text_area.scala"
  "src/scala_console.scala"
  "src/sendback.scala"
  "src/symbols_dockable.scala"
  "src/syslog_dockable.scala"
  "src/text_overview.scala"
  "src/theories_dockable.scala"
  "src/token_markup.scala"
)

declare -a RESOURCES=(
  "src/actions.xml"
  "src/dockables.xml"
  "src/Isabelle.props"
  "src/jEdit.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 DIR       include session directory"
  echo "    -f           fresh build"
  echo "    -j OPTION    add jEdit runtime option"
  echo "                 (default JEDIT_OPTIONS=$JEDIT_OPTIONS)"
  echo "    -l NAME      logic session name (default ISABELLE_LOGIC=$ISABELLE_LOGIC)"
  echo "    -m MODE      add print mode for output"
  echo "    -s           system build mode for session image"
  echo
  echo "Start jEdit with Isabelle plugin setup and opens theory FILES"
  echo "(default \"$USER_HOME/Scratch.thy\")."
  echo
  exit 1
}

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

function failed()
{
  fail "Failed!"
}


## process command line

# options

declare -a BUILD_DIALOG_OPTIONS=()

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

function getoptions()
{
  OPTIND=1
  while getopts "J:bd:fj:l:m:s" OPT
  do
    case "$OPT" in
      J)
        JAVA_ARGS["${#JAVA_ARGS[@]}"]="$OPTARG"
        ;;
      b)
        BUILD_ONLY=true
        ;;
      d)
        if [ -z "$JEDIT_SESSION_DIRS" ]; then
          JEDIT_SESSION_DIRS="$OPTARG"
        else
          JEDIT_SESSION_DIRS="$JEDIT_SESSION_DIRS:$OPTARG"
        fi
        BUILD_DIALOG_OPTIONS["${#BUILD_DIALOG_OPTIONS[@]}"]="-d"
        BUILD_DIALOG_OPTIONS["${#BUILD_DIALOG_OPTIONS[@]}"]="$OPTARG"
        ;;
      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
        ;;
      s)
        BUILD_DIALOG_OPTIONS["${#BUILD_DIALOG_OPTIONS[@]}"]="-s"
        ;;
      \?)
        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[@]}"]="$(jvmpath "$USER_HOME/Scratch.thy")"
else
  while [ "$#" -gt 0 ]; do
    ARGS["${#ARGS[@]}"]="$(jvmpath "$1")"
    shift
  done
fi


## dependencies

if [ -e "$ISABELLE_HOME/Admin/build" ]; then
  if [ "$BUILD_JARS" = jars_fresh ]; then
    "$ISABELLE_TOOL" graphview -b -f || exit $?
  else
    "$ISABELLE_HOME/Admin/build" "$BUILD_JARS" || exit $?
    "$ISABELLE_TOOL" graphview -b || exit $?
  fi
fi

PURE_JAR="$ISABELLE_HOME/lib/classes/ext/Pure.jar"
GRAPHVIEW_JAR="$ISABELLE_HOME/lib/classes/ext/Graphview.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/SideKick.jar"
  "$ISABELLE_JEDIT_BUILD_HOME/contrib/cobra.jar"
  "$ISABELLE_JEDIT_BUILD_HOME/contrib/js.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" "$GRAPHVIEW_JAR" "${SOURCES[@]}" "${RESOURCES[@]}"
      )
    elif [ -e "$ISABELLE_HOME/Admin/build" ]; then
      declare -a DEPS=("$PURE_JAR" "$GRAPHVIEW_JAR" "${SOURCES[@]}" "${RESOURCES[@]}")
    else
      declare -a DEPS=()
    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 -p -R -f "$ISABELLE_JEDIT_BUILD_HOME/contrib/$ISABELLE_JEDIT_BUILD_VERSION/." dist/.
  cp -p -R -f "${RESOURCES[@]}" dist/classes/.
  cp src/jEdit.props dist/properties/.
  cp -p -R -f src/modes/. 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-options" FILE="isabelle-options.xml"/>\n\n,;
      print qq,<MODE NAME="isabelle-root" FILE="isabelle-root.xml" FILE_NAME_GLOB="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 -p -R -f "${JEDIT_JARS[@]}" dist/jars/. || failed
  (
    for JAR in "$JEDIT_JAR" "${JEDIT_JARS[@]}" "$PURE_JAR" "$GRAPHVIEW_JAR" \
      "$SCALA_HOME/lib/scala-compiler.jar"
    do
      CLASSPATH="$CLASSPATH:$JAR"
    done
    CLASSPATH="$(jvmpath "$CLASSPATH")"
    exec "$SCALA_HOME/bin/scalac" $ISABELLE_SCALA_BUILD_OPTIONS -d dist/classes "${SOURCES[@]}"
  ) || fail "Failed to compile sources"

  cd dist/classes
  isabelle_jdk 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-readme" 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


# build logic

"$ISABELLE_TOOL" build_dialog "${BUILD_DIALOG_OPTIONS[@]}" -C "$JEDIT_LOGIC"
RC="$?"
[ "$RC" = 0 ] || exit "$RC"


# main

[ "$BUILD_ONLY" = true ] || {
  export JEDIT_SESSION_DIRS JEDIT_LOGIC JEDIT_PRINT_MODE

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