src/Tools/jEdit/lib/Tools/jedit_client
author wenzelm
Mon, 30 Jun 2025 20:44:40 +0200
changeset 82800 476627cac12e
parent 73987 fc363a3b690a
permissions -rwxr-xr-x
NEWS;
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
66906
03a96b8c7c06 updated to jdk-8u152, which is for x86_64 only;
wenzelm
parents: 62589
diff changeset
    11
eval "declare -a JAVA_ARGS=($JEDIT_JAVA_SYSTEM_OPTIONS $JEDIT_JAVA_OPTIONS)"
61170
dee0aec271b7 added isabelle jedit_client;
wenzelm
parents:
diff changeset
    12
dee0aec271b7 added isabelle jedit_client;
wenzelm
parents:
diff changeset
    13
dee0aec271b7 added isabelle jedit_client;
wenzelm
parents:
diff changeset
    14
## diagnostics
dee0aec271b7 added isabelle jedit_client;
wenzelm
parents:
diff changeset
    15
dee0aec271b7 added isabelle jedit_client;
wenzelm
parents:
diff changeset
    16
PRG="$(basename "$0")"
dee0aec271b7 added isabelle jedit_client;
wenzelm
parents:
diff changeset
    17
dee0aec271b7 added isabelle jedit_client;
wenzelm
parents:
diff changeset
    18
function usage()
dee0aec271b7 added isabelle jedit_client;
wenzelm
parents:
diff changeset
    19
{
dee0aec271b7 added isabelle jedit_client;
wenzelm
parents:
diff changeset
    20
  echo
dee0aec271b7 added isabelle jedit_client;
wenzelm
parents:
diff changeset
    21
  echo "Usage: isabelle $PRG [OPTIONS] [FILES ...]"
dee0aec271b7 added isabelle jedit_client;
wenzelm
parents:
diff changeset
    22
  echo
dee0aec271b7 added isabelle jedit_client;
wenzelm
parents:
diff changeset
    23
  echo "  Options are:"
dee0aec271b7 added isabelle jedit_client;
wenzelm
parents:
diff changeset
    24
  echo "    -c           only check presence of server"
dee0aec271b7 added isabelle jedit_client;
wenzelm
parents:
diff changeset
    25
  echo "    -n           only report server name"
73128
b15fe413b4d2 tuned message;
wenzelm
parents: 66906
diff changeset
    26
  echo "    -s NAME      server name (default \"$SERVER_NAME\")"
61170
dee0aec271b7 added isabelle jedit_client;
wenzelm
parents:
diff changeset
    27
  echo
dee0aec271b7 added isabelle jedit_client;
wenzelm
parents:
diff changeset
    28
  echo "  Connect to already running Isabelle/jEdit instance and open FILES"
dee0aec271b7 added isabelle jedit_client;
wenzelm
parents:
diff changeset
    29
  echo
dee0aec271b7 added isabelle jedit_client;
wenzelm
parents:
diff changeset
    30
  exit 1
dee0aec271b7 added isabelle jedit_client;
wenzelm
parents:
diff changeset
    31
}
dee0aec271b7 added isabelle jedit_client;
wenzelm
parents:
diff changeset
    32
dee0aec271b7 added isabelle jedit_client;
wenzelm
parents:
diff changeset
    33
function fail()
dee0aec271b7 added isabelle jedit_client;
wenzelm
parents:
diff changeset
    34
{
dee0aec271b7 added isabelle jedit_client;
wenzelm
parents:
diff changeset
    35
  echo "$1" >&2
dee0aec271b7 added isabelle jedit_client;
wenzelm
parents:
diff changeset
    36
  exit 2
dee0aec271b7 added isabelle jedit_client;
wenzelm
parents:
diff changeset
    37
}
dee0aec271b7 added isabelle jedit_client;
wenzelm
parents:
diff changeset
    38
dee0aec271b7 added isabelle jedit_client;
wenzelm
parents:
diff changeset
    39
