--- a/NEWS Thu Feb 25 16:53:34 2016 +0000
+++ b/NEWS Thu Feb 25 20:23:32 2016 +0100
@@ -156,6 +156,10 @@
*** System ***
+* The Isabelle system environment always ensures that the main
+executables are found within the PATH: isabelle, isabelle_process,
+isabelle_scala_script.
+
* SML/NJ is no longer supported.
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/lib/scripts/getfunctions Thu Feb 25 20:23:32 2016 +0100
@@ -0,0 +1,206 @@
+# -*- shell-script -*- :mode=shellscript:
+#
+# Author: Makarius
+#
+# Isabelle shell functions, with on-demand re-initialization for
+# non-interactive bash processess. NB: bash shell functions are not portable
+# and may be dropped by aggressively POSIX-conformant versions of /bin/sh.
+
+if type splitarray >/dev/null 2>/dev/null
+then
+ :
+else
+
+if [ "$OSTYPE" = cygwin ]; then
+ function platform_path() { cygpath -i -C UTF8 -w -p "$@"; }
+else
+ function platform_path() { echo "$@"; }
+fi
+export -f platform_path
+
+#GNU tar (notably on Mac OS X)
+if [ -x /usr/bin/gnutar ]; then
+ function tar() { /usr/bin/gnutar "$@"; }
+ export -f tar
+fi
+
+#shared library convenience
+function librarypath ()
+{
+ for X in "$@"
+ do
+ case "$ISABELLE_PLATFORM" in
+ *-darwin)
+ if [ -z "$DYLD_LIBRARY_PATH" ]; then
+ DYLD_LIBRARY_PATH="$X"
+ else
+ DYLD_LIBRARY_PATH="$X:$DYLD_LIBRARY_PATH"
+ fi
+ export DYLD_LIBRARY_PATH
+ ;;
+ *)
+ if [ -z "$LD_LIBRARY_PATH" ]; then
+ LD_LIBRARY_PATH="$X"
+ else
+ LD_LIBRARY_PATH="$X:$LD_LIBRARY_PATH"
+ fi
+ export LD_LIBRARY_PATH
+ ;;
+ esac
+ done
+}
+export -f librarypath
+
+#robust invocation via ISABELLE_JDK_HOME
+function isabelle_jdk ()
+{
+ if [ -z "$ISABELLE_JDK_HOME" ]; then
+ echo "Unknown ISABELLE_JDK_HOME -- Java development tools unavailable" >&2
+ return 127
+ else
+ local PRG="$1"; shift
+ "$ISABELLE_JDK_HOME/bin/$PRG" "$@"
+ fi
+}
+export -f isabelle_jdk
+
+#robust invocation via JAVA_HOME
+function isabelle_java ()
+{
+ if [ -z "$JAVA_HOME" ]; then
+ echo "Unknown JAVA_HOME -- Java unavailable" >&2
+ return 127
+ else
+ local PRG="$1"; shift
+ "$JAVA_HOME/bin/$PRG" "$@"
+ fi
+}
+export -f isabelle_java
+
+#robust invocation via SCALA_HOME
+function isabelle_scala ()
+{
+ if [ -z "$JAVA_HOME" ]; then
+ echo "Unknown JAVA_HOME -- Java unavailable" >&2
+ return 127
+ elif [ -z "$SCALA_HOME" ]; then
+ echo "Unknown SCALA_HOME -- Scala unavailable" >&2
+ return 127
+ else
+ local PRG="$1"; shift
+ "$SCALA_HOME/bin/$PRG" "$@"
+ fi
+}
+export -f isabelle_scala
+
+#classpath
+function classpath ()
+{
+ for X in "$@"
+ do
+ if [ -z "$ISABELLE_CLASSPATH" ]; then
+ ISABELLE_CLASSPATH="$X"
+ else
+ ISABELLE_CLASSPATH="$ISABELLE_CLASSPATH:$X"
+ fi
+ done
+ export ISABELLE_CLASSPATH
+}
+export -f classpath
+
+#administrative build
+if [ -e "$ISABELLE_HOME/Admin/build" ]; then
+ function isabelle_admin_build ()
+ {
+ "$ISABELLE_HOME/Admin/build" "$@"
+ }
+else
+ function isabelle_admin_build () { return 0; }
+fi
+export -f isabelle_admin_build
+
+#arrays
+function splitarray ()
+{
+ SPLITARRAY=()
+ local IFS="$1"; shift
+ for X in $*
+ do
+ SPLITARRAY["${#SPLITARRAY[@]}"]="$X"
+ done
+}
+export -f splitarray
+
+#init component tree
+function init_component ()
+{
+ local COMPONENT="$1"
+ case "$COMPONENT" in
+ /*) ;;
+ *)
+ echo >&2 "Absolute component path required: \"$COMPONENT\""
+ exit 2
+ ;;
+ esac
+
+ if [ -d "$COMPONENT" ]; then
+ if [ -z "$ISABELLE_COMPONENTS" ]; then
+ ISABELLE_COMPONENTS="$COMPONENT"
+ else
+ ISABELLE_COMPONENTS="$ISABELLE_COMPONENTS:$COMPONENT"
+ fi
+ else
+ echo >&2 "### Missing Isabelle component: \"$COMPONENT\""
+ if [ -z "$ISABELLE_COMPONENTS_MISSING" ]; then
+ ISABELLE_COMPONENTS_MISSING="$COMPONENT"
+ else
+ ISABELLE_COMPONENTS_MISSING="$ISABELLE_COMPONENTS_MISSING:$COMPONENT"
+ fi
+ fi
+
+ if [ -f "$COMPONENT/etc/settings" ]; then
+ source "$COMPONENT/etc/settings"
+ local RC="$?"
+ if [ "$RC" -ne 0 ]; then
+ echo >&2 "Return code $RC from bash script: \"$COMPONENT/etc/settings\""
+ exit 2
+ fi
+ fi
+ if [ -f "$COMPONENT/etc/components" ]; then
+ init_components "$COMPONENT" "$COMPONENT/etc/components"
+ fi
+}
+export -f init_component
+
+#init component forest
+function init_components ()
+{
+ local BASE="$1"
+ local CATALOG="$2"
+ local COMPONENT=""
+ local -a COMPONENTS=()
+
+ if [ ! -f "$CATALOG" ]; then
+ echo >&2 "Bad component catalog file: \"$CATALOG\""
+ exit 2
+ fi
+
+ {
+ while { unset REPLY; read -r; test "$?" = 0 -o -n "$REPLY"; }
+ do
+ case "$REPLY" in
+ \#* | "") ;;
+ /*) COMPONENTS["${#COMPONENTS[@]}"]="$REPLY" ;;
+ *) COMPONENTS["${#COMPONENTS[@]}"]="$BASE/$REPLY" ;;
+ esac
+ done
+ } < "$CATALOG"
+
+ for COMPONENT in "${COMPONENTS[@]}"
+ do
+ init_component "$COMPONENT"
+ done
+}
+export -f init_components
+
+fi
--- a/lib/scripts/getsettings Thu Feb 25 16:53:34 2016 +0000
+++ b/lib/scripts/getsettings Thu Feb 25 20:23:32 2016 +0100
@@ -1,20 +1,21 @@
# -*- shell-script -*- :mode=shellscript:
#
-# Author: Markus Wenzel, TU Muenchen
+# Author: Makarius
#
-# getsettings - bash source script to augment current env.
+# Static Isabelle environment for root of process tree.
+
+export ISABELLE_HOME
+
+export BASH_ENV="$ISABELLE_HOME/lib/scripts/getfunctions"
+source "$BASH_ENV"
+
if [ -z "$ISABELLE_SETTINGS_PRESENT" ]
then
-set -o allexport
-
-ISABELLE_SETTINGS_PRESENT=true
+export ISABELLE_SETTINGS_PRESENT=true
-#GNU tar (notably on Mac OS X)
-if [ -x /usr/bin/gnutar ]; then
- function tar() { /usr/bin/gnutar "$@"; }
-fi
+set -o allexport
#sane environment defaults (notably on Mac OS X)
if [ "$ISABELLE_APP" = true -a -x /usr/libexec/path_helper ]; then
@@ -36,7 +37,6 @@
USER_HOME="$(cygpath -u "$USERPROFILE")"
fi
- function platform_path() { cygpath -i -C UTF8 -w -p "$@"; }
CYGWIN_ROOT="$(platform_path "/")"
ISABELLE_ROOT="$(platform_path "$ISABELLE_HOME")"
@@ -49,33 +49,15 @@
ISABELLE_ROOT="$ISABELLE_HOME"
- function platform_path() { echo "$@"; }
-
ISABELLE_CLASSPATH="$CLASSPATH"
unset CLASSPATH
fi
-export ISABELLE_HOME
-
-#key executables
+#main executables
ISABELLE_TOOL="$ISABELLE_HOME/bin/isabelle"
ISABELLE_PROCESS="$ISABELLE_HOME/bin/isabelle_process"
ISABELLE_SCALA_SCRIPT="$ISABELLE_HOME/bin/isabelle_scala_script"
-
-function isabelle ()
-{
- "$ISABELLE_TOOL" "$@"
-}
-
-function isabelle_process ()
-{
- "$ISABELLE_PROCESS" "$@"
-}
-
-function isabelle_scala_script ()
-{
- "$ISABELLE_SCALA_SCRIPT" "$@"
-}
+PATH="$ISABELLE_HOME/bin:$PATH"
#platform
source "$ISABELLE_HOME/lib/scripts/isabelle-platform"
@@ -88,186 +70,12 @@
ISABELLE_ID=""
[ -z "$ISABELLE_IDENTIFIER" ] && ISABELLE_IDENTIFIER=""
-#sometimes users put strange things in here ...
-unset ENV
-unset BASH_ENV
-
-#shared library convenience
-function librarypath ()
-{
- for X in "$@"
- do
- case "$ISABELLE_PLATFORM" in
- *-darwin)
- if [ -z "$DYLD_LIBRARY_PATH" ]; then
- DYLD_LIBRARY_PATH="$X"
- else
- DYLD_LIBRARY_PATH="$X:$DYLD_LIBRARY_PATH"
- fi
- export DYLD_LIBRARY_PATH
- ;;
- *)
- if [ -z "$LD_LIBRARY_PATH" ]; then
- LD_LIBRARY_PATH="$X"
- else
- LD_LIBRARY_PATH="$X:$LD_LIBRARY_PATH"
- fi
- export LD_LIBRARY_PATH
- ;;
- esac
- done
-}
-
-#robust invocation via ISABELLE_JDK_HOME
-function isabelle_jdk ()
-{
- if [ -z "$ISABELLE_JDK_HOME" ]; then
- echo "Unknown ISABELLE_JDK_HOME -- Java development tools unavailable" >&2
- return 127
- else
- local PRG="$1"; shift
- "$ISABELLE_JDK_HOME/bin/$PRG" "$@"
- fi
-}
-
-#robust invocation via JAVA_HOME
-function isabelle_java ()
-{
- if [ -z "$JAVA_HOME" ]; then
- echo "Unknown JAVA_HOME -- Java unavailable" >&2
- return 127
- else
- local PRG="$1"; shift
- "$JAVA_HOME/bin/$PRG" "$@"
- fi
-}
-
-#robust invocation via SCALA_HOME
-function isabelle_scala ()
-{
- if [ -z "$JAVA_HOME" ]; then
- echo "Unknown JAVA_HOME -- Java unavailable" >&2
- return 127
- elif [ -z "$SCALA_HOME" ]; then
- echo "Unknown SCALA_HOME -- Scala unavailable" >&2
- return 127
- else
- local PRG="$1"; shift
- "$SCALA_HOME/bin/$PRG" "$@"
- fi
-}
-
-#administrative build
-if [ -e "$ISABELLE_HOME/Admin/build" ]; then
- function isabelle_admin_build ()
- {
- "$ISABELLE_HOME/Admin/build" "$@"
- }
-else
- function isabelle_admin_build () { return 0; }
-fi
-
-#classpath
-function classpath ()
-{
- for X in "$@"
- do
- if [ -z "$ISABELLE_CLASSPATH" ]; then
- ISABELLE_CLASSPATH="$X"
- else
- ISABELLE_CLASSPATH="$ISABELLE_CLASSPATH:$X"
- fi
- done
- export ISABELLE_CLASSPATH
-}
-
-#arrays
-function splitarray ()
-{
- SPLITARRAY=()
- local IFS="$1"; shift
- for X in $*
- do
- SPLITARRAY["${#SPLITARRAY[@]}"]="$X"
- done
-}
-
# components
ISABELLE_COMPONENTS=""
ISABELLE_COMPONENTS_MISSING=""
-#init component tree
-function init_component ()
-{
- local COMPONENT="$1"
- case "$COMPONENT" in
- /*) ;;
- *)
- echo >&2 "Absolute component path required: \"$COMPONENT\""
- exit 2
- ;;
- esac
-
- if [ -d "$COMPONENT" ]; then
- if [ -z "$ISABELLE_COMPONENTS" ]; then
- ISABELLE_COMPONENTS="$COMPONENT"
- else
- ISABELLE_COMPONENTS="$ISABELLE_COMPONENTS:$COMPONENT"
- fi
- else
- echo >&2 "### Missing Isabelle component: \"$COMPONENT\""
- if [ -z "$ISABELLE_COMPONENTS_MISSING" ]; then
- ISABELLE_COMPONENTS_MISSING="$COMPONENT"
- else
- ISABELLE_COMPONENTS_MISSING="$ISABELLE_COMPONENTS_MISSING:$COMPONENT"
- fi
- fi
-
- if [ -f "$COMPONENT/etc/settings" ]; then
- source "$COMPONENT/etc/settings"
- local RC="$?"
- if [ "$RC" -ne 0 ]; then
- echo >&2 "Return code $RC from bash script: \"$COMPONENT/etc/settings\""
- exit 2
- fi
- fi
- if [ -f "$COMPONENT/etc/components" ]; then
- init_components "$COMPONENT" "$COMPONENT/etc/components"
- fi
-}
-
-#init component forest
-function init_components ()
-{
- local BASE="$1"
- local CATALOG="$2"
- local COMPONENT=""
- local -a COMPONENTS=()
-
- if [ ! -f "$CATALOG" ]; then
- echo >&2 "Bad component catalog file: \"$CATALOG\""
- exit 2
- fi
-
- {
- while { unset REPLY; read -r; test "$?" = 0 -o -n "$REPLY"; }
- do
- case "$REPLY" in
- \#* | "") ;;
- /*) COMPONENTS["${#COMPONENTS[@]}"]="$REPLY" ;;
- *) COMPONENTS["${#COMPONENTS[@]}"]="$BASE/$REPLY" ;;
- esac
- done
- } < "$CATALOG"
-
- for COMPONENT in "${COMPONENTS[@]}"
- do
- init_component "$COMPONENT"
- done
-}
-
#main components
init_component "$ISABELLE_HOME"
[ -d "$ISABELLE_HOME/Admin" ] && init_component "$ISABELLE_HOME/Admin"
--- a/src/Doc/System/Scala.thy Thu Feb 25 16:53:34 2016 +0000
+++ b/src/Doc/System/Scala.thy Thu Feb 25 20:23:32 2016 +0100
@@ -77,11 +77,7 @@
text \<open>
The executable @{executable "$ISABELLE_HOME/bin/isabelle_scala_script"}
allows to run Isabelle/Scala source files stand-alone programs, by using a
- suitable ``hash-bang'' line and executable file permissions.
-
- The subsequent example assumes that the main Isabelle binaries have been
- installed in some directory that is included in @{setting PATH} (see also
- @{tool "install"}):
+ suitable ``hash-bang'' line and executable file permissions. For example:
@{verbatim [display]
\<open>#!/usr/bin/env isabelle_scala_script
@@ -89,8 +85,12 @@
Console.println("browser_info = " + options.bool("browser_info"))
Console.println("document = " + options.string("document"))\<close>}
- Alternatively the full @{file "$ISABELLE_HOME/bin/isabelle_scala_script"}
- may be specified in expanded form.
+ This assumes that the executable may be found via the @{setting PATH} from
+ the process environment: this is the case when Isabelle settings are active,
+ e.g.\ in the context of the main Isabelle tool wrapper
+ \secref{sec:isabelle-tool}. Alternatively, the full @{file
+ "$ISABELLE_HOME/bin/isabelle_scala_script"} may be specified in expanded
+ form.
\<close>
end