lib/Tools/console
author blanchet
Thu Sep 04 11:20:59 2014 +0200 (2014-09-04)
changeset 58182 82478e6c60cb
parent 57686 5b16e2370ccb
child 61135 8f7d802b7a71
permissions -rwxr-xr-x
tweaked setup for datatype realizer
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@25632
     7
PRG="$(basename "$0")"
wenzelm@25632
     8
wenzelm@25632
     9
function usage()
wenzelm@25632
    10
{
wenzelm@25632
    11
  echo
wenzelm@28650
    12
  echo "Usage: isabelle $PRG [OPTIONS]"
wenzelm@25632
    13
  echo
wenzelm@25632
    14
  echo "  Options are:"
wenzelm@57439
    15
  echo "    -d DIR       include session directory"
wenzelm@57439
    16
  echo "    -l NAME      logic session name (default ISABELLE_LOGIC=\"$ISABELLE_LOGIC\")"
wenzelm@25632
    17
  echo "    -m MODE      add print mode for output"
wenzelm@57439
    18
  echo "    -n           no build of session image on startup"
wenzelm@52062
    19
  echo "    -o OPTION    override Isabelle system OPTION (via NAME=VAL or NAME)"
wenzelm@57439
    20
  echo "    -s           system build mode for session image"
wenzelm@25632
    21
  echo
wenzelm@57439
    22
  echo "  Run Isabelle process with raw ML console and line editor"
wenzelm@57439
    23
  echo "  (ISABELLE_LINE_EDITOR=\"$ISABELLE_LINE_EDITOR\")."
wenzelm@25632
    24
  echo
wenzelm@25632
    25
  exit 1
wenzelm@25632
    26
}
wenzelm@25632
    27
wenzelm@25632
    28
wenzelm@25632
    29
## process command line
wenzelm@25632
    30
wenzelm@25632
    31
# options
wenzelm@25632
    32
wenzelm@57439
    33
declare -a ISABELLE_OPTIONS=()
wenzelm@57580
    34
wenzelm@57580
    35
declare -a INCLUDE_DIRS=()
wenzelm@57580
    36
LOGIC="$ISABELLE_LOGIC"
wenzelm@57580
    37
NO_BUILD="false"
wenzelm@57581
    38
declare -a SYSTEM_OPTIONS=()
wenzelm@57580
    39
SYSTEM_MODE="false"
wenzelm@25632
    40
wenzelm@57439
    41
while getopts "d:l:m:no:s" OPT
wenzelm@25632
    42
do
wenzelm@25632
    43
  case "$OPT" in
wenzelm@57439
    44
    d)
wenzelm@57580
    45
      INCLUDE_DIRS["${#INCLUDE_DIRS[@]}"]="$OPTARG"
wenzelm@57439
    46
      ;;
wenzelm@25632
    47
    l)
wenzelm@25632
    48
      LOGIC="$OPTARG"
wenzelm@25632
    49
      ;;
wenzelm@25632
    50
    m)
wenzelm@52062
    51
      ISABELLE_OPTIONS["${#ISABELLE_OPTIONS[@]}"]="-m"
wenzelm@52062
    52
      ISABELLE_OPTIONS["${#ISABELLE_OPTIONS[@]}"]="$OPTARG"
wenzelm@52062
    53
      ;;
wenzelm@57439
    54
    n)
wenzelm@57580
    55
      NO_BUILD="true"
wenzelm@57439
    56
      ;;
wenzelm@52062
    57
    o)
wenzelm@57581
    58
      SYSTEM_OPTIONS["${#SYSTEM_OPTIONS[@]}"]="$OPTARG"
wenzelm@25632
    59
      ;;
wenzelm@57439
    60
    s)
wenzelm@57580
    61
      SYSTEM_MODE="true"
wenzelm@25632
    62
      ;;
wenzelm@25632
    63
    \?)
wenzelm@25632
    64
      usage
wenzelm@25632
    65
      ;;
wenzelm@25632
    66
  esac
wenzelm@25632
    67
done
wenzelm@25632
    68
wenzelm@25632
    69
shift $(($OPTIND - 1))
wenzelm@25632
    70
wenzelm@25632
    71
wenzelm@25632
    72
# args
wenzelm@25632
    73
wenzelm@25632
    74
[ "$#" -ne 0 ] && { echo "Bad args: $*"; usage; }
wenzelm@25632
    75
wenzelm@25632
    76
wenzelm@25632
    77
## main
wenzelm@25632
    78
wenzelm@57580
    79
isabelle_admin_build jars || exit $?
wenzelm@57580
    80
wenzelm@57580
    81
declare -a JAVA_ARGS; eval "JAVA_ARGS=($ISABELLE_BUILD_JAVA_OPTIONS)"
wenzelm@57580
    82
wenzelm@57686
    83
mkdir -p "$ISABELLE_TMP_PREFIX" || exit $?
wenzelm@57581
    84
OPTIONS_FILE="$ISABELLE_TMP_PREFIX/options$$"
wenzelm@57581
    85
wenzelm@57580
    86
"$ISABELLE_TOOL" java "${JAVA_ARGS[@]}" isabelle.Build_Console \
wenzelm@57581
    87
  "$LOGIC" "$NO_BUILD" "$SYSTEM_MODE" "$OPTIONS_FILE" \
wenzelm@57581
    88
  "${INCLUDE_DIRS[@]}" $'\n' "${SYSTEM_OPTIONS[@]}" || {
wenzelm@57581
    89
  rm -f "$OPTIONS_FILE"
wenzelm@57581
    90
  exit "$?"
wenzelm@57581
    91
}
wenzelm@57581
    92
wenzelm@57581
    93
ISABELLE_OPTIONS["${#ISABELLE_OPTIONS[@]}"]="-O"
wenzelm@57581
    94
ISABELLE_OPTIONS["${#ISABELLE_OPTIONS[@]}"]="$OPTIONS_FILE"
wenzelm@57439
    95
wenzelm@57439
    96
if type -p "$ISABELLE_LINE_EDITOR" > /dev/null
wenzelm@57439
    97
then
wenzelm@57439
    98
  exec "$ISABELLE_LINE_EDITOR" "$ISABELLE_PROCESS" "${ISABELLE_OPTIONS[@]}" -- "$LOGIC"
wenzelm@25632
    99
else
wenzelm@57439
   100
  echo "### No line editor: \"$ISABELLE_LINE_EDITOR\""
wenzelm@52062
   101
  exec "$ISABELLE_PROCESS" "${ISABELLE_OPTIONS[@]}" -- "$LOGIC"
wenzelm@25632
   102
fi