# HG changeset patch
# User wenzelm
# Date 1475420748 -7200
# Node ID 2e4d80723fb01c6eac31b6b48edf45df41895a8a
# Parent  18cbe1b8d85937afb12dcb603bf265984075f0ef
added isabelle_java cold-start executable;

diff -r 18cbe1b8d859 -r 2e4d80723fb0 NEWS
--- 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)
diff -r 18cbe1b8d859 -r 2e4d80723fb0 bin/isabelle_java
--- /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
+}
diff -r 18cbe1b8d859 -r 2e4d80723fb0 lib/Tools/install
--- 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
-
diff -r 18cbe1b8d859 -r 2e4d80723fb0 src/Doc/System/Environment.thy
--- 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>