lib/Tools/client
author wenzelm
Sat, 10 Mar 2018 13:54:55 +0100
changeset 67810 8ebae6708590
child 67811 33199d033505
permissions -rwxr-xr-x
console interaction with line-editor;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
67810
8ebae6708590 console interaction with line-editor;
wenzelm
parents:
diff changeset
     1
#!/usr/bin/env bash
8ebae6708590 console interaction with line-editor;
wenzelm
parents:
diff changeset
     2
#
8ebae6708590 console interaction with line-editor;
wenzelm
parents:
diff changeset
     3
# Author: Makarius
8ebae6708590 console interaction with line-editor;
wenzelm
parents:
diff changeset
     4
#
8ebae6708590 console interaction with line-editor;
wenzelm
parents:
diff changeset
     5
# DESCRIPTION: console interaction for Isabelle server (with line-editor)
8ebae6708590 console interaction with line-editor;
wenzelm
parents:
diff changeset
     6
8ebae6708590 console interaction with line-editor;
wenzelm
parents:
diff changeset
     7
PRG="$(basename "$0")"
8ebae6708590 console interaction with line-editor;
wenzelm
parents:
diff changeset
     8
8ebae6708590 console interaction with line-editor;
wenzelm
parents:
diff changeset
     9
function usage()
8ebae6708590 console interaction with line-editor;
wenzelm
parents:
diff changeset
    10
{
8ebae6708590 console interaction with line-editor;
wenzelm
parents:
diff changeset
    11
  echo
8ebae6708590 console interaction with line-editor;
wenzelm
parents:
diff changeset
    12
  echo "Usage: isabelle $PRG [OPTIONS]"
8ebae6708590 console interaction with line-editor;
wenzelm
parents:
diff changeset
    13
  echo
8ebae6708590 console interaction with line-editor;
wenzelm
parents:
diff changeset
    14
  echo "  Options are:"
8ebae6708590 console interaction with line-editor;
wenzelm
parents:
diff changeset
    15
  echo "    -n NAME      explicit server name"
8ebae6708590 console interaction with line-editor;
wenzelm
parents:
diff changeset
    16
  echo "    -p PORT      explicit server port"
8ebae6708590 console interaction with line-editor;
wenzelm
parents:
diff changeset
    17
  echo
8ebae6708590 console interaction with line-editor;
wenzelm
parents:
diff changeset
    18
  echo "  Console interaction for Isabelle server (with line-editor)."
8ebae6708590 console interaction with line-editor;
wenzelm
parents:
diff changeset
    19
  echo
8ebae6708590 console interaction with line-editor;
wenzelm
parents:
diff changeset
    20
  exit 1
8ebae6708590 console interaction with line-editor;
wenzelm
parents:
diff changeset
    21
}
8ebae6708590 console interaction with line-editor;
wenzelm
parents:
diff changeset
    22
8ebae6708590 console interaction with line-editor;
wenzelm
parents:
diff changeset
    23
function fail()
8ebae6708590 console interaction with line-editor;
wenzelm
parents:
diff changeset
    24
{
8ebae6708590 console interaction with line-editor;
wenzelm
parents:
diff changeset
    25
  echo "$1" >&2
8ebae6708590 console interaction with line-editor;
wenzelm
parents:
diff changeset
    26
  exit 2
8ebae6708590 console interaction with line-editor;
wenzelm
parents:
diff changeset
    27
}
8ebae6708590 console interaction with line-editor;
wenzelm
parents:
diff changeset
    28
8ebae6708590 console interaction with line-editor;
wenzelm
parents:
diff changeset
    29
8ebae6708590 console interaction with line-editor;
wenzelm
parents:
diff changeset
    30
## process command line
8ebae6708590 console interaction with line-editor;
wenzelm
parents:
diff changeset
    31
8ebae6708590 console interaction with line-editor;
wenzelm
parents:
diff changeset
    32
# options
8ebae6708590 console interaction with line-editor;
wenzelm
parents:
diff changeset
    33
8ebae6708590 console interaction with line-editor;
wenzelm
parents:
diff changeset
    34
declare -a SERVER_OPTS=()
8ebae6708590 console interaction with line-editor;
wenzelm
parents:
diff changeset
    35
