src/Tools/jEdit/lib/Tools/jedit

support alternative ancestor session;

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


## sources

declare -a SOURCES_BASE=(
  "src-base/dockable.scala"
  "src-base/isabelle_encoding.scala"
  "src-base/jedit_lib.scala"
  "src-base/pide_docking_framework.scala"
  "src-base/plugin.scala"
  "src-base/syntax_style.scala"
)

declare -a RESOURCES_BASE=(
  "src-base/Isabelle_Base.props"
  "src-base/services.xml"
)

declare -a SOURCES=(
  "src/active.scala"
  "src/completion_popup.scala"
  "src/context_menu.scala"
  "src/debugger_dockable.scala"
  "src/document_model.scala"
  "src/document_view.scala"
  "src/documentation_dockable.scala"
  "src/fold_handling.scala"
  "src/font_info.scala"
  "src/graphview_dockable.scala"
  "src/info_dockable.scala"
  "src/isabelle.scala"
  "src/isabelle_encoding.scala"
  "src/isabelle_options.scala"
  "src/isabelle_sidekick.scala"
  "src/jedit_bibtex.scala"
  "src/jedit_editor.scala"
  "src/jedit_lib.scala"
  "src/jedit_options.scala"
  "src/jedit_rendering.scala"
  "src/jedit_resources.scala"
  "src/jedit_sessions.scala"
  "src/jedit_spell_checker.scala"
  "src/keymap_merge.scala"
  "src/monitor_dockable.scala"
  "src/output_dockable.scala"
  "src/plugin.scala"
  "src/pretty_text_area.scala"
  "src/pretty_tooltip.scala"
  "src/process_indicator.scala"
  "src/protocol_dockable.scala"
  "src/query_dockable.scala"
  "src/raw_output_dockable.scala"
  "src/rich_text_area.scala"
  "src/scala_console.scala"
  "src/session_build.scala"
  "src/simplifier_trace_dockable.scala"
  "src/simplifier_trace_window.scala"
  "src/sledgehammer_dockable.scala"
  "src/state_dockable.scala"
  "src/symbols_dockable.scala"
  "src/syntax_style.scala"
  "src/syslog_dockable.scala"
  "src/text_overview.scala"
  "src/text_structure.scala"
  "src/theories_dockable.scala"
  "src/timing_dockable.scala"
  "src/token_markup.scala"
)

declare -a RESOURCES=(
  "src/actions.xml"
  "src/dockables.xml"
  "src/Isabelle.props"
  "src/jEdit.props"
  "src/services.xml"
  "src/modes/isabelle-ml.xml"
  "src/modes/isabelle-news.xml"
  "src/modes/isabelle-options.xml"
  "src/modes/isabelle-root.xml"
  "src/modes/isabelle.xml"
  "src/modes/sml.xml"
)


## diagnostics

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

function usage()
{
  echo
  echo "Usage: isabelle $PRG [OPTIONS] [FILES ...]"
  echo
  echo "  Options are:"
  echo "    -A           specify ancestor for base session image (default: parent)"
  echo "    -B           use base session image, with theories from other sessions"
  echo "    -F           focus on selected logic session: ignore unrelated theories"
  echo "    -D NAME=X    set JVM system property"
  echo "    -J OPTION    add JVM runtime option"
  echo "                 (default $JEDIT_JAVA_SYSTEM_OPTIONS $JEDIT_JAVA_OPTIONS)"
  echo "    -P           use parent session image"
  echo "    -R           open ROOT entry of logic session"
  echo "    -S NAME      edit specified logic session, same as abbreviates -B -F -R -l NAME"
  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)"
  echo "    -l NAME      logic session name"
  echo "    -m MODE      add print mode for output"
  echo "    -n           no build of session image on startup"
  echo "    -p CMD       ML process command prefix (process policy)"
  echo "    -s           system build mode for session image"
  echo
  echo "  Start jEdit with Isabelle plugin setup and open FILES"
  echo "  (default \"$USER_HOME/Scratch.thy\" or \":\" for empty buffer)."
  echo
  exit 1
}

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

function failed()
{
  fail "Failed!"
}


## process command line

# options

