lib/Tools/console
author wenzelm
Fri Jan 01 16:40:47 2016 +0100 (2016-01-01)
changeset 62028 2ecee4679f99
parent 61958 0a5dd617a88c
child 62047 1ae53588dcbb
permissions -rwxr-xr-x
updated for release;
wenzelm@25632
     1
#!/usr/bin/env bash
wenzelm@25632
     2
#
wenzelm@57439
     3
# Author: Makarius
wenzelm@25632
     4
#
wenzelm@57439
     5
# DESCRIPTION: run Isabelle process with raw ML console and line editor
wenzelm@25632
     6
wenzelm@61135
     7
## settings
wenzelm@61135
     8
wenzelm@61135
     9
case "$ISABELLE_JAVA_PLATFORM" in
wenzelm@61135
    10
  x86-*)
wenzelm@61135
    11
    ISABELLE_BUILD_JAVA_OPTIONS="$ISABELLE_BUILD_JAVA_OPTIONS32"
wenzelm@61135
    12
    ;;
wenzelm@61135
    13
  x86_64-*)
wenzelm@61135
    14
    ISABELLE_BUILD_JAVA_OPTIONS="$ISABELLE_BUILD_JAVA_OPTIONS64"
wenzelm@61135
    15
    ;;
wenzelm@61135
    16
esac
wenzelm@61135
    17
wenzelm@61135
    18
wenzelm@61135
    19
## diagnostics
wenzelm@61135
    20
wenzelm@25632
    21
PRG="$(basename "$0")"
wenzelm@25632
    22
wenzelm@25632
    23
function usage()
wenzelm@25632
    24
{
wenzelm@25632
    25
  echo
wenzelm@28650
    26
  echo "Usage: isabelle $PRG [OPTIONS]"
wenzelm@25632
    27
  echo
wenzelm@25632
    28
  echo "  Options are:"
wenzelm@57439
    29
  echo "    -d DIR       include session directory"
wenzelm@57439
    30
  echo "    -l NAME      logic session name (default ISABELLE_LOGIC=\"$ISABELLE_LOGIC\")"
wenzelm@25632
    31
  echo "    -m MODE      add print mode for output"
wenzelm@57439
    32
  echo "    -n           no build of session image on startup"
wenzelm@52062
    33
  echo "    -o OPTION    override Isabelle system OPTION (via NAME=VAL or NAME)"
wenzelm@57439
    34
  echo "    -s           system build mode for session image"
wenzelm@25632
    35
  echo
wenzelm@57439
    36
  echo "  Run Isabelle process with raw ML console and line editor"
wenzelm@57439
    37
  echo "  (ISABELLE_LINE_EDITOR=\"$ISABELLE_LINE_EDITOR\")."
wenzelm@25632
    38
  echo
wenzelm@25632
    39
  exit 1
wenzelm@25632
    40
}
wenzelm@25632
    41
wenzelm@25632
    42
wenzelm@25632
    43
## process command line
wenzelm@25632
    44
wenzelm@25632
    45
# options
wenzelm@25632
    46
wenzelm@61958
    47
declare -a ISABELLE_OPTIONS=(-m ASCII)
wenzelm@57580
    48
wenzelm@57580
    49
declare -a INCLUDE_DIRS=()
wenzelm@57580
    50
LOGIC="$ISABELLE_LOGIC"
wenzelm@57580
    51
NO_BUILD="false"
wenzelm@57581
    52
declare -a SYSTEM_OPTIONS=()
wenzelm@57580
    53
SYSTEM_MODE="false"
wenzelm@25632
    54
wenzelm@57439
    55
while getopts "d:l:m:no:s" OPT
wenzelm@25632
    56
do
wenzelm@25632
    57
  case "$OPT" in
wenzelm@57439
    58
    d)
wenzelm@57580
    59
      INCLUDE_DIRS["${#INCLUDE_DIRS[@]}"]="$OPTARG"
