src/Tools/jEdit/lib/Tools/jedit

build auxiliary jEdit component in Isabelle/Scala;
clarified directory layout;

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


## sources

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

declare -a RESOURCES0=(
  "src/Tools/jEdit/src-base/Isabelle_Base.props"
  "src/Tools/jEdit/src-base/services.xml"
)

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

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


## diagnostics

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

function usage()
{
  echo
  echo "Usage: isabelle $PRG [OPTIONS] [FILES ...]"
  echo
  echo "  Options are:"
  echo "    -A NAME      ancestor session for option -R (default: parent)"
  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 "    -R NAME      build image with requirements from other sessions"
  echo "    -b           build only"
  echo "    -d DIR       include session directory"
  echo "    -f           fresh build"
  echo "    -i NAME      include session in name-space of theories"
  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 (system_heaps=true)"
  echo "    -u           user build mode for session image (system_heaps=false)"
  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
FRESH_BUILD=""
ML_PROCESS_POLICY=""
JEDIT_LOGIC_ANCESTOR=""
JEDIT_LOGIC_REQUIREMENTS=""
JEDIT_INCLUDE_SESSIONS=""
JEDIT_SESSION_DIRS="-"
JEDIT_LOGIC=""
JEDIT_PRINT_MODE=""
JEDIT_NO_BUILD=""
JEDIT_BUILD_MODE="default"

function getoptions()
{
  OPTIND=1
  while getopts "A:BFD:J:R:bd:fi:j:l:m:np:su" OPT
  do
    case "$OPT" in
      A)
        JEDIT_LOGIC_ANCESTOR="$OPTARG"
        ;;
      D)
        JAVA_ARGS["${#JAVA_ARGS[@]}"]="-D$OPTARG"
        ;;
      J)
        JAVA_ARGS["${#JAVA_ARGS[@]}"]="$OPTARG"
        ;;
      R)
        JEDIT_LOGIC="$OPTARG"
        JEDIT_LOGIC_REQUIREMENTS="true"
        ;;
      b)
        BUILD_ONLY=true
        ;;
      d)
        JEDIT_SESSION_DIRS="$JEDIT_SESSION_DIRS:$OPTARG"
        ;;
      i)
        if [ -z "$JEDIT_INCLUDE_SESSIONS" ]; then
          JEDIT_INCLUDE_SESSIONS="$OPTARG"
        else
          JEDIT_INCLUDE_SESSIONS="$JEDIT_INCLUDE_SESSIONS:$OPTARG"
        fi
        ;;
      f)
        FRESH_BUILD="true"
        ;;
      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_NO_BUILD="true"
        ;;
      p)
        ML_PROCESS_POLICY="$OPTARG"
        ;;
      s)
        JEDIT_BUILD_MODE="system"
        ;;
      u)
        JEDIT_BUILD_MODE="user"
        ;;
      \?)
        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 $?
  if [ -n "$FRESH_BUILD" ]; then
    "$ISABELLE_HOME/Admin/build" jars_fresh || exit $?
  else
    "$ISABELLE_HOME/Admin/build" jars || exit $?
  fi
elif [ -n "$FRESH_BUILD" ]; then
  echo >&2 "### Ignoring fresh build option: not a repository clone"
  FRESH_BUILD=""
fi


# target

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

TARGET_DIR="src/Tools/jEdit/dist"
TARGET_JAR0="$TARGET_DIR/jars/Isabelle-jEdit-base.jar"
TARGET_JAR="$TARGET_DIR/jars/Isabelle-jEdit.jar"
TARGET_SHASUM="$TARGET_DIR/Isabelle-jEdit.shasum"

declare -a TARGET_DEPS=("lib/classes/Pure.jar" "$TARGET_DIR/jedit.jar")
for DEP in "$TARGET_DIR"/jars/*.jar
do
  TARGET_DEPS["${#TARGET_DEPS[@]}"]="$DEP"
done

function target_shasum()
(
  shasum -a1 -b "$TARGET_JAR0" "$TARGET_JAR" "${TARGET_DEPS[@]}" \
    "${SOURCES0[@]}" "${RESOURCES0[@]}" "${SOURCES[@]}" "${RESOURCES[@]}" 2>/dev/null
)

function target_clean()
{
  rm -rf "$ISABELLE_HOME/$TARGET_DIR"
}

[ -n "$FRESH_BUILD" ] && target_clean


## build

BUILD_DIR="$TARGET_DIR/build"

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

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

    for DEP in "${TARGET_DEPS[@]}"
    do
      classpath "$DEP"
    done
    export CLASSPATH="$(platform_path "$ISABELLE_CLASSPATH")"
    isabelle_scala scalac $ISABELLE_SCALAC_OPTIONS -d "$BUILD_DIR" "$@"
  ) || fail "Failed to compile sources"
}

function make_jar()
{
  isabelle_jdk jar -c -f "$1" -C "$BUILD_DIR" . || failed
  rm -rf "$ISABELLE_HOME/$BUILD_DIR"
}

target_shasum | cmp "$TARGET_SHASUM" >/dev/null 2>/dev/null
if [ -e "$ISABELLE_HOME/Admin/build" -a "$?" -ne 0 ]; then
  echo "### Building Isabelle/jEdit ..."

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

  target_clean || failed
  mkdir -p "$TARGET_DIR" || failed

  cp -p -R "$ISABELLE_JEDIT_BUILD_HOME/$ISABELLE_JEDIT_BUILD_VERSION/." "$TARGET_DIR/."

  init_resources "${RESOURCES0[@]}"
  compile_sources "${SOURCES0[@]}"
  make_jar "$TARGET_JAR0"
  classpath "$TARGET_JAR0"

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

  perl -i -e 'while (<>) {
    if (m/FILE="ml.xml"/ or m/FILE_NAME_GLOB="...sml,ml."/ or m/FILE_NAME_GLOB="..ftl"/) { }
    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; }
  }' "$TARGET_DIR/modes/catalog"

  (
    cd "$TARGET_DIR"
    isabelle_jdk jar -x -f 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 -c -f jedit.jar -e org.gjt.sp.jedit.jEdit org || failed
    rm -rf META-INF org
  )

  compile_sources "${SOURCES[@]}"
  make_jar "$TARGET_JAR"

  target_shasum > "$TARGET_SHASUM"

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

EOF

fi


## main

popd >/dev/null

if [ "$BUILD_ONLY" = false ]
then
  "$ISABELLE_HOME/lib/scripts/java-gui-setup"

  export JEDIT_SESSION_DIRS JEDIT_LOGIC JEDIT_LOGIC_ANCESTOR JEDIT_LOGIC_REQUIREMENTS \
    JEDIT_INCLUDE_SESSIONS JEDIT_PRINT_MODE JEDIT_NO_BUILD JEDIT_BUILD_MODE
  export JEDIT_ML_PROCESS_POLICY="$ML_PROCESS_POLICY"
  classpath "$JEDIT_HOME/dist/jedit.jar"
  exec isabelle java -splash:"$(platform_path "$ISABELLE_HOME/lib/logo/isabelle.gif")" \
    "${JAVA_ARGS[@]}" isabelle.Main "${ARGS[@]}"
fi