| 67810 |      1 | #!/usr/bin/env bash
 | 
|  |      2 | #
 | 
|  |      3 | # Author: Makarius
 | 
|  |      4 | #
 | 
| 67904 |      5 | # DESCRIPTION: console interaction for Isabelle servers (with line-editor)
 | 
| 67810 |      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 "    -n NAME      explicit server name"
 | 
|  |     16 |   echo "    -p PORT      explicit server port"
 | 
|  |     17 |   echo
 | 
| 67904 |     18 |   echo "  Console interaction for Isabelle servers (with line-editor)."
 | 
| 67810 |     19 |   echo
 | 
|  |     20 |   exit 1
 | 
|  |     21 | }
 | 
|  |     22 | 
 | 
|  |     23 | function fail()
 | 
|  |     24 | {
 | 
|  |     25 |   echo "$1" >&2
 | 
|  |     26 |   exit 2
 | 
|  |     27 | }
 | 
|  |     28 | 
 | 
|  |     29 | 
 | 
|  |     30 | ## process command line
 | 
|  |     31 | 
 | 
|  |     32 | # options
 | 
|  |     33 | 
 | 
| 67876 |     34 | declare -a SERVER_OPTS=(-s -c)
 | 
| 67810 |     35 | 
 | 
|  |     36 | while getopts "n:p:" OPT
 | 
|  |     37 | do
 | 
|  |     38 |   case "$OPT" in
 | 
|  |     39 |     n)
 | 
|  |     40 |       SERVER_OPTS["${#SERVER_OPTS[@]}"]="-n"
 | 
|  |     41 |       SERVER_OPTS["${#SERVER_OPTS[@]}"]="$OPTARG"
 | 
|  |     42 |       ;;
 | 
|  |     43 |     p)
 | 
|  |     44 |       SERVER_OPTS["${#SERVER_OPTS[@]}"]="-p"
 | 
|  |     45 |       SERVER_OPTS["${#SERVER_OPTS[@]}"]="$OPTARG"
 | 
|  |     46 |       ;;
 | 
|  |     47 |     \?)
 | 
|  |     48 |       usage
 | 
|  |     49 |       ;;
 | 
|  |     50 |   esac
 | 
|  |     51 | done
 | 
|  |     52 | 
 | 
|  |     53 | shift $(($OPTIND - 1))
 | 
|  |     54 | 
 | 
|  |     55 | 
 | 
|  |     56 | # args
 | 
|  |     57 | 
 | 
|  |     58 | [ "$#" -ne 0 ] && usage
 | 
|  |     59 | 
 | 
|  |     60 | 
 | 
|  |     61 | # main
 | 
|  |     62 | 
 | 
|  |     63 | if type -p "$ISABELLE_LINE_EDITOR" > /dev/null
 | 
|  |     64 | then
 | 
| 67876 |     65 |   exec "$ISABELLE_LINE_EDITOR" isabelle server "${SERVER_OPTS[@]}"
 | 
| 67810 |     66 | else
 | 
| 71373 |     67 |   echo >&2 "### No line editor: \"$ISABELLE_LINE_EDITOR\""
 | 
| 67876 |     68 |   exec isabelle server "${SERVER_OPTS[@]}"
 | 
| 67810 |     69 | fi
 |