src/Tools/jEdit/lib/Tools/jedit_client
author wenzelm
Mon, 14 Sep 2015 16:06:32 +0200
changeset 61170 dee0aec271b7
child 61294 2d3d26e9b191
permissions -rwxr-xr-x
added isabelle jedit_client;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
61170
dee0aec271b7 added isabelle jedit_client;
wenzelm
parents:
diff changeset
     1
#!/usr/bin/env bash
dee0aec271b7 added isabelle jedit_client;
wenzelm
parents:
diff changeset
     2
#
dee0aec271b7 added isabelle jedit_client;
wenzelm
parents:
diff changeset
     3
# Author: Makarius
dee0aec271b7 added isabelle jedit_client;
wenzelm
parents:
diff changeset
     4
#
dee0aec271b7 added isabelle jedit_client;
wenzelm
parents:
diff changeset
     5
# DESCRIPTION: Isabelle/jEdit client for already running application
dee0aec271b7 added isabelle jedit_client;
wenzelm
parents:
diff changeset
     6
dee0aec271b7 added isabelle jedit_client;
wenzelm
parents:
diff changeset
     7
## settings
dee0aec271b7 added isabelle jedit_client;
wenzelm
parents:
diff changeset
     8
dee0aec271b7 added isabelle jedit_client;
wenzelm
parents:
diff changeset
     9
SERVER_NAME="${ISABELLE_IDENTIFIER:-Isabelle}"
dee0aec271b7 added isabelle jedit_client;
wenzelm
parents:
diff changeset
    10
dee0aec271b7 added isabelle jedit_client;
wenzelm
parents:
diff changeset
    11
case "$ISABELLE_JAVA_PLATFORM" in
dee0aec271b7 added isabelle jedit_client;
wenzelm
parents:
diff changeset
    12
  x86_64-*)
dee0aec271b7 added isabelle jedit_client;
wenzelm
parents:
diff changeset
    13
    JEDIT_JAVA_OPTIONS="$JEDIT_JAVA_OPTIONS64"
dee0aec271b7 added isabelle jedit_client;
wenzelm
parents:
diff changeset
    14
    ;;
dee0aec271b7 added isabelle jedit_client;
wenzelm
parents:
diff changeset
    15
  *)
dee0aec271b7 added isabelle jedit_client;
wenzelm
parents:
diff changeset
    16
    JEDIT_JAVA_OPTIONS="$JEDIT_JAVA_OPTIONS32"
dee0aec271b7 added isabelle jedit_client;
wenzelm
parents:
diff changeset
    17
    ;;
dee0aec271b7 added isabelle jedit_client;
wenzelm
parents:
diff changeset
    18
esac
dee0aec271b7 added isabelle jedit_client;
wenzelm
parents:
diff changeset
    19
dee0aec271b7 added isabelle jedit_client;
wenzelm
parents:
diff changeset
    20
declare -a JAVA_ARGS; eval "JAVA_ARGS=($JEDIT_JAVA_SYSTEM_OPTIONS $JEDIT_JAVA_OPTIONS)"
dee0aec271b7 added isabelle jedit_client;
wenzelm
parents:
diff changeset
    21
dee0aec271b7 added isabelle jedit_client;
wenzelm
parents:
diff changeset
    22
dee0aec271b7 added isabelle jedit_client;
wenzelm
parents:
diff changeset
    23
## diagnostics
dee0aec271b7 added isabelle jedit_client;
wenzelm
parents:
diff changeset
    24
dee0aec271b7 added isabelle jedit_client;
wenzelm
parents:
diff changeset
    25
PRG="$(basename "$0")"
dee0aec271b7 added isabelle jedit_client;
wenzelm
parents:
diff changeset
    26
dee0aec271b7 added isabelle jedit_client;
wenzelm
parents:
diff changeset
    27
function usage()
dee0aec271b7 added isabelle jedit_client;
wenzelm
parents:
diff changeset
    28
{
dee0aec271b7 added isabelle jedit_client;
wenzelm
parents:
diff changeset
    29
  echo
dee0aec271b7 added isabelle jedit_client;
wenzelm
parents:
diff changeset
    30
  echo "Usage: isabelle $PRG [OPTIONS] [FILES ...]"
dee0aec271b7 added isabelle jedit_client;
wenzelm
parents:
diff changeset
    31
  echo
dee0aec271b7 added isabelle jedit_client;
wenzelm
parents:
diff changeset
    32
  echo "  Options are:"
dee0aec271b7 added isabelle jedit_client;
wenzelm
parents:
diff changeset
    33
  echo "    -c           only check presence of server"
dee0aec271b7 added isabelle jedit_client;
wenzelm
parents:
diff changeset
    34
  echo "    -n           only report server name"
dee0aec271b7 added isabelle jedit_client;
wenzelm
parents:
diff changeset
    35
  echo "    -s NAME      server name (default $SERVER_NAME)"
dee0aec271b7 added isabelle jedit_client;
wenzelm
parents:
diff changeset
    36
  echo
dee0aec271b7 added isabelle jedit_client;
wenzelm
parents:
diff changeset
    37
  echo "  Connect to already running Isabelle/jEdit instance and open FILES"
dee0aec271b7 added isabelle jedit_client;
wenzelm
parents:
diff changeset
    38
  echo
dee0aec271b7 added isabelle jedit_client;
wenzelm
parents:
diff changeset
    39
  exit 1
dee0aec271b7 added isabelle jedit_client;
wenzelm
parents:
diff changeset
    40
}
dee0aec271b7 added isabelle jedit_client;
wenzelm
parents:
diff changeset
    41
