lib/Tools/console

prefer Variable.focus, despite subtle differences of Logic.strip_params vs. Term.strip_all_vars;

#!/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 SYSTEM_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)
      SYSTEM_OPTIONS["${#SYSTEM_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)"

mkdir -p "$ISABELLE_TMP_PREFIX" || exit $?
OPTIONS_FILE="$ISABELLE_TMP_PREFIX/options$$"

"$ISABELLE_TOOL" java "${JAVA_ARGS[@]}" isabelle.Build_Console \
  "$LOGIC" "$NO_BUILD" "$SYSTEM_MODE" "$OPTIONS_FILE" \
  "${INCLUDE_DIRS[@]}" $'\n' "${SYSTEM_OPTIONS[@]}" || {
  rm -f "$OPTIONS_FILE"
  exit "$?"
}

ISABELLE_OPTIONS["${#ISABELLE_OPTIONS[@]}"]="-O"
ISABELLE_OPTIONS["${#ISABELLE_OPTIONS[@]}"]="$OPTIONS_FILE"

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