# HG changeset patch
# User wenzelm
# Date 1520686495 -3600
# Node ID 8ebae6708590782822481acd36e8e2601f824ba2
# Parent  a5fa8d854e5e9614758f89395ca8d865b6c677b9
console interaction with line-editor;

diff -r a5fa8d854e5e -r 8ebae6708590 lib/Tools/client
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/lib/Tools/client	Sat Mar 10 13:54:55 2018 +0100
@@ -0,0 +1,69 @@
+#!/usr/bin/env bash
+#
+# Author: Makarius
+#
+# DESCRIPTION: console interaction for Isabelle server (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 server (with line-editor)."
+  echo
+  exit 1
+}
+
+function fail()
+{
+  echo "$1" >&2
+  exit 2
+}
+
+
+## process command line
+
+# options
+
+declare -a SERVER_OPTS=()
+
+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 -C "${SERVER_OPTS[@]}"
+else
+  echo "### No line editor: \"$ISABELLE_LINE_EDITOR\""
+  exec isabelle server -C "${SERVER_OPTS[@]}"
+fi