dee0aec271b7 added isabelle jedit_client;
wenzelm
parents:
diff changeset
    42
function fail()
dee0aec271b7 added isabelle jedit_client;
wenzelm
parents:
diff changeset
    43
{
dee0aec271b7 added isabelle jedit_client;
wenzelm
parents:
diff changeset
    44
  echo "$1" >&2
dee0aec271b7 added isabelle jedit_client;
wenzelm
parents:
diff changeset
    45
  exit 2
dee0aec271b7 added isabelle jedit_client;
wenzelm
parents:
diff changeset
    46
}
dee0aec271b7 added isabelle jedit_client;
wenzelm
parents:
diff changeset
    47
dee0aec271b7 added isabelle jedit_client;
wenzelm
parents:
diff changeset
    48
function failed()
dee0aec271b7 added isabelle jedit_client;
wenzelm
parents:
diff changeset
    49
{
dee0aec271b7 added isabelle jedit_client;
wenzelm
parents:
diff changeset
    50
  fail "Failed!"
dee0aec271b7 added isabelle jedit_client;
wenzelm
parents:
diff changeset
    51
}
dee0aec271b7 added isabelle jedit_client;
wenzelm
parents:
diff changeset
    52
dee0aec271b7 added isabelle jedit_client;
wenzelm
parents:
diff changeset
    53
dee0aec271b7 added isabelle jedit_client;
wenzelm
parents:
diff changeset
    54
## process command line
dee0aec271b7 added isabelle jedit_client;
wenzelm
parents:
diff changeset
    55
dee0aec271b7 added isabelle jedit_client;
wenzelm
parents:
diff changeset
    56
# options
dee0aec271b7 added isabelle jedit_client;
wenzelm
parents:
diff changeset
    57
dee0aec271b7 added isabelle jedit_client;
wenzelm
parents:
diff changeset
    58
CHECK_ONLY="false"
dee0aec271b7 added isabelle jedit_client;
wenzelm
parents:
diff changeset
    59
NAME_ONLY="false"
dee0aec271b7 added isabelle jedit_client;
wenzelm
parents:
diff changeset
    60
dee0aec271b7 added isabelle jedit_client;
wenzelm
parents:
diff changeset
    61
while getopts "cns:" OPT
dee0aec271b7 added isabelle jedit_client;
wenzelm
parents:
diff changeset
    62
do
dee0aec271b7 added isabelle jedit_client;
wenzelm
parents:
diff changeset
    63
  case "$OPT" in
dee0aec271b7 added isabelle jedit_client;
wenzelm
parents:
diff changeset
    64
    c)
dee0aec271b7 added isabelle jedit_client;
wenzelm
parents:
diff changeset
    65
      CHECK_ONLY="true"
dee0aec271b7 added isabelle jedit_client;
wenzelm
parents:
diff changeset
    66
      ;;
dee0aec271b7 added isabelle jedit_client;
wenzelm
parents:
diff changeset
    67
    n)
dee0aec271b7 added isabelle jedit_client;
wenzelm
parents:
diff changeset
    68
      NAME_ONLY="true"
dee0aec271b7 added isabelle jedit_client;
wenzelm
parents:
diff changeset
    69
      ;;
dee0aec271b7 added isabelle jedit_client;
wenzelm
parents:
diff changeset
    70
    s)
dee0aec271b7 added isabelle jedit_client;
wenzelm
parents:
diff changeset
    71
      SERVER_NAME="$OPTARG"
dee0aec271b7 added isabelle jedit_client;
wenzelm
parents:
diff changeset
    72
      ;;
dee0aec271b7 added isabelle jedit_client;
wenzelm
parents:
diff changeset
    73
    \?)
dee0aec271b7 added isabelle jedit_client;
wenzelm
parents:
diff changeset
    74
      usage
dee0aec271b7 added isabelle jedit_client;
wenzelm
parents:
diff changeset
    75
      ;;
dee0aec271b7 added isabelle jedit_client;
wenzelm
parents:
diff changeset
    76
  esac
dee0aec271b7 added isabelle jedit_client;
wenzelm
parents:
diff changeset
    77