wenzelm@57439
    60
      ;;
wenzelm@25632
    61
    l)
wenzelm@25632
    62
      LOGIC="$OPTARG"
wenzelm@25632
    63
      ;;
wenzelm@25632
    64
    m)
wenzelm@52062
    65
      ISABELLE_OPTIONS["${#ISABELLE_OPTIONS[@]}"]="-m"
wenzelm@52062
    66
      ISABELLE_OPTIONS["${#ISABELLE_OPTIONS[@]}"]="$OPTARG"
wenzelm@52062
    67
      ;;
wenzelm@57439
    68
    n)
wenzelm@57580
    69
      NO_BUILD="true"
wenzelm@57439
    70
      ;;
wenzelm@52062
    71
    o)
wenzelm@57581
    72
      SYSTEM_OPTIONS["${#SYSTEM_OPTIONS[@]}"]="$OPTARG"
wenzelm@25632
    73
      ;;
wenzelm@57439
    74
    s)
wenzelm@57580
    75
      SYSTEM_MODE="true"
wenzelm@25632
    76
      ;;
wenzelm@25632
    77
    \?)
wenzelm@25632
    78
      usage
wenzelm@25632
    79
      ;;
wenzelm@25632
    80
  esac
wenzelm@25632
    81
done
wenzelm@25632
    82
wenzelm@25632
    83
shift $(($OPTIND - 1))
wenzelm@25632
    84
wenzelm@25632
    85
wenzelm@25632
    86
# args
wenzelm@25632
    87
wenzelm@25632
    88
[ "$#" -ne 0 ] && { echo "Bad args: $*"; usage; }
wenzelm@25632
    89
wenzelm@25632
    90
wenzelm@25632
    91
## main
wenzelm@25632
    92
wenzelm@57580
    93
isabelle_admin_build jars || exit $?
wenzelm@57580
    94
wenzelm@57580
    95
declare -a JAVA_ARGS; eval "JAVA_ARGS=($ISABELLE_BUILD_JAVA_OPTIONS)"
wenzelm@57580
    96
wenzelm@57686
    97
mkdir -p "$ISABELLE_TMP_PREFIX" || exit $?
wenzelm@57581
    98
OPTIONS_FILE="$ISABELLE_TMP_PREFIX/options$$"
wenzelm@57581
    99
wenzelm@57580
   100
"$ISABELLE_TOOL" java "${JAVA_ARGS[@]}" isabelle.Build_Console \
wenzelm@57581
   101
  "$LOGIC" "$NO_BUILD" "$SYSTEM_MODE" "$OPTIONS_FILE" \
wenzelm@57581
   102
  "${INCLUDE_DIRS[@]}" $'\n' "${SYSTEM_OPTIONS[@]}" || {
wenzelm@57581
   103
  rm -f "$OPTIONS_FILE"
wenzelm@57581
   104
  exit "$?"
wenzelm@57581
   105
}
wenzelm@57581
   106
wenzelm@57581
   107
ISABELLE_OPTIONS["${#ISABELLE_OPTIONS[@]}"]="-O"
wenzelm@57581
   108
ISABELLE_OPTIONS["${#ISABELLE_OPTIONS[@]}"]="$OPTIONS_FILE"
wenzelm@57439
   109
wenzelm@57439
   110
if type -p "$ISABELLE_LINE_EDITOR" > /dev/null
wenzelm@57439
   111
then
wenzelm@57439
   112
  exec "$ISABELLE_LINE_EDITOR" "$ISABELLE_PROCESS" "${ISABELLE_OPTIONS[@]}" -- "$LOGIC"
wenzelm@25632
   113
else
wenzelm@57439
   114
  echo "### No line editor: \"$ISABELLE_LINE_EDITOR\""
wenzelm@52062
   115
  exec "$ISABELLE_PROCESS" "${ISABELLE_OPTIONS[@]}" -- "$LOGIC"
wenzelm@25632
   116
fi