isabelle: Admin/Linux/Isabelle.run@49b964a6fe11 (annotated)

53483 74a4685a96c8 generate application based on $JEDIT_JAVA_OPTIONS $JEDIT_SYSTEM_OPTIONS at build time (see also src/Tools/jEdit/lib/Tools/jedit); wenzelm parents: diff changeset	1	#!/usr/bin/env bash
74a4685a96c8 generate application based on $JEDIT_JAVA_OPTIONS $JEDIT_SYSTEM_OPTIONS at build time (see also src/Tools/jEdit/lib/Tools/jedit); wenzelm parents: diff changeset	2	#
74a4685a96c8 generate application based on $JEDIT_JAVA_OPTIONS $JEDIT_SYSTEM_OPTIONS at build time (see also src/Tools/jEdit/lib/Tools/jedit); wenzelm parents: diff changeset	3	# Author: Makarius
74a4685a96c8 generate application based on $JEDIT_JAVA_OPTIONS $JEDIT_SYSTEM_OPTIONS at build time (see also src/Tools/jEdit/lib/Tools/jedit); wenzelm parents: diff changeset	4	#
54313 da2e6282a4f5 native executable even for Linux, to avoid surprises with file managers opening executable script as text file; wenzelm parents: 54037 diff changeset	5	# Main Isabelle application script.
53483 74a4685a96c8 generate application based on $JEDIT_JAVA_OPTIONS $JEDIT_SYSTEM_OPTIONS at build time (see also src/Tools/jEdit/lib/Tools/jedit); wenzelm parents: diff changeset	6
53573 3cffcc303fc0 cold-start of main application even on Linux; wenzelm parents: 53483 diff changeset	7	# dereference executable
53483 74a4685a96c8 generate application based on $JEDIT_JAVA_OPTIONS $JEDIT_SYSTEM_OPTIONS at build time (see also src/Tools/jEdit/lib/Tools/jedit); wenzelm parents: diff changeset	8	if [ -L "$0" ]; then
74a4685a96c8 generate application based on $JEDIT_JAVA_OPTIONS $JEDIT_SYSTEM_OPTIONS at build time (see also src/Tools/jEdit/lib/Tools/jedit); wenzelm parents: diff changeset	9	TARGET="$(LC_ALL=C ls -l "$0" \| sed 's/.* -> //')"
74a4685a96c8 generate application based on $JEDIT_JAVA_OPTIONS $JEDIT_SYSTEM_OPTIONS at build time (see also src/Tools/jEdit/lib/Tools/jedit); wenzelm parents: diff changeset	10	exec "$(cd "$(dirname "$0")"; cd "$(pwd -P)"; cd "$(dirname "$TARGET")"; pwd)/$(basename "$TARGET")" "$@"
74a4685a96c8 generate application based on $JEDIT_JAVA_OPTIONS $JEDIT_SYSTEM_OPTIONS at build time (see also src/Tools/jEdit/lib/Tools/jedit); wenzelm parents: diff changeset	11	fi
74a4685a96c8 generate application based on $JEDIT_JAVA_OPTIONS $JEDIT_SYSTEM_OPTIONS at build time (see also src/Tools/jEdit/lib/Tools/jedit); wenzelm parents: diff changeset	12
74a4685a96c8 generate application based on $JEDIT_JAVA_OPTIONS $JEDIT_SYSTEM_OPTIONS at build time (see also src/Tools/jEdit/lib/Tools/jedit); wenzelm parents: diff changeset	13
53573 3cffcc303fc0 cold-start of main application even on Linux; wenzelm parents: 53483 diff changeset	14	# minimal Isabelle environment
53483 74a4685a96c8 generate application based on $JEDIT_JAVA_OPTIONS $JEDIT_SYSTEM_OPTIONS at build time (see also src/Tools/jEdit/lib/Tools/jedit); wenzelm parents: diff changeset	15
74a4685a96c8 generate application based on $JEDIT_JAVA_OPTIONS $JEDIT_SYSTEM_OPTIONS at build time (see also src/Tools/jEdit/lib/Tools/jedit); wenzelm parents: diff changeset	16	ISABELLE_HOME="$(cd "$(dirname "$0")"; cd "$(pwd -P)"; pwd)"
53573 3cffcc303fc0 cold-start of main application even on Linux; wenzelm parents: 53483 diff changeset	17	source "$ISABELLE_HOME/lib/scripts/isabelle-platform"
53483 74a4685a96c8 generate application based on $JEDIT_JAVA_OPTIONS $JEDIT_SYSTEM_OPTIONS at build time (see also src/Tools/jEdit/lib/Tools/jedit); wenzelm parents: diff changeset	18
74a4685a96c8 generate application based on $JEDIT_JAVA_OPTIONS $JEDIT_SYSTEM_OPTIONS at build time (see also src/Tools/jEdit/lib/Tools/jedit); wenzelm parents: diff changeset	19
61134 80ac5e17772d clarified Java runtime options for 32 vs. 64 bit; wenzelm parents: 58792 diff changeset	20	# Java runtime options
80ac5e17772d clarified Java runtime options for 32 vs. 64 bit; wenzelm parents: 58792 diff changeset	21
80ac5e17772d clarified Java runtime options for 32 vs. 64 bit; wenzelm parents: 58792 diff changeset	22	ISABELLE_NAME="$(basename "$0" .run)"
80ac5e17772d clarified Java runtime options for 32 vs. 64 bit; wenzelm parents: 58792 diff changeset	23	if [ -z "$ISABELLE_PLATFORM64" ]; then
80ac5e17772d clarified Java runtime options for 32 vs. 64 bit; wenzelm parents: 58792 diff changeset	24	declare -a JAVA_OPTIONS=($(perl -p -e 's,#.*$,,g;' "$ISABELLE_HOME/${ISABELLE_NAME}.options32"))
80ac5e17772d clarified Java runtime options for 32 vs. 64 bit; wenzelm parents: 58792 diff changeset	25	else
80ac5e17772d clarified Java runtime options for 32 vs. 64 bit; wenzelm parents: 58792 diff changeset	26	declare -a JAVA_OPTIONS=($(perl -p -e 's,#.*$,,g;' "$ISABELLE_HOME/${ISABELLE_NAME}.options64"))
80ac5e17772d clarified Java runtime options for 32 vs. 64 bit; wenzelm parents: 58792 diff changeset	27	fi
80ac5e17772d clarified Java runtime options for 32 vs. 64 bit; wenzelm parents: 58792 diff changeset	28
80ac5e17772d clarified Java runtime options for 32 vs. 64 bit; wenzelm parents: 58792 diff changeset	29
53573 3cffcc303fc0 cold-start of main application even on Linux; wenzelm parents: 53483 diff changeset	30	# main
53483 74a4685a96c8 generate application based on $JEDIT_JAVA_OPTIONS $JEDIT_SYSTEM_OPTIONS at build time (see also src/Tools/jEdit/lib/Tools/jedit); wenzelm parents: diff changeset	31
54037 ab77ec347220 unset XMODIFIERS by default, in order to prevent total loss of key events seen on Fedora 18/19; wenzelm parents: 53581 diff changeset	32	#paranoia setting -- avoid problems of Java/Swing versus XIM/IBus etc.
ab77ec347220 unset XMODIFIERS by default, in order to prevent total loss of key events seen on Fedora 18/19; wenzelm parents: 53581 diff changeset	33	unset XMODIFIERS
ab77ec347220 unset XMODIFIERS by default, in order to prevent total loss of key events seen on Fedora 18/19; wenzelm parents: 53581 diff changeset	34
61172 0a1b62bbbdf9 single-instance application for Linux; wenzelm parents: 61134 diff changeset	35	if "$ISABELLE_HOME/bin/isabelle" jedit_client -c
0a1b62bbbdf9 single-instance application for Linux; wenzelm parents: 61134 diff changeset	36	then
0a1b62bbbdf9 single-instance application for Linux; wenzelm parents: 61134 diff changeset	37	"$ISABELLE_HOME/bin/isabelle" jedit_client "$@"
0a1b62bbbdf9 single-instance application for Linux; wenzelm parents: 61134 diff changeset	38	else
0a1b62bbbdf9 single-instance application for Linux; wenzelm parents: 61134 diff changeset	39	exec "$ISABELLE_HOME/contrib/jdk/${ISABELLE_PLATFORM64:-$ISABELLE_PLATFORM32}/jre/bin/java" \
61298 49b964a6fe11 proper isabelle.root for bootstrap; wenzelm parents: 61172 diff changeset	40	"-Disabelle.root=$ISABELLE_HOME" "${JAVA_OPTIONS[@]}" \
61172 0a1b62bbbdf9 single-instance application for Linux; wenzelm parents: 61134 diff changeset	41	-classpath "{CLASSPATH}" \
0a1b62bbbdf9 single-instance application for Linux; wenzelm parents: 61134 diff changeset	42	"-splash:$ISABELLE_HOME/lib/logo/isabelle.gif" \
0a1b62bbbdf9 single-instance application for Linux; wenzelm parents: 61134 diff changeset	43	isabelle.Main -server="$("$ISABELLE_HOME/bin/isabelle" jedit_client -n)" "$@"
0a1b62bbbdf9 single-instance application for Linux; wenzelm parents: 61134 diff changeset	44	fi

author	wenzelm
	Wed, 30 Sep 2015 23:37:20 +0200
changeset 61298	49b964a6fe11
parent 61172	0a1b62bbbdf9
child 62036	773cb226738c
permissions	-rw-r--r--