lib/Tools/client

clarified messages, depending on option "document_echo";

#!/usr/bin/env bash
#
# Author: Makarius
#
# DESCRIPTION: console interaction for Isabelle servers (with line-editor)

PRG="$(basename "$0")"

function usage()
{
  echo
  echo "Usage: isabelle $PRG [OPTIONS]"
  echo
  echo "  Options are:"
  echo "    -n NAME      explicit server name"
  echo "    -p PORT      explicit server port"
  echo
  echo "  Console interaction for Isabelle servers (with line-editor)."
  echo
  exit 1
}

function fail()
{
  echo "$1" >&2
  exit 2
}


## process command line

# options

declare -a SERVER_OPTS=(-s -c)

while getopts "n:p:" OPT
do
  case "$OPT" in
    n)
      SERVER_OPTS["${#SERVER_OPTS[@]}"]="-n"
      SERVER_OPTS["${#SERVER_OPTS[@]}"]="$OPTARG"
      ;;
    p)
      SERVER_OPTS["${#SERVER_OPTS[@]}"]="-p"
      SERVER_OPTS["${#SERVER_OPTS[@]}"]="$OPTARG"
      ;;
    \?)
      usage
      ;;
  esac
done

shift $(($OPTIND - 1))


# args

[ "$#" -ne 0 ] && usage


# main

if type -p "$ISABELLE_LINE_EDITOR" > /dev/null
then
  exec "$ISABELLE_LINE_EDITOR" isabelle server "${SERVER_OPTS[@]}"
else
  echo >&2 "### No line editor: \"$ISABELLE_LINE_EDITOR\""
  exec isabelle server "${SERVER_OPTS[@]}"
fi