lib/Tools/console

check and build Isabelle session for console tool -- avoid multiple Scala/JVM invocation;

#!/usr/bin/env bash
#
# Author: Makarius
#
# DESCRIPTION: run Isabelle process with raw ML console and line editor

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

function usage()
{
  echo
  echo "Usage: isabelle $PRG [OPTIONS]"
  echo
  echo "  Options are:"
  echo "    -d DIR       include session directory"
  echo "    -l NAME      logic session name (default ISABELLE_LOGIC=\"$ISABELLE_LOGIC\")"
  echo "    -m MODE      add print mode for output"
  echo "    -n           no build of session image on startup"
  echo "    -o OPTION    override Isabelle system OPTION (via NAME=VAL or NAME)"
  echo "    -s           system build mode for session image"
  echo
  echo "  Run Isabelle process with raw ML console and line editor"
  echo "  (ISABELLE_LINE_EDITOR=\"$ISABELLE_LINE_EDITOR\")."
  echo
  exit 1
}


## process command line

# options

declare -a ISABELLE_OPTIONS=()

declare -a INCLUDE_DIRS=()
LOGIC="$ISABELLE_LOGIC"
NO_BUILD="false"
declare -a BUILD_OPTIONS=()
SYSTEM_MODE="false"

while getopts "d:l:m:no:s" OPT
do
  case "$OPT" in
    d)
      INCLUDE_DIRS["${#INCLUDE_DIRS[@]}"]="$OPTARG"
      ;;
    l)
      LOGIC="$OPTARG"
      ;;
    m)
      ISABELLE_OPTIONS["${#ISABELLE_OPTIONS[@]}"]="-m"
      ISABELLE_OPTIONS["${#ISABELLE_OPTIONS[@]}"]="$OPTARG"
      ;;
    n)
      NO_BUILD="true"
      ;;
    o)
      ISABELLE_OPTIONS["${#ISABELLE_OPTIONS[@]}"]="-o"
      ISABELLE_OPTIONS["${#ISABELLE_OPTIONS[@]}"]="$OPTARG"
      BUILD_OPTIONS["${#BUILD_OPTIONS[@]}"]="$OPTARG"
      ;;
    s)
      SYSTEM_MODE="true"
      ;;
    \?)
      usage
      ;;
  esac
done

shift $(($OPTIND - 1))


# args

[ "$#" -ne 0 ] && { echo "Bad args: $*"; usage; }


## main

isabelle_admin_build jars || exit $?

declare -a JAVA_ARGS; eval "JAVA_ARGS=($ISABELLE_BUILD_JAVA_OPTIONS)"

"$ISABELLE_TOOL" java "${JAVA_ARGS[@]}" isabelle.Build_Console \
  "$LOGIC" "$NO_BUILD" "$SYSTEM_MODE" \
  "${INCLUDE_DIRS[@]}" $'\n' "${BUILD_OPTIONS[@]}" || exit "$?"

if type -p "$ISABELLE_LINE_EDITOR" > /dev/null
then
  exec "$ISABELLE_LINE_EDITOR" "$ISABELLE_PROCESS" "${ISABELLE_OPTIONS[@]}" -- "$LOGIC"
else
  echo "### No line editor: \"$ISABELLE_LINE_EDITOR\""
  exec "$ISABELLE_PROCESS" "${ISABELLE_OPTIONS[@]}" -- "$LOGIC"
fi