# HG changeset patch # User wenzelm # Date 1442239592 -7200 # Node ID dee0aec271b7bfbcad205a3c95ea30446210eaea # Parent 4de9ff3ea29a607b80101439885c5fd556fda6b2 added isabelle jedit_client; diff -r 4de9ff3ea29a -r dee0aec271b7 NEWS --- a/NEWS Sun Sep 13 22:56:52 2015 +0200 +++ b/NEWS Mon Sep 14 16:06:32 2015 +0200 @@ -21,6 +21,10 @@ At least one Debugger view needs to be active to have any effect on the running ML program. +* Command-line tool "isabelle jedit_client" allows to connect to already +running Isabelle/jEdit process. This achieves the effect of +single-instance applications seen on common GUI desktops. + *** Isar *** diff -r 4de9ff3ea29a -r dee0aec271b7 src/Tools/jEdit/lib/Tools/jedit_client --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Tools/jEdit/lib/Tools/jedit_client Mon Sep 14 16:06:32 2015 +0200 @@ -0,0 +1,115 @@ +#!/usr/bin/env bash +# +# Author: Makarius +# +# DESCRIPTION: Isabelle/jEdit client for already running application + +## settings + +SERVER_NAME="${ISABELLE_IDENTIFIER:-Isabelle}" + +case "$ISABELLE_JAVA_PLATFORM" in + x86_64-*) + JEDIT_JAVA_OPTIONS="$JEDIT_JAVA_OPTIONS64" + ;; + *) + JEDIT_JAVA_OPTIONS="$JEDIT_JAVA_OPTIONS32" + ;; +esac + +declare -a JAVA_ARGS; eval "JAVA_ARGS=($JEDIT_JAVA_SYSTEM_OPTIONS $JEDIT_JAVA_OPTIONS)" + + +## diagnostics + +PRG="$(basename "$0")" + +function usage() +{ + echo + echo "Usage: isabelle $PRG [OPTIONS] [FILES ...]" + echo + echo " Options are:" + echo " -c only check presence of server" + echo " -n only report server name" + echo " -s NAME server name (default $SERVER_NAME)" + echo + echo " Connect to already running Isabelle/jEdit instance and open FILES" + echo + exit 1 +} + +function fail() +{ + echo "$1" >&2 + exit 2 +} + +function failed() +{ + fail "Failed!" +} + + +## process command line + +# options + +CHECK_ONLY="false" +NAME_ONLY="false" + +while getopts "cns:" OPT +do + case "$OPT" in + c) + CHECK_ONLY="true" + ;; + n) + NAME_ONLY="true" + ;; + s) + SERVER_NAME="$OPTARG" + ;; + \?) + usage + ;; + esac +done + +shift $(($OPTIND - 1)) + + +# args + +declare -a ARGS=() + +while [ "$#" -gt 0 ] +do + ARGS["${#ARGS[@]}"]="$(jvmpath "$1")" + shift +done + + +## main + +if [ "$CHECK_ONLY" = true ] +then + [ -f "$JEDIT_SETTINGS/$SERVER_NAME" ] + exit $? +fi + +if [ "$NAME_ONLY" = true ] +then + echo "$SERVER_NAME" + exit +fi + +"$ISABELLE_TOOL" jedit -b || exit $? + +if [ -f "$JEDIT_SETTINGS/$SERVER_NAME" ] +then + exec "$ISABELLE_TOOL" java "${JAVA_ARGS[@]}" -jar "$JEDIT_HOME/dist/jedit.jar" \ + "-settings=$(jvmpath "$JEDIT_SETTINGS")" -server="$SERVER_NAME" -reuseview "${ARGS[@]}" +else + fail "Isabelle/jEdit server \"$SERVER_NAME\" not active" +fi