lib/Tools/tty
author wenzelm
Thu Apr 24 00:29:55 2014 +0200 (2014-04-24)
changeset 56686 2386d1a3ca8f
parent 52062 4f91262e7f33
permissions -rwxr-xr-x
canonical list operations, as in ML;
avoid odd mutable data structures;
     1 #!/usr/bin/env bash
     2 #
     3 # Author: Markus Wenzel, TU Muenchen
     4 #
     5 # DESCRIPTION: run Isabelle process with plain tty interaction
     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 "    -l NAME      logic image name (default ISABELLE_LOGIC=\"$ISABELLE_LOGIC\")"
    16   echo "    -m MODE      add print mode for output"
    17   echo "    -o OPTION    override Isabelle system OPTION (via NAME=VAL or NAME)"
    18   echo "    -p NAME      line editor program name"
    19   echo "                 (default ISABELLE_LINE_EDITOR=\"$ISABELLE_LINE_EDITOR\")"
    20   echo
    21   echo "  Run Isabelle process with plain tty interaction and line editor."
    22   echo
    23   exit 1
    24 }
    25 
    26 function fail()
    27 {
    28   echo "$1" >&2
    29   exit 2
    30 }
    31 
    32 
    33 ## process command line
    34 
    35 # options
    36 
    37 declare -a ISABELLE_OPTIONS=("-I")
    38 
    39 LOGIC=""
    40 LINE_EDITOR="$ISABELLE_LINE_EDITOR"
    41 
    42 while getopts "l:m:p:o:" OPT
    43 do
    44   case "$OPT" in
    45     l)
    46       LOGIC="$OPTARG"
    47       ;;
    48     m)
    49       ISABELLE_OPTIONS["${#ISABELLE_OPTIONS[@]}"]="-m"
    50       ISABELLE_OPTIONS["${#ISABELLE_OPTIONS[@]}"]="$OPTARG"
    51       ;;
    52     o)
    53       ISABELLE_OPTIONS["${#ISABELLE_OPTIONS[@]}"]="-o"
    54       ISABELLE_OPTIONS["${#ISABELLE_OPTIONS[@]}"]="$OPTARG"
    55       ;;
    56     p)
    57       LINE_EDITOR="$OPTARG"
    58       ;;
    59     \?)
    60       usage
    61       ;;
    62   esac
    63 done
    64 
    65 shift $(($OPTIND - 1))
    66 
    67 
    68 # args
    69 
    70 [ "$#" -ne 0 ] && { echo "Bad args: $*"; usage; }
    71 
    72 
    73 ## main
    74 
    75 if [ -n "$LINE_EDITOR" ]; then
    76   exec "$LINE_EDITOR" "$ISABELLE_PROCESS" "${ISABELLE_OPTIONS[@]}" -- "$LOGIC"
    77 else
    78   exec "$ISABELLE_PROCESS" "${ISABELLE_OPTIONS[@]}" -- "$LOGIC"
    79 fi