function failed()
dee0aec271b7 added isabelle jedit_client;
wenzelm
parents:
diff changeset
    40
{
dee0aec271b7 added isabelle jedit_client;
wenzelm
parents:
diff changeset
    41
  fail "Failed!"
dee0aec271b7 added isabelle jedit_client;
wenzelm
parents:
diff changeset
    42
}
dee0aec271b7 added isabelle jedit_client;
wenzelm
parents:
diff changeset
    43
dee0aec271b7 added isabelle jedit_client;
wenzelm
parents:
diff changeset
    44
dee0aec271b7 added isabelle jedit_client;
wenzelm
parents:
diff changeset
    45
## process command line
dee0aec271b7 added isabelle jedit_client;
wenzelm
parents:
diff changeset
    46
dee0aec271b7 added isabelle jedit_client;
wenzelm
parents:
diff changeset
    47
# options
dee0aec271b7 added isabelle jedit_client;
wenzelm
parents:
diff changeset
    48
dee0aec271b7 added isabelle jedit_client;
wenzelm
parents:
diff changeset
    49
CHECK_ONLY="false"
dee0aec271b7 added isabelle jedit_client;
wenzelm
parents:
diff changeset
    50
NAME_ONLY="false"
dee0aec271b7 added isabelle jedit_client;
wenzelm
parents:
diff changeset
    51
dee0aec271b7 added isabelle jedit_client;
wenzelm
parents:
diff changeset
    52
while getopts "cns:" OPT
dee0aec271b7 added isabelle jedit_client;
wenzelm
parents:
diff changeset
    53
do
dee0aec271b7 added isabelle jedit_client;
wenzelm
parents:
diff changeset
    54
  case "$OPT" in
dee0aec271b7 added isabelle jedit_client;
wenzelm
parents:
diff changeset
    55
    c)
dee0aec271b7 added isabelle jedit_client;
wenzelm
parents:
diff changeset
    56
      CHECK_ONLY="true"
dee0aec271b7 added isabelle jedit_client;
wenzelm
parents:
diff changeset
    57
      ;;
dee0aec271b7 added isabelle jedit_client;
wenzelm
parents:
diff changeset
    58
    n)
dee0aec271b7 added isabelle jedit_client;
wenzelm
parents:
diff changeset
    59
      NAME_ONLY="true"
dee0aec271b7 added isabelle jedit_client;
wenzelm
parents:
diff changeset
    60
      ;;
dee0aec271b7 added isabelle jedit_client;
wenzelm
parents:
diff changeset
    61
    s)
dee0aec271b7 added isabelle jedit_client;
wenzelm
parents:
diff changeset
    62
      SERVER_NAME="$OPTARG"
dee0aec271b7 added isabelle jedit_client;
wenzelm
parents:
diff changeset
    63
      ;;
dee0aec271b7 added isabelle jedit_client;
wenzelm
parents:
diff changeset
    64
    \?)
dee0aec271b7 added isabelle jedit_client;
wenzelm
parents:
diff changeset
    65
      usage
dee0aec271b7 added isabelle jedit_client;
wenzelm
parents:
diff changeset
    66
      ;;
dee0aec271b7 added isabelle jedit_client;
wenzelm
parents:
diff changeset
    67
  esac
dee0aec271b7 added isabelle jedit_client;
wenzelm
parents:
diff changeset
    68
done
dee0aec271b7 added isabelle jedit_client;
wenzelm
parents:
diff changeset
    69
dee0aec271b7 added isabelle jedit_client;
wenzelm
parents:
diff changeset
    70
shift $(($OPTIND - 1))
dee0aec271b7 added isabelle jedit_client;
wenzelm
parents:
diff changeset
    71
dee0aec271b7 added isabelle jedit_client;
wenzelm
parents:
diff changeset
    72
dee0aec271b7 added isabelle jedit_client;
wenzelm
parents:
diff changeset
    73
# args
dee0aec271b7 added isabelle jedit_client;
wenzelm
parents:
diff changeset
    74
dee0aec271b7 added isabelle jedit_client;
wenzelm
parents:
diff changeset
    75
declare -a ARGS=()
dee0aec271b7 added isabelle jedit_client;
wenzelm
parents:
diff changeset
    76
dee0aec271b7 added isabelle jedit_client;
wenzelm
parents:
diff changeset
    77
