lib/Tools/client
author wenzelm
Wed, 31 Mar 2021 11:24:46 +0200
changeset 73772 d3f2038198ae
parent 71582 201486ced92d
permissions -rwxr-xr-x
clarified (again): local tip could be actually more recent;
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
#
67904
465f43a9f780 documentation for the Isabelle server;
wenzelm
parents: 67876
diff changeset
     5
# DESCRIPTION: console interaction for Isabelle servers (with line-editor)
67810
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
67904
465f43a9f780 documentation for the Isabelle server;
wenzelm
parents: 67876
diff changeset
    18
  echo "  Console interaction for Isabelle servers (with line-editor)."
67810
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
67876
cc4832285c38 proper options;
wenzelm
parents: 67811
diff changeset
    34
declare -a SERVER_OPTS=(-s -c)
67810
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
67876
cc4832285c38 proper options;
wenzelm
parents: 67811
diff changeset
    65
  exec "$ISABELLE_LINE_EDITOR" isabelle server "${SERVER_OPTS[@]}"
67810
8ebae6708590 console interaction with line-editor;
wenzelm
parents:
diff changeset
    66
else
71582
201486ced92d clarified output channel;
wenzelm
parents: 67904
diff changeset
    67
  echo >&2 "### No line editor: \"$ISABELLE_LINE_EDITOR\""
67876
cc4832285c38 proper options;
wenzelm
parents: 67811
diff changeset
    68
  exec isabelle server "${SERVER_OPTS[@]}"
67810
8ebae6708590 console interaction with line-editor;
wenzelm
parents:
diff changeset
    69
fi