lib/Tools/java
author wenzelm
Wed, 22 Dec 2010 11:52:57 +0100
changeset 41380 92237dee0f29
parent 36238 344377ce2e0a
child 41622 ad5474a8374b
permissions -rwxr-xr-x
isabelle java: prefer -server here;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
27914
9a7f17370ffb refined scala/java wrappers via isatool;
wenzelm
parents:
diff changeset
     1
#!/usr/bin/env bash
9a7f17370ffb refined scala/java wrappers via isatool;
wenzelm
parents:
diff changeset
     2
#
9a7f17370ffb refined scala/java wrappers via isatool;
wenzelm
parents:
diff changeset
     3
# Author: Makarius
9a7f17370ffb refined scala/java wrappers via isatool;
wenzelm
parents:
diff changeset
     4
#
27916
09b3010ffaf2 removed unused usage;
wenzelm
parents: 27914
diff changeset
     5
# DESCRIPTION: invoke Java within the Isabelle environment
27914
9a7f17370ffb refined scala/java wrappers via isatool;
wenzelm
parents:
diff changeset
     6
9a7f17370ffb refined scala/java wrappers via isatool;
wenzelm
parents:
diff changeset
     7
CLASSPATH="$(jvmpath "$CLASSPATH")"
41380
92237dee0f29 isabelle java: prefer -server here;
wenzelm
parents: 36238
diff changeset
     8
92237dee0f29 isabelle java: prefer -server here;
wenzelm
parents: 36238
diff changeset
     9
JAVA_EXE="${THIS_JAVA:-$ISABELLE_JAVA}"
92237dee0f29 isabelle java: prefer -server here;
wenzelm
parents: 36238
diff changeset
    10
if "$JAVA_EXE" -server >/dev/null 2>/dev/null
92237dee0f29 isabelle java: prefer -server here;
wenzelm
parents: 36238
diff changeset
    11
then
92237dee0f29 isabelle java: prefer -server here;
wenzelm
parents: 36238
diff changeset
    12
  exec "$JAVA_EXE" -server "$@"
92237dee0f29 isabelle java: prefer -server here;
wenzelm
parents: 36238
diff changeset
    13
else
92237dee0f29 isabelle java: prefer -server here;
wenzelm
parents: 36238
diff changeset
    14
  exec "$JAVA_EXE" "$@"
92237dee0f29 isabelle java: prefer -server here;
wenzelm
parents: 36238
diff changeset
    15
fi
92237dee0f29 isabelle java: prefer -server here;
wenzelm
parents: 36238
diff changeset
    16