done
dee0aec271b7 added isabelle jedit_client;
wenzelm
parents:
diff changeset
    78
dee0aec271b7 added isabelle jedit_client;
wenzelm
parents:
diff changeset
    79
shift $(($OPTIND - 1))
dee0aec271b7 added isabelle jedit_client;
wenzelm
parents:
diff changeset
    80
dee0aec271b7 added isabelle jedit_client;
wenzelm
parents:
diff changeset
    81
dee0aec271b7 added isabelle jedit_client;
wenzelm
parents:
diff changeset
    82
# args
dee0aec271b7 added isabelle jedit_client;
wenzelm
parents:
diff changeset
    83
dee0aec271b7 added isabelle jedit_client;
wenzelm
parents:
diff changeset
    84
declare -a ARGS=()
dee0aec271b7 added isabelle jedit_client;
wenzelm
parents:
diff changeset
    85
dee0aec271b7 added isabelle jedit_client;
wenzelm
parents:
diff changeset
    86
while [ "$#" -gt 0 ]
dee0aec271b7 added isabelle jedit_client;
wenzelm
parents:
diff changeset
    87
do
dee0aec271b7 added isabelle jedit_client;
wenzelm
parents:
diff changeset
    88
  ARGS["${#ARGS[@]}"]="$(jvmpath "$1")"
dee0aec271b7 added isabelle jedit_client;
wenzelm
parents:
diff changeset
    89
  shift
dee0aec271b7 added isabelle jedit_client;
wenzelm
parents:
diff changeset
    90
done
dee0aec271b7 added isabelle jedit_client;
wenzelm
parents:
diff changeset
    91
dee0aec271b7 added isabelle jedit_client;
wenzelm
parents:
diff changeset
    92
dee0aec271b7 added isabelle jedit_client;
wenzelm
parents:
diff changeset
    93
## main
dee0aec271b7 added isabelle jedit_client;
wenzelm
parents:
diff changeset
    94
dee0aec271b7 added isabelle jedit_client;
wenzelm
parents:
diff changeset
    95
if [ "$CHECK_ONLY" = true ]
dee0aec271b7 added isabelle jedit_client;
wenzelm
parents:
diff changeset
    96
then
dee0aec271b7 added isabelle jedit_client;
wenzelm
parents:
diff changeset
    97
  [ -f "$JEDIT_SETTINGS/$SERVER_NAME" ]
dee0aec271b7 added isabelle jedit_client;
wenzelm
parents:
diff changeset
    98
  exit $?
dee0aec271b7 added isabelle jedit_client;
wenzelm
parents:
diff changeset
    99
fi
dee0aec271b7 added isabelle jedit_client;
wenzelm
parents:
diff changeset
   100
dee0aec271b7 added isabelle jedit_client;
wenzelm
parents:
diff changeset
   101
if [ "$NAME_ONLY" = true ]
dee0aec271b7 added isabelle jedit_client;
wenzelm
parents:
diff changeset
   102
then
dee0aec271b7 added isabelle jedit_client;
wenzelm
parents:
diff changeset
   103
  echo "$SERVER_NAME"
dee0aec271b7 added isabelle jedit_client;
wenzelm
parents:
diff changeset
   104
  exit
dee0aec271b7 added isabelle jedit_client;
wenzelm
parents:
diff changeset
   105
fi
dee0aec271b7 added isabelle jedit_client;
wenzelm
parents:
diff changeset
   106
dee0aec271b7 added isabelle jedit_client;
wenzelm
parents:
diff changeset
   107
"$ISABELLE_TOOL" jedit -b || exit $?
dee0aec271b7 added isabelle jedit_client;
wenzelm
parents:
diff changeset
   108
dee0aec271b7 added isabelle jedit_client;
wenzelm
parents:
diff changeset
   109
if [ -f "$JEDIT_SETTINGS/$SERVER_NAME" ]
dee0aec271b7 added isabelle jedit_client;
wenzelm
parents:
diff changeset
   110
then
dee0aec271b7 added isabelle jedit_client;
wenzelm
parents:
diff changeset
   111
  exec "$ISABELLE_TOOL" java "${JAVA_ARGS[@]}" -jar "$JEDIT_HOME/dist/jedit.jar" \
dee0aec271b7 added isabelle jedit_client;
wenzelm
parents:
diff changeset
   112
    "-settings=$(jvmpath "$JEDIT_SETTINGS")" -server="$SERVER_NAME" -reuseview "${ARGS[@]}"
dee0aec271b7 added isabelle jedit_client;
wenzelm
parents:
diff changeset
   113
else
dee0aec271b7 added isabelle jedit_client;
wenzelm
parents:
diff changeset
   114
  fail "Isabelle/jEdit server \"$SERVER_NAME\" not active"
dee0aec271b7 added isabelle jedit_client;
wenzelm
parents:
diff changeset
   115
fi