# HG changeset patch
# User wenzelm
# Date 1456428212 -3600
# Node ID d515293f59709f342907224417f0055af17ade58
# Parent  994b8bab5a99dcba2722c3ceff6147dd5485e6cf# Parent  cb6c4e307b1c7a97b7b5f3a28f1522eea86b0364
merged

diff -r 994b8bab5a99 -r d515293f5970 NEWS
--- 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.
 
 
diff -r 994b8bab5a99 -r d515293f5970 lib/scripts/getfunctions
--- /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
diff -r 994b8bab5a99 -r d515293f5970 lib/scripts/getsettings
--- 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"
diff -r 994b8bab5a99 -r d515293f5970 src/Doc/System/Scala.thy
--- 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