BUILD_ONLY=false
BUILD_JARS="jars"
ML_PROCESS_POLICY=""
JEDIT_LOGIC_ANCESTOR=""
JEDIT_LOGIC_BASE=""
JEDIT_LOGIC_FOCUS=""
JEDIT_SESSION_DIRS=""
JEDIT_LOGIC_ROOT=""
JEDIT_LOGIC_PARENT=""
JEDIT_LOGIC=""
JEDIT_PRINT_MODE=""
JEDIT_BUILD_MODE="normal"

function getoptions()
{
  OPTIND=1
  while getopts "A:BFD:J:PRS:bd:fj:l:m:np:s" OPT
  do
    case "$OPT" in
      A)
        JEDIT_LOGIC_ANCESTOR="$OPTARG"
        ;;
      B)
        JEDIT_LOGIC_BASE="true"
        JEDIT_LOGIC_PARENT=""
        ;;
      D)
        JAVA_ARGS["${#JAVA_ARGS[@]}"]="-D$OPTARG"
        ;;
      F)
        JEDIT_LOGIC_FOCUS="true"
        ;;
      J)
        JAVA_ARGS["${#JAVA_ARGS[@]}"]="$OPTARG"
        ;;
      P)
        JEDIT_LOGIC_PARENT="true"
        JEDIT_LOGIC_BASE=""
        ;;
      R)
        JEDIT_LOGIC_ROOT="true"
        ;;
      S)
        JEDIT_LOGIC="$OPTARG"
        JEDIT_LOGIC_BASE="true"
        JEDIT_LOGIC_PARENT=""
        JEDIT_LOGIC_FOCUS="true"
        JEDIT_LOGIC_ROOT="true"
        ;;
      b)
        BUILD_ONLY=true
        ;;
      d)
        if [ -z "$JEDIT_SESSION_DIRS" ]; then
          JEDIT_SESSION_DIRS="$OPTARG"
        else
          JEDIT_SESSION_DIRS="$JEDIT_SESSION_DIRS:$OPTARG"
        fi
        ;;
      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
        ;;
      n)
        JEDIT_BUILD_MODE="none"
        ;;
      p)
        ML_PROCESS_POLICY="$OPTARG"
        ;;
      s)
        JEDIT_BUILD_MODE="system"
        ;;
      \?)
        usage
        ;;
    esac
  done
}

eval "declare -a JAVA_ARGS=($JEDIT_JAVA_SYSTEM_OPTIONS $JEDIT_JAVA_OPTIONS)"

declare -a ARGS=()

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

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


# args

while [ "$#" -gt 0 ]; do
  ARGS["${#ARGS[@]}"]="$(platform_path "$1")"
  shift
done


## dependencies

if [ -e "$ISABELLE_HOME/Admin/build" ]; then
  isabelle browser -b || exit $?
  "$ISABELLE_HOME/Admin/build" "$BUILD_JARS" || exit $?
fi

PURE_JAR="$ISABELLE_HOME/lib/classes/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/Code2HTML.jar"
  "$ISABELLE_JEDIT_BUILD_HOME/contrib/CommonControls.jar"
  "$ISABELLE_JEDIT_BUILD_HOME/contrib/Console.jar"
  "$ISABELLE_JEDIT_BUILD_HOME/contrib/ErrorList.jar"
  "$ISABELLE_JEDIT_BUILD_HOME/contrib/Highlight.jar"
  "$ISABELLE_JEDIT_BUILD_HOME/contrib/kappalayout.jar"
  "$ISABELLE_JEDIT_BUILD_HOME/contrib/MacOSX.jar"
  "$ISABELLE_JEDIT_BUILD_HOME/contrib/Navigator.jar"
  "$ISABELLE_JEDIT_BUILD_HOME/contrib/SideKick.jar"
  "$ISABELLE_JEDIT_BUILD_HOME/contrib/idea-icons.jar"
  "$ISABELLE_JEDIT_BUILD_HOME/contrib/jsr305-2.0.0.jar"
)


# target

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

declare -a UPDATED=()

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


# build

function init_resources ()
{
  mkdir -p dist/classes || failed
  cp -p -R -f "$@" dist/classes/.
}

