#!/usr/bin/env bash

#

# Author: Makarius

#

# DESCRIPTION: Isabelle/jEdit interface wrapper

## sources

declare -a SOURCES=(

  "src/active.scala"

  "src/completion_popup.scala"

  "src/dockable.scala"

  "src/document_model.scala"

  "src/document_view.scala"

  "src/documentation_dockable.scala"

  "src/find_dockable.scala"

  "src/fold_handling.scala"

  "src/graphview_dockable.scala"

  "src/html_panel.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_editor.scala"

  "src/jedit_lib.scala"

  "src/jedit_main.scala"

  "src/jedit_options.scala"

  "src/jedit_thy_load.scala"

  "src/monitor_dockable.scala"

  "src/osx_adapter.scala"

  "src/output_dockable.scala"

  "src/plugin.scala"

  "src/popup.scala"

  "src/pretty_text_area.scala"

  "src/pretty_tooltip.scala"

  "src/process_indicator.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/sledgehammer_dockable.scala"

  "src/symbols_dockable.scala"

  "src/syslog_dockable.scala"

  "src/text_overview.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-news.xml"

  "src/modes/isabelle-options.xml"

  "src/modes/isabelle-root.xml"

  "src/modes/isabelle.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"

  echo "    -m MODE      add print mode for output"

  echo "    -n           no build dialog for session image on startup"

  echo "    -s           system build mode for session image"

  echo

  echo "Start jEdit with Isabelle plugin setup and open 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=(-L jedit_logic)

BUILD_ONLY=false

BUILD_JARS="jars"

JEDIT_SESSION_DIRS=""

JEDIT_LOGIC=""

JEDIT_PRINT_MODE=""

NO_BUILD="false"

function getoptions()

{

  OPTIND=1

  while getopts "J:bd:fj:l:m:ns" 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)

        BUILD_DIALOG_OPTIONS["${#BUILD_DIALOG_OPTIONS[@]}"]="-l"

        BUILD_DIALOG_OPTIONS["${#BUILD_DIALOG_OPTIONS[@]}"]="$OPTARG"

        JEDIT_LOGIC="$OPTARG"

        ;;

      m)

        if [ -z "$JEDIT_PRINT_MODE" ]; then

          JEDIT_PRINT_MODE="$OPTARG"

        else

          JEDIT_PRINT_MODE="$JEDIT_PRINT_MODE,$OPTARG"

        fi

        ;;

      n)

        NO_BUILD="true"

        ;;

      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

  "$ISABELLE_TOOL" browser -b || exit $?

  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=(

  "Console.jar"

  "ErrorList.jar"

  "Highlight.jar"

  "SideKick.jar"

  "cobra.jar"

  "js.jar"

  "idea-icons.jar"

  "jsr305-2.0.0.jar"

)

declare -a JEDIT_BUILD_JARS=()

declare -a JEDIT_STARTUP_JARS=()

for NAME in "${JEDIT_JARS[@]}"

do

  JEDIT_BUILD_JARS["${#JEDIT_BUILD_JARS[@]}"]="$ISABELLE_JEDIT_BUILD_HOME/contrib/$NAME"

  JEDIT_STARTUP_JARS["${#JEDIT_STARTUP_JARS[@]}"]="$JEDIT_HOME/dist/jars/$NAME"

done

declare -a JFREECHART_JARS=()

for NAME in $JFREECHART_JAR_NAMES

do

  JFREECHART_JARS["${#JFREECHART_JARS[@]}"]="$JFREECHART_HOME/lib/$NAME"

done

# 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_BUILD_JARS[@]}" "${JFREECHART_JARS[@]}" "$XZ_JAVA_HOME/lib/xz.jar"

        "$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-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; }' dist/modes/catalog

  cp -p -R -f "${JEDIT_BUILD_JARS[@]}" dist/jars/. || failed

  (

    for JAR in "$JEDIT_JAR" "${JEDIT_BUILD_JARS[@]}" "${JFREECHART_JARS[@]}" \

      "$XZ_JAVA_HOME/lib/xz.jar" "$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

if [ "$BUILD_ONLY" = false ]; then

  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

  if [ "$NO_BUILD" = false ]; then

    "$ISABELLE_TOOL" build_dialog "${BUILD_DIALOG_OPTIONS[@]}"

    RC="$?"

    [ "$RC" = 0 ] || exit "$RC"

  fi

  JEDIT_CLASSPATH="$JEDIT_HOME/dist/jedit.jar"

  for JAR in "$JEDIT_HOME/dist/jars/Isabelle-jEdit.jar" "${JEDIT_STARTUP_JARS[@]}" \

    "${JFREECHART_JARS[@]}"

  do

    JEDIT_CLASSPATH="$JEDIT_CLASSPATH:$JAR"

  done

  JEDIT_CLASSPATH="$(jvmpath "$JEDIT_CLASSPATH")"

  export JEDIT_SESSION_DIRS JEDIT_LOGIC JEDIT_PRINT_MODE

  exec "$ISABELLE_TOOL" java "${JAVA_ARGS[@]}" \

    -classpath "$JEDIT_CLASSPATH" isabelle.jedit.JEdit_Main "${ARGS[@]}"

fi