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