function compile_sources ()
{
  (
    #FIXME workarounds for scalac 2.11.0
    export CYGWIN="nodosfilewarning"
    function stty() { :; }
    export -f stty

    for JAR in "$JEDIT_JAR" "${JEDIT_JARS[@]}" "$PURE_JAR"
    do
      classpath "$JAR"
    done
    export CLASSPATH="$(platform_path "$ISABELLE_CLASSPATH")"
    isabelle_scala scalac $ISABELLE_SCALAC_OPTIONS -d dist/classes "$@"
  ) || fail "Failed to compile sources"
}

function make_jar ()
{
  cd dist/classes
  isabelle_jdk jar cf "../../$1" * || failed
  cd ../..
  rm -rf dist/classes
}

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 || failed

  cp -p -R -f "$ISABELLE_JEDIT_BUILD_HOME/contrib/$ISABELLE_JEDIT_BUILD_VERSION/." dist/.

  init_resources "${RESOURCES_BASE[@]}"
  compile_sources "${SOURCES_BASE[@]}"
  make_jar "$TARGET_BASE"
  classpath "$PWD/$TARGET_BASE"

  init_resources "${RESOURCES[@]}"
  cp src/jEdit.props dist/properties/.
  cp -p -R -f src/modes/. dist/modes/.

  perl -i -e 'while (<>) {
    if (m/FILE="ml.xml"/ or m/FILE_NAME_GLOB="...sml,ml."/) { }
    elsif (m/NAME="javacc"/) {
      print qq!<MODE NAME="isabelle" FILE="isabelle.xml" FILE_NAME_GLOB="{*.thy,ROOT0.ML,ROOT.ML}"/>\n\n!;
      print qq!<MODE NAME="isabelle-ml" FILE="isabelle-ml.xml" FILE_NAME_GLOB="*.ML"/>\n\n!;
      print qq!<MODE NAME="isabelle-news" FILE="isabelle-news.xml"/>\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!;
      print;
    }
    elsif (m/NAME="sqr"/) {
      print qq!<MODE NAME="sml" FILE="sml.xml" FILE_NAME_GLOB="*.{sml,sig}"/>\n\n!;
      print;
    }
    else { print; }
  }' dist/modes/catalog

  cd dist
  isabelle_jdk jar xf jedit.jar
  cp "$ISABELLE_HOME/lib/logo/isabelle_transparent-32.gif" \
    "org/gjt/sp/jedit/icons/themes/classic/32x32/apps/isabelle.gif" || failed
  cp "$ISABELLE_HOME/lib/logo/isabelle_transparent-32.gif" \
    "org/gjt/sp/jedit/icons/themes/tango/32x32/apps/isabelle.gif" || failed
  isabelle_jdk jar cfe jedit.jar org.gjt.sp.jedit.jEdit org || failed
  rm -rf META-INF org
  cd ..

  cp -p -R -f "${JEDIT_JARS[@]}" dist/jars/. || failed
  compile_sources "${SOURCES[@]}"
  make_jar "$TARGET"

  cp "$ISABELLE_JEDIT_BUILD_HOME/doc/jedit5.4.0manual-a4.pdf" dist/doc/jedit-manual.pdf
  cp dist/doc/CHANGES.txt dist/doc/jedit-changes
  cat > dist/doc/Contents <<EOF
Original jEdit Documentation
  jedit-manual    jEdit 5.4 User's Guide
  jedit-changes   jEdit 5.4 Version History

EOF

fi

popd >/dev/null


## main

if [ "$BUILD_ONLY" = false ]
then
  export JEDIT_SESSION_DIRS JEDIT_LOGIC JEDIT_LOGIC_ANCESTOR JEDIT_LOGIC_BASE JEDIT_LOGIC_FOCUS \
    JEDIT_LOGIC_PARENT JEDIT_LOGIC_ROOT JEDIT_PRINT_MODE JEDIT_BUILD_MODE
  export JEDIT_ML_PROCESS_POLICY="$ML_PROCESS_POLICY"
  classpath "$JEDIT_HOME/dist/jedit.jar"
  exec isabelle java "${JAVA_ARGS[@]}" isabelle.Main "${ARGS[@]}"
fi