while [ "$#" -gt 0 ]
dee0aec271b7 added isabelle jedit_client;
wenzelm
parents:
diff changeset
    78
do
61294
2d3d26e9b191 renamed jvmpath to platform_path;
wenzelm
parents: 61170
diff changeset
    79
  ARGS["${#ARGS[@]}"]="$(platform_path "$1")"
61170
dee0aec271b7 added isabelle jedit_client;
wenzelm
parents:
diff changeset
    80
  shift
dee0aec271b7 added isabelle jedit_client;
wenzelm
parents:
diff changeset
    81
done
dee0aec271b7 added isabelle jedit_client;
wenzelm
parents:
diff changeset
    82
dee0aec271b7 added isabelle jedit_client;
wenzelm
parents:
diff changeset
    83
dee0aec271b7 added isabelle jedit_client;
wenzelm
parents:
diff changeset
    84
## main
dee0aec271b7 added isabelle jedit_client;
wenzelm
parents:
diff changeset
    85
dee0aec271b7 added isabelle jedit_client;
wenzelm
parents:
diff changeset
    86
if [ "$CHECK_ONLY" = true ]
dee0aec271b7 added isabelle jedit_client;
wenzelm
parents:
diff changeset
    87
then
dee0aec271b7 added isabelle jedit_client;
wenzelm
parents:
diff changeset
    88
  [ -f "$JEDIT_SETTINGS/$SERVER_NAME" ]
dee0aec271b7 added isabelle jedit_client;
wenzelm
parents:
diff changeset
    89
  exit $?
dee0aec271b7 added isabelle jedit_client;
wenzelm
parents:
diff changeset
    90
fi
dee0aec271b7 added isabelle jedit_client;
wenzelm
parents:
diff changeset
    91
dee0aec271b7 added isabelle jedit_client;
wenzelm
parents:
diff changeset
    92
if [ "$NAME_ONLY" = true ]
dee0aec271b7 added isabelle jedit_client;
wenzelm
parents:
diff changeset
    93
then
dee0aec271b7 added isabelle jedit_client;
wenzelm
parents:
diff changeset
    94
  echo "$SERVER_NAME"
dee0aec271b7 added isabelle jedit_client;
wenzelm
parents:
diff changeset
    95
  exit
dee0aec271b7 added isabelle jedit_client;
wenzelm
parents:
diff changeset
    96
fi
dee0aec271b7 added isabelle jedit_client;
wenzelm
parents:
diff changeset
    97
62589
b5783412bfed prefer plain "isabelle" from PATH within Isabelle settings environment;
wenzelm
parents: 62040
diff changeset
    98
isabelle jedit -b || exit $?
61170
dee0aec271b7 added isabelle jedit_client;
wenzelm
parents:
diff changeset
    99
dee0aec271b7 added isabelle jedit_client;
wenzelm
parents:
diff changeset
   100
if [ -f "$JEDIT_SETTINGS/$SERVER_NAME" ]
dee0aec271b7 added isabelle jedit_client;
wenzelm
parents:
diff changeset
   101
then
73987
fc363a3b690a build.props for isabelle.jar, including isabelle.jedit;
wenzelm
parents: 73128
diff changeset
   102
  exec isabelle java "${JAVA_ARGS[@]}" org.gjt.sp.jedit.jEdit \
62040
2d150b6afdeb proper platform_path for Windows;
wenzelm
parents: 61294
diff changeset
   103
    "-settings=$(platform_path "$JEDIT_SETTINGS")" \
2d150b6afdeb proper platform_path for Windows;
wenzelm
parents: 61294
diff changeset
   104
    -server="$SERVER_NAME" -reuseview "${ARGS[@]}"
61170
dee0aec271b7 added isabelle jedit_client;
wenzelm
parents:
diff changeset
   105
else
dee0aec271b7 added isabelle jedit_client;
wenzelm
parents:
diff changeset
   106
  fail "Isabelle/jEdit server \"$SERVER_NAME\" not active"
dee0aec271b7 added isabelle jedit_client;
wenzelm
parents:
diff changeset
   107
fi