8ebae6708590 console interaction with line-editor;
wenzelm
parents:
diff changeset
    36
while getopts "n:p:" OPT
8ebae6708590 console interaction with line-editor;
wenzelm
parents:
diff changeset
    37
do
8ebae6708590 console interaction with line-editor;
wenzelm
parents:
diff changeset
    38
  case "$OPT" in
8ebae6708590 console interaction with line-editor;
wenzelm
parents:
diff changeset
    39
    n)
8ebae6708590 console interaction with line-editor;
wenzelm
parents:
diff changeset
    40
      SERVER_OPTS["${#SERVER_OPTS[@]}"]="-n"
8ebae6708590 console interaction with line-editor;
wenzelm
parents:
diff changeset
    41
      SERVER_OPTS["${#SERVER_OPTS[@]}"]="$OPTARG"
8ebae6708590 console interaction with line-editor;
wenzelm
parents:
diff changeset
    42
      ;;
8ebae6708590 console interaction with line-editor;
wenzelm
parents:
diff changeset
    43
    p)
8ebae6708590 console interaction with line-editor;
wenzelm
parents:
diff changeset
    44
      SERVER_OPTS["${#SERVER_OPTS[@]}"]="-p"
8ebae6708590 console interaction with line-editor;
wenzelm
parents:
diff changeset
    45
      SERVER_OPTS["${#SERVER_OPTS[@]}"]="$OPTARG"
8ebae6708590 console interaction with line-editor;
wenzelm
parents:
diff changeset
    46
      ;;
8ebae6708590 console interaction with line-editor;
wenzelm
parents:
diff changeset
    47
    \?)
8ebae6708590 console interaction with line-editor;
wenzelm
parents:
diff changeset
    48
      usage
8ebae6708590 console interaction with line-editor;
wenzelm
parents:
diff changeset
    49
      ;;
8ebae6708590 console interaction with line-editor;
wenzelm
parents:
diff changeset
    50
  esac
8ebae6708590 console interaction with line-editor;
wenzelm
parents:
diff changeset
    51
done
8ebae6708590 console interaction with line-editor;
wenzelm
parents:
diff changeset
    52
8ebae6708590 console interaction with line-editor;
wenzelm
parents:
diff changeset
    53
shift $(($OPTIND - 1))
8ebae6708590 console interaction with line-editor;
wenzelm
parents:
diff changeset
    54
8ebae6708590 console interaction with line-editor;
wenzelm
parents:
diff changeset
    55
8ebae6708590 console interaction with line-editor;
wenzelm
parents:
diff changeset
    56
# args
8ebae6708590 console interaction with line-editor;
wenzelm
parents:
diff changeset
    57
8ebae6708590 console interaction with line-editor;
wenzelm
parents:
diff changeset
    58
[ "$#" -ne 0 ] && usage
8ebae6708590 console interaction with line-editor;
wenzelm
parents:
diff changeset
    59
8ebae6708590 console interaction with line-editor;
wenzelm
parents:
diff changeset
    60
8ebae6708590 console interaction with line-editor;
wenzelm
parents:
diff changeset
    61
# main
8ebae6708590 console interaction with line-editor;
wenzelm
parents:
diff changeset
    62
8ebae6708590 console interaction with line-editor;
wenzelm
parents:
diff changeset
    63
if type -p "$ISABELLE_LINE_EDITOR" > /dev/null
8ebae6708590 console interaction with line-editor;
wenzelm
parents:
diff changeset
    64
then
8ebae6708590 console interaction with line-editor;
wenzelm
parents:
diff changeset
    65
  exec "$ISABELLE_LINE_EDITOR" isabelle server -C "${SERVER_OPTS[@]}"
8ebae6708590 console interaction with line-editor;
wenzelm
parents:
diff changeset
    66
else
8ebae6708590 console interaction with line-editor;
wenzelm
parents:
diff changeset
    67
  echo "### No line editor: \"$ISABELLE_LINE_EDITOR\""
8ebae6708590 console interaction with line-editor;
wenzelm
parents:
diff changeset
    68
  exec isabelle server -C "${SERVER_OPTS[@]}"
8ebae6708590 console interaction with line-editor;
wenzelm
parents:
diff changeset
    69
fi