isabelle: Admin/Linux/Isabelle.run@373dcdd363dc (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	# 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	8
71338 373dcdd363dc updated linux_app-20191223: x86_64-linux; wenzelm parents: 69126 diff changeset	9	ISABELLE_HOME="$(cd "$(dirname "$0")"; cd "$(pwd -P)/../.."; pwd)"
53573 3cffcc303fc0 cold-start of main application even on Linux; wenzelm parents: 53483 diff changeset	10	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	11
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
61134 80ac5e17772d clarified Java runtime options for 32 vs. 64 bit; wenzelm parents: 58792 diff changeset	13	# Java runtime options
80ac5e17772d clarified Java runtime options for 32 vs. 64 bit; wenzelm parents: 58792 diff changeset	14
80ac5e17772d clarified Java runtime options for 32 vs. 64 bit; wenzelm parents: 58792 diff changeset	15	ISABELLE_NAME="$(basename "$0" .run)"
67492 954f44210b92 options file for x86_64 only (amending 03a96b8c7c06); wenzelm parents: 67490 diff changeset	16	declare -a JAVA_OPTIONS=($(perl -p -e 's,#.*$,,g;' "$ISABELLE_HOME/${ISABELLE_NAME}.options"))
61134 80ac5e17772d clarified Java runtime options for 32 vs. 64 bit; wenzelm parents: 58792 diff changeset	17
80ac5e17772d clarified Java runtime options for 32 vs. 64 bit; wenzelm parents: 58792 diff changeset	18
53573 3cffcc303fc0 cold-start of main application even on Linux; wenzelm parents: 53483 diff changeset	19	# 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	20
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	21	#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	22	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	23
67492 954f44210b92 options file for x86_64 only (amending 03a96b8c7c06); wenzelm parents: 67490 diff changeset	24	exec "$ISABELLE_HOME/contrib/jdk/x86_64-linux/jre/bin/java" \
63574 4ea48cbc54c1 uniform server startup like windows and macos, for improved robustness if jEdit is terminated abruptly; wenzelm parents: 62036 diff changeset	25	"-Disabelle.root=$ISABELLE_HOME" "${JAVA_OPTIONS[@]}" \
4ea48cbc54c1 uniform server startup like windows and macos, for improved robustness if jEdit is terminated abruptly; wenzelm parents: 62036 diff changeset	26	-classpath "{CLASSPATH}" \
4ea48cbc54c1 uniform server startup like windows and macos, for improved robustness if jEdit is terminated abruptly; wenzelm parents: 62036 diff changeset	27	"-splash:$ISABELLE_HOME/lib/logo/isabelle.gif" \
4ea48cbc54c1 uniform server startup like windows and macos, for improved robustness if jEdit is terminated abruptly; wenzelm parents: 62036 diff changeset	28	isabelle.Main "$@"

author	wenzelm
	Mon, 23 Dec 2019 15:24:14 +0100
changeset 71338	373dcdd363dc
parent 69126	e1b4b14ded58
permissions	-rw-r--r--