added isabelle_java cold-start executable;
authorwenzelm
Sun Oct 02 17:05:48 2016 +0200 (2016-10-02)
changeset 639952e4d80723fb0
parent 63994 18cbe1b8d859
child 63996 3f47fec9edfc
added isabelle_java cold-start executable;
NEWS
bin/isabelle_java
lib/Tools/install
src/Doc/System/Environment.thy
     1.1 --- a/NEWS	Sun Oct 02 15:35:56 2016 +0200
     1.2 +++ b/NEWS	Sun Oct 02 17:05:48 2016 +0200
     1.3 @@ -975,6 +975,10 @@
     1.4  multiprocessor systems. The "isabelle jedit" tool allows to override the
     1.5  implicit default via option -p.
     1.6  
     1.7 +* The isabelle_java executable allows to run a Java process within the
     1.8 +name space of Java and Scala components that are bundled with Isabelle,
     1.9 +but without the Isabelle settings environment.
    1.10 +
    1.11  
    1.12  
    1.13  New in Isabelle2016 (February 2016)
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/bin/isabelle_java	Sun Oct 02 17:05:48 2016 +0200
     2.3 @@ -0,0 +1,70 @@
     2.4 +#!/usr/bin/env bash
     2.5 +#
     2.6 +# Author: Makarius
     2.7 +#
     2.8 +# Isabelle/Java cold start -- without settings environment
     2.9 +
    2.10 +if [ -L "$0" ]; then
    2.11 +  TARGET="$(LC_ALL=C ls -l "$0" | sed 's/.* -> //')"
    2.12 +  exec "$(cd "$(dirname "$0")"; cd "$(pwd -P)"; cd "$(dirname "$TARGET")"; pwd)/$(basename "$TARGET")" "$@"
    2.13 +fi
    2.14 +
    2.15 +export ISABELLE_HOME="$(cd "$(dirname "$0")"; cd "$(pwd -P)"; cd ..; pwd)"
    2.16 +
    2.17 +(
    2.18 +  source "$ISABELLE_HOME/lib/scripts/getsettings" || exit 2
    2.19 +
    2.20 +  declare -a JAVA_ARGS; eval "JAVA_ARGS=($ISABELLE_JAVA_SYSTEM_OPTIONS)"
    2.21 +
    2.22 +  if [ -f "$ISABELLE_HOME/src/Tools/jEdit/dist/jedit.jar" ]; then
    2.23 +    classpath "$ISABELLE_HOME/src/Tools/jEdit/dist/jedit.jar"
    2.24 +  fi
    2.25 +
    2.26 +  [ -n "$CLASSPATH" ] && classpath "$CLASSPATH"
    2.27 +
    2.28 +  echo "$ISABELLE_ROOT"
    2.29 +  echo "$CYGWIN_ROOT"
    2.30 +  echo "$JAVA_HOME"
    2.31 +  echo "$(platform_path "$ISABELLE_CLASSPATH")"
    2.32 +  for ARG in "${JAVA_ARGS[@]}"; do echo "$ARG"; done
    2.33 +) | {
    2.34 +  LINE_COUNT=0
    2.35 +  export ISABELLE_ROOT=""
    2.36 +  export CYGWIN_ROOT=""
    2.37 +  unset JAVA_HOME
    2.38 +  unset ISABELLE_CLASSPATH
    2.39 +  unset JAVA_ARGS; declare -a JAVA_ARGS
    2.40 +
    2.41 +  while { unset REPLY; read -r; test "$?" = 0 -o -n "$REPLY"; }
    2.42 +  do
    2.43 +    case "$LINE_COUNT" in
    2.44 +      0)
    2.45 +        LINE_COUNT=1
    2.46 +        ISABELLE_ROOT="$REPLY"
    2.47 +        ;;
    2.48 +      1)
    2.49 +        LINE_COUNT=2
    2.50 +        CYGWIN_ROOT="$REPLY"
    2.51 +        ;;
    2.52 +      2)
    2.53 +        LINE_COUNT=3
    2.54 +        JAVA_HOME="$REPLY"
    2.55 +        ;;
    2.56 +      3)
    2.57 +        LINE_COUNT=4
    2.58 +        ISABELLE_CLASSPATH="$REPLY"
    2.59 +        ;;
    2.60 +      *)
    2.61 +        JAVA_ARGS["${#JAVA_ARGS[@]}"]="$REPLY"
    2.62 +        ;;
    2.63 +    esac
    2.64 +  done
    2.65 +
    2.66 +  if [ -z "$JAVA_HOME" ]; then
    2.67 +    echo "Unknown JAVA_HOME -- Java unavailable" >&2
    2.68 +    exit 127
    2.69 +  else
    2.70 +    unset CLASSPATH
    2.71 +    exec "$JAVA_HOME/bin/java" "${JAVA_ARGS[@]}" -classpath "$ISABELLE_CLASSPATH" "$@"
    2.72 +  fi
    2.73 +}
     3.1 --- a/lib/Tools/install	Sun Oct 02 15:35:56 2016 +0200
     3.2 +++ b/lib/Tools/install	Sun Oct 02 17:05:48 2016 +0200
     3.3 @@ -63,7 +63,7 @@
     3.4  
     3.5  mkdir -p "$BINDIR" || fail "Bad directory: \"$BINDIR\""
     3.6  
     3.7 -for NAME in isabelle isabelle_scala_script
     3.8 +for NAME in isabelle isabelle_java isabelle_scala_script
     3.9  do
    3.10    BIN="$BINDIR/$NAME"
    3.11    DIST="$DISTDIR/bin/$NAME"
    3.12 @@ -74,4 +74,3 @@
    3.13    echo "exec \"$DIST\" \"\$@\"" >> "$BIN"
    3.14    chmod +x "$BIN"
    3.15  done
    3.16 -
     4.1 --- a/src/Doc/System/Environment.thy	Sun Oct 02 15:35:56 2016 +0200
     4.2 +++ b/src/Doc/System/Environment.thy	Sun Oct 02 17:05:48 2016 +0200
     4.3 @@ -399,6 +399,35 @@
     4.4  \<close>
     4.5  
     4.6  
     4.7 +section \<open>The raw Isabelle Java process \label{sec:isabelle-java}\<close>
     4.8 +
     4.9 +text \<open>
    4.10 +  The @{executable_ref isabelle_java} executable allows to run a Java process
    4.11 +  within the name space of Java and Scala components that are bundled with
    4.12 +  Isabelle, but \<^emph>\<open>without\<close> the Isabelle settings environment
    4.13 +  (\secref{sec:settings}).
    4.14 +
    4.15 +  After such a JVM cold-start, the Isabelle environment can be accessed via
    4.16 +  \<^verbatim>\<open>Isabelle_System.getenv\<close> as usual, but the underlying process environment
    4.17 +  remains clean. This is e.g.\ relevant when invoking other processes that
    4.18 +  should remain separate from the current Isabelle installation.
    4.19 +
    4.20 +  \<^medskip>
    4.21 +  Note that under normal circumstances, Isabelle command-line tools are run
    4.22 +  \<^emph>\<open>within\<close> the settings environment, as provided by the @{executable
    4.23 +  isabelle} wrapper (\secref{sec:isabelle-tool} and \secref{sec:tool-java}).
    4.24 +\<close>
    4.25 +
    4.26 +
    4.27 +subsubsection \<open>Example\<close>
    4.28 +
    4.29 +text \<open>
    4.30 +  The subsequent example creates a raw Java process on the command-line and
    4.31 +  invokes the main Isabelle application entry point:
    4.32 +  @{verbatim [display] \<open>isabelle_java isabelle.Main\<close>}
    4.33 +\<close>
    4.34 +
    4.35 +
    4.36  section \<open>YXML versus XML\<close>
    4.37  
    4.38  text \<open>