--- a/NEWS Sun Oct 02 15:35:56 2016 +0200
+++ b/NEWS Sun Oct 02 17:05:48 2016 +0200
@@ -975,6 +975,10 @@
multiprocessor systems. The "isabelle jedit" tool allows to override the
implicit default via option -p.
+* The isabelle_java executable allows to run a Java process within the
+name space of Java and Scala components that are bundled with Isabelle,
+but without the Isabelle settings environment.
+
New in Isabelle2016 (February 2016)
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/bin/isabelle_java Sun Oct 02 17:05:48 2016 +0200
@@ -0,0 +1,70 @@
+#!/usr/bin/env bash
+#
+# Author: Makarius
+#
+# Isabelle/Java cold start -- without settings environment
+
+if [ -L "$0" ]; then
+ TARGET="$(LC_ALL=C ls -l "$0" | sed 's/.* -> //')"
+ exec "$(cd "$(dirname "$0")"; cd "$(pwd -P)"; cd "$(dirname "$TARGET")"; pwd)/$(basename "$TARGET")" "$@"
+fi
+
+export ISABELLE_HOME="$(cd "$(dirname "$0")"; cd "$(pwd -P)"; cd ..; pwd)"
+
+(
+ source "$ISABELLE_HOME/lib/scripts/getsettings" || exit 2
+
+ declare -a JAVA_ARGS; eval "JAVA_ARGS=($ISABELLE_JAVA_SYSTEM_OPTIONS)"
+
+ if [ -f "$ISABELLE_HOME/src/Tools/jEdit/dist/jedit.jar" ]; then
+ classpath "$ISABELLE_HOME/src/Tools/jEdit/dist/jedit.jar"
+ fi
+
+ [ -n "$CLASSPATH" ] && classpath "$CLASSPATH"
+
+ echo "$ISABELLE_ROOT"
+ echo "$CYGWIN_ROOT"
+ echo "$JAVA_HOME"
+ echo "$(platform_path "$ISABELLE_CLASSPATH")"
+ for ARG in "${JAVA_ARGS[@]}"; do echo "$ARG"; done
+) | {
+ LINE_COUNT=0
+ export ISABELLE_ROOT=""
+ export CYGWIN_ROOT=""
+ unset JAVA_HOME
+ unset ISABELLE_CLASSPATH
+ unset JAVA_ARGS; declare -a JAVA_ARGS
+
+ while { unset REPLY; read -r; test "$?" = 0 -o -n "$REPLY"; }
+ do
+ case "$LINE_COUNT" in
+ 0)
+ LINE_COUNT=1
+ ISABELLE_ROOT="$REPLY"
+ ;;
+ 1)
+ LINE_COUNT=2
+ CYGWIN_ROOT="$REPLY"
+ ;;
+ 2)
+ LINE_COUNT=3
+ JAVA_HOME="$REPLY"
+ ;;
+ 3)
+ LINE_COUNT=4
+ ISABELLE_CLASSPATH="$REPLY"
+ ;;
+ *)
+ JAVA_ARGS["${#JAVA_ARGS[@]}"]="$REPLY"
+ ;;
+ esac
+ done
+
+ if [ -z "$JAVA_HOME" ]; then
+ echo "Unknown JAVA_HOME -- Java unavailable" >&2
+ exit 127
+ else
+ unset CLASSPATH
+ exec "$JAVA_HOME/bin/java" "${JAVA_ARGS[@]}" -classpath "$ISABELLE_CLASSPATH" "$@"
+ fi
+}
--- a/lib/Tools/install Sun Oct 02 15:35:56 2016 +0200
+++ b/lib/Tools/install Sun Oct 02 17:05:48 2016 +0200
@@ -63,7 +63,7 @@
mkdir -p "$BINDIR" || fail "Bad directory: \"$BINDIR\""
-for NAME in isabelle isabelle_scala_script
+for NAME in isabelle isabelle_java isabelle_scala_script
do
BIN="$BINDIR/$NAME"
DIST="$DISTDIR/bin/$NAME"
@@ -74,4 +74,3 @@
echo "exec \"$DIST\" \"\$@\"" >> "$BIN"
chmod +x "$BIN"
done
-
--- a/src/Doc/System/Environment.thy Sun Oct 02 15:35:56 2016 +0200
+++ b/src/Doc/System/Environment.thy Sun Oct 02 17:05:48 2016 +0200
@@ -399,6 +399,35 @@
\<close>
+section \<open>The raw Isabelle Java process \label{sec:isabelle-java}\<close>
+
+text \<open>
+ The @{executable_ref isabelle_java} executable allows to run a Java process
+ within the name space of Java and Scala components that are bundled with
+ Isabelle, but \<^emph>\<open>without\<close> the Isabelle settings environment
+ (\secref{sec:settings}).
+
+ After such a JVM cold-start, the Isabelle environment can be accessed via
+ \<^verbatim>\<open>Isabelle_System.getenv\<close> as usual, but the underlying process environment
+ remains clean. This is e.g.\ relevant when invoking other processes that
+ should remain separate from the current Isabelle installation.
+
+ \<^medskip>
+ Note that under normal circumstances, Isabelle command-line tools are run
+ \<^emph>\<open>within\<close> the settings environment, as provided by the @{executable
+ isabelle} wrapper (\secref{sec:isabelle-tool} and \secref{sec:tool-java}).
+\<close>
+
+
+subsubsection \<open>Example\<close>
+
+text \<open>
+ The subsequent example creates a raw Java process on the command-line and
+ invokes the main Isabelle application entry point:
+ @{verbatim [display] \<open>isabelle_java isabelle.Main\<close>}
+\<close>
+
+
section \<open>YXML versus XML\<close>
text \<open>