renamed "isabelle-process" to "isabelle_process", with shell function to avoid dynamic path lookups;

--- a/NEWS	Sun Apr 06 16:36:28 2014 +0200
+++ b/NEWS	Sun Apr 06 16:59:41 2014 +0200
@@ -662,6 +662,13 @@
 repeated invocation in PIDE front-end: re-use single file
 $ISABELLE_HOME_USER/tmp/drafts.pdf and corresponding views.
 
+* The raw Isabelle process executable has been renamed from
+"isabelle-process" to "isabelle_process", which conforms to common
+shell naming conventions, and allows to define a shell function within
+the Isabelle environment to avoid dynamic path lookup.  Rare
+incompatibility for old tools that do not use the $ISABELLE_PROCESS
+settings variable yet.
+
 
 
 New in Isabelle2013-2 (December 2013)

--- a/bin/isabelle-process	Sun Apr 06 16:36:28 2014 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,249 +0,0 @@
-#!/usr/bin/env bash
-#
-# Author: Markus Wenzel, TU Muenchen
-#
-# Isabelle process startup script.
-
-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
-
-
-## settings
-
-PRG="$(basename "$0")"
-
-ISABELLE_HOME="$(cd "$(dirname "$0")"; cd "$(pwd -P)"; cd ..; pwd)"
-source "$ISABELLE_HOME/lib/scripts/getsettings" || exit 2
-
-
-## diagnostics
-
-function usage()
-{
-  echo
-  echo "Usage: $PRG [OPTIONS] [INPUT] [OUTPUT]"
-  echo
-  echo "  Options are:"
-  echo "    -I           startup Isar interaction mode"
-  echo "    -P           startup Proof General interaction mode"
-  echo "    -S           secure mode -- disallow critical operations"
-  echo "    -T ADDR      startup process wrapper, with socket address"
-  echo "    -W IN:OUT    startup process wrapper, with input/output fifos"
-  echo "    -e MLTEXT    pass MLTEXT to the ML session"
-  echo "    -m MODE      add print mode for output"
-  echo "    -o OPTION    override Isabelle system OPTION (via NAME=VAL or NAME)"
-  echo "    -q           non-interactive session"
-  echo "    -r           open heap file read-only"
-  echo "    -w           reset write permissions on OUTPUT"
-  echo
-  echo "  INPUT (default \"$ISABELLE_LOGIC\") and OUTPUT specify in/out heaps."
-  echo "  These are either names to be searched in the Isabelle path, or"
-  echo "  actual file names (containing at least one /)."
-  echo "  If INPUT is \"RAW_ML_SYSTEM\", just start the bare bones ML system."
-  echo
-  exit 1
-}
-
-function fail()
-{
-  echo "$1" >&2
-  exit 2
-}
-
-
-## process command line
-
-# options
-
-ISAR=""
-PROOFGENERAL=""
-SECURE=""
-WRAPPER_SOCKET=""
-WRAPPER_FIFOS=""
-MLTEXT=""
-MODES=""
-declare -a SYSTEM_OPTIONS=()
-TERMINATE=""
-READONLY=""
-NOWRITE=""
-
-while getopts "IPST:W:e:m:o:qrw" OPT
-do
-  case "$OPT" in
-    I)
-      ISAR=true
-      ;;
-    P)
-      PROOFGENERAL=true
-      ;;
-    S)
-      SECURE=true
-      ;;
-    T)
-      WRAPPER_SOCKET="$OPTARG"
-      ;;
-    W)
-      WRAPPER_FIFOS="$OPTARG"
-      ;;
-    e)
-      MLTEXT="$MLTEXT $OPTARG"
-      ;;
-    m)
-      if [ -z "$MODES" ]; then
-        MODES="\"$OPTARG\""
-      else
-        MODES="\"$OPTARG\", $MODES"
-      fi
-      ;;
-    o)
-      SYSTEM_OPTIONS["${#SYSTEM_OPTIONS[@]}"]="$OPTARG"
-      ;;
-    q)
-      TERMINATE=true
-      ;;
-    r)
-      READONLY=true
-      ;;
-    w)
-      NOWRITE=true
-      ;;
-    \?)
-      usage
-      ;;
-  esac
-done
-
-shift $(($OPTIND - 1))
-
-
-# args
-
-INPUT=""
-OUTPUT=""
-
-if [ "$#" -ge 1 ]; then
-  INPUT="$1"
-  shift
-fi
-
-if [ "$#" -ge 1 ]; then
-  OUTPUT="$1"
-  shift
-fi
-
-[ "$#" -ne 0 ] && { echo "Bad args: $*"; usage; }
-
-
-## check ML system
-
-[ -z "$ML_SYSTEM" ] && fail "Missing ML system settings! Unable to run Isabelle."
-
-
-## input heap file
-
-[ -z "$INPUT" ] && INPUT="$ISABELLE_LOGIC"
-
-case "$INPUT" in
-  RAW_ML_SYSTEM)
-    INFILE=""
-    ;;
-  */*)
-    INFILE="$INPUT"
-    [ ! -f "$INFILE" ] && fail "Bad heap file: \"$INFILE\""
-    ;;
-  *)
-    INFILE=""
-    ISA_PATH=""
-
-    splitarray ":" "$ISABELLE_PATH"; PATHS=("${SPLITARRAY[@]}")
-    for DIR in "${PATHS[@]}"
-    do
-      DIR="$DIR/$ML_IDENTIFIER"
-      ISA_PATH="$ISA_PATH  $DIR\n"
-      [ -z "$INFILE" -a -f "$DIR/$INPUT" ] && INFILE="$DIR/$INPUT"
-    done
-
-    if [ -z "$INFILE" ]; then
-      echo "Unknown logic \"$INPUT\" -- no heap file found in:" >&2
-      echo -ne "$ISA_PATH" >&2
-      exit 2
-    fi
-    ;;
-esac
-
-
-## output heap file
-
-case "$OUTPUT" in
-  "")
-    if [ -z "$READONLY" -a -w "$INFILE" ]; then
-      perl -e "exit (((stat('$INFILE'))[2] & 0222) != 0 ? 0 : 1);" && OUTFILE="$INFILE"
-    fi
-    ;;
-  */*)
-    OUTFILE="$OUTPUT"
-    ;;
-  *)
-    mkdir -p "$ISABELLE_OUTPUT"
-    OUTFILE="$ISABELLE_OUTPUT/$OUTPUT"
-    ;;
-esac
-
-
-## prepare tmp directory
-
-[ -z "$ISABELLE_TMP_PREFIX" ] && ISABELLE_TMP_PREFIX=/tmp/isabelle
-ISABELLE_PID="$$"
-ISABELLE_TMP="$ISABELLE_TMP_PREFIX$ISABELLE_PID"
-mkdir -p "$ISABELLE_TMP"
-
-
-## run it!
-
-ML_SYSTEM_BASE=$(echo "$ML_SYSTEM" | cut -f1 -d-)
-
-[ -n "$MODES" ] && MLTEXT="Unsynchronized.change print_mode (append [$MODES]); $MLTEXT"
-
-[ -n "$SECURE" ] && MLTEXT="$MLTEXT; Secure.set_secure ();"
-
-NICE="nice"
-
-if [ -n "$WRAPPER_SOCKET" ]; then
-  MLTEXT="$MLTEXT; Isabelle_Process.init_socket \"$WRAPPER_SOCKET\";"
-elif [ -n "$WRAPPER_FIFOS" ]; then
-  splitarray ":" "$WRAPPER_FIFOS"; FIFOS=("${SPLITARRAY[@]}")
-  [ "${#FIFOS[@]}" -eq 2 ] || fail "Expected IN:OUT fifo specification"
-  [ -p "${FIFOS[0]}" ] || fail "Bad input fifo: ${FIFOS[0]}"
-  [ -p "${FIFOS[1]}" ] || fail "Bad output fifo: ${FIFOS[1]}"
-  MLTEXT="$MLTEXT; Isabelle_Process.init_fifos \"${FIFOS[0]}\" \"${FIFOS[1]}\";"
-else
-  ISABELLE_PROCESS_OPTIONS="$ISABELLE_TMP/options"
-  "$ISABELLE_TOOL" options -x "$ISABELLE_PROCESS_OPTIONS" -- "${SYSTEM_OPTIONS[@]}" || \
-    fail "Failed to retrieve Isabelle system options"
-  if [ "$INPUT" != RAW_ML_SYSTEM -a "$INPUT" != RAW ]; then
-    MLTEXT="Options.load_default () handle _ => exit 2; $MLTEXT"
-  fi
-  if [ -n "$PROOFGENERAL" ]; then
-    MLTEXT="$MLTEXT; ProofGeneral.init ();"
-  elif [ -n "$ISAR" ]; then
-    MLTEXT="$MLTEXT; Isar.main ();"
-  else
-    NICE=""
-  fi
-fi
-
-export INFILE OUTFILE MLTEXT TERMINATE NOWRITE ISABELLE_PID ISABELLE_TMP ISABELLE_PROCESS_OPTIONS
-
-if [ -f "$ISABELLE_HOME/lib/scripts/run-$ML_SYSTEM" ]; then
-  $NICE "$ISABELLE_HOME/lib/scripts/run-$ML_SYSTEM"
-else
-  $NICE "$ISABELLE_HOME/lib/scripts/run-$ML_SYSTEM_BASE"
-fi
-RC="$?"
-
-[ -n "$ISABELLE_PROCESS_OPTIONS" ] && rm -f "$ISABELLE_PROCESS_OPTIONS"
-rmdir "$ISABELLE_TMP"
-
-exit "$RC"

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/bin/isabelle_process	Sun Apr 06 16:59:41 2014 +0200
@@ -0,0 +1,249 @@
+#!/usr/bin/env bash
+#
+# Author: Markus Wenzel, TU Muenchen
+#
+# Isabelle process startup script.
+
+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
+
+
+## settings
+
+PRG="$(basename "$0")"
+
+ISABELLE_HOME="$(cd "$(dirname "$0")"; cd "$(pwd -P)"; cd ..; pwd)"
+source "$ISABELLE_HOME/lib/scripts/getsettings" || exit 2
+
+
+## diagnostics
+
+function usage()
+{
+  echo
+  echo "Usage: $PRG [OPTIONS] [INPUT] [OUTPUT]"
+  echo
+  echo "  Options are:"
+  echo "    -I           startup Isar interaction mode"
+  echo "    -P           startup Proof General interaction mode"
+  echo "    -S           secure mode -- disallow critical operations"
+  echo "    -T ADDR      startup process wrapper, with socket address"
+  echo "    -W IN:OUT    startup process wrapper, with input/output fifos"
+  echo "    -e MLTEXT    pass MLTEXT to the ML session"
+  echo "    -m MODE      add print mode for output"
+  echo "    -o OPTION    override Isabelle system OPTION (via NAME=VAL or NAME)"
+  echo "    -q           non-interactive session"
+  echo "    -r           open heap file read-only"
+  echo "    -w           reset write permissions on OUTPUT"
+  echo
+  echo "  INPUT (default \"$ISABELLE_LOGIC\") and OUTPUT specify in/out heaps."
+  echo "  These are either names to be searched in the Isabelle path, or"
+  echo "  actual file names (containing at least one /)."
+  echo "  If INPUT is \"RAW_ML_SYSTEM\", just start the bare bones ML system."
+  echo
+  exit 1
+}
+
+function fail()
+{
+  echo "$1" >&2
+  exit 2
+}
+
+
+## process command line
+
+# options
+
+ISAR=""
+PROOFGENERAL=""
+SECURE=""
+WRAPPER_SOCKET=""
+WRAPPER_FIFOS=""
+MLTEXT=""
+MODES=""
+declare -a SYSTEM_OPTIONS=()
+TERMINATE=""
+READONLY=""
+NOWRITE=""
+
+while getopts "IPST:W:e:m:o:qrw" OPT
+do
+  case "$OPT" in
+    I)
+      ISAR=true
+      ;;
+    P)
+      PROOFGENERAL=true
+      ;;
+    S)
+      SECURE=true
+      ;;
+    T)
+      WRAPPER_SOCKET="$OPTARG"
+      ;;
+    W)
+      WRAPPER_FIFOS="$OPTARG"
+      ;;
+    e)
+      MLTEXT="$MLTEXT $OPTARG"
+      ;;
+    m)
+      if [ -z "$MODES" ]; then
+        MODES="\"$OPTARG\""
+      else
+        MODES="\"$OPTARG\", $MODES"
+      fi
+      ;;
+    o)
+      SYSTEM_OPTIONS["${#SYSTEM_OPTIONS[@]}"]="$OPTARG"
+      ;;
+    q)
+      TERMINATE=true
+      ;;
+    r)
+      READONLY=true
+      ;;
+    w)
+      NOWRITE=true
+      ;;
+    \?)
+      usage
+      ;;
+  esac
+done
+
+shift $(($OPTIND - 1))
+
+
+# args
+
+INPUT=""
+OUTPUT=""
+
+if [ "$#" -ge 1 ]; then
+  INPUT="$1"
+  shift
+fi
+
+if [ "$#" -ge 1 ]; then
+  OUTPUT="$1"
+  shift
+fi
+
+[ "$#" -ne 0 ] && { echo "Bad args: $*"; usage; }
+
+
+## check ML system
+
+[ -z "$ML_SYSTEM" ] && fail "Missing ML system settings! Unable to run Isabelle."
+
+
+## input heap file
+
+[ -z "$INPUT" ] && INPUT="$ISABELLE_LOGIC"
+
+case "$INPUT" in
+  RAW_ML_SYSTEM)
+    INFILE=""
+    ;;
+  */*)
+    INFILE="$INPUT"
+    [ ! -f "$INFILE" ] && fail "Bad heap file: \"$INFILE\""
+    ;;
+  *)
+    INFILE=""
+    ISA_PATH=""
+
+    splitarray ":" "$ISABELLE_PATH"; PATHS=("${SPLITARRAY[@]}")
+    for DIR in "${PATHS[@]}"
+    do
+      DIR="$DIR/$ML_IDENTIFIER"
+      ISA_PATH="$ISA_PATH  $DIR\n"
+      [ -z "$INFILE" -a -f "$DIR/$INPUT" ] && INFILE="$DIR/$INPUT"
+    done
+
+    if [ -z "$INFILE" ]; then
+      echo "Unknown logic \"$INPUT\" -- no heap file found in:" >&2
+      echo -ne "$ISA_PATH" >&2
+      exit 2
+    fi
+    ;;
+esac
+
+
+## output heap file
+
+case "$OUTPUT" in
+  "")
+    if [ -z "$READONLY" -a -w "$INFILE" ]; then
+      perl -e "exit (((stat('$INFILE'))[2] & 0222) != 0 ? 0 : 1);" && OUTFILE="$INFILE"
+    fi
+    ;;
+  */*)
+    OUTFILE="$OUTPUT"
+    ;;
+  *)
+    mkdir -p "$ISABELLE_OUTPUT"
+    OUTFILE="$ISABELLE_OUTPUT/$OUTPUT"
+    ;;
+esac
+
+
+## prepare tmp directory
+
+[ -z "$ISABELLE_TMP_PREFIX" ] && ISABELLE_TMP_PREFIX=/tmp/isabelle
+ISABELLE_PID="$$"
+ISABELLE_TMP="$ISABELLE_TMP_PREFIX$ISABELLE_PID"
+mkdir -p "$ISABELLE_TMP"
+
+
+## run it!
+
+ML_SYSTEM_BASE=$(echo "$ML_SYSTEM" | cut -f1 -d-)
+
+[ -n "$MODES" ] && MLTEXT="Unsynchronized.change print_mode (append [$MODES]); $MLTEXT"
+
+[ -n "$SECURE" ] && MLTEXT="$MLTEXT; Secure.set_secure ();"
+
+NICE="nice"
+
+if [ -n "$WRAPPER_SOCKET" ]; then
+  MLTEXT="$MLTEXT; Isabelle_Process.init_socket \"$WRAPPER_SOCKET\";"
+elif [ -n "$WRAPPER_FIFOS" ]; then
+  splitarray ":" "$WRAPPER_FIFOS"; FIFOS=("${SPLITARRAY[@]}")
+  [ "${#FIFOS[@]}" -eq 2 ] || fail "Expected IN:OUT fifo specification"
+  [ -p "${FIFOS[0]}" ] || fail "Bad input fifo: ${FIFOS[0]}"
+  [ -p "${FIFOS[1]}" ] || fail "Bad output fifo: ${FIFOS[1]}"
+  MLTEXT="$MLTEXT; Isabelle_Process.init_fifos \"${FIFOS[0]}\" \"${FIFOS[1]}\";"
+else
+  ISABELLE_PROCESS_OPTIONS="$ISABELLE_TMP/options"
+  "$ISABELLE_TOOL" options -x "$ISABELLE_PROCESS_OPTIONS" -- "${SYSTEM_OPTIONS[@]}" || \
+    fail "Failed to retrieve Isabelle system options"
+  if [ "$INPUT" != RAW_ML_SYSTEM -a "$INPUT" != RAW ]; then
+    MLTEXT="Options.load_default () handle _ => exit 2; $MLTEXT"
+  fi
+  if [ -n "$PROOFGENERAL" ]; then
+    MLTEXT="$MLTEXT; ProofGeneral.init ();"
+  elif [ -n "$ISAR" ]; then
+    MLTEXT="$MLTEXT; Isar.main ();"
+  else
+    NICE=""
+  fi
+fi
+
+export INFILE OUTFILE MLTEXT TERMINATE NOWRITE ISABELLE_PID ISABELLE_TMP ISABELLE_PROCESS_OPTIONS
+
+if [ -f "$ISABELLE_HOME/lib/scripts/run-$ML_SYSTEM" ]; then
+  $NICE "$ISABELLE_HOME/lib/scripts/run-$ML_SYSTEM"
+else
+  $NICE "$ISABELLE_HOME/lib/scripts/run-$ML_SYSTEM_BASE"
+fi
+RC="$?"
+
+[ -n "$ISABELLE_PROCESS_OPTIONS" ] && rm -f "$ISABELLE_PROCESS_OPTIONS"
+rmdir "$ISABELLE_TMP"
+
+exit "$RC"

--- a/lib/Tools/install	Sun Apr 06 16:36:28 2014 +0200
+++ b/lib/Tools/install	Sun Apr 06 16:59:41 2014 +0200
@@ -63,7 +63,7 @@
 
 mkdir -p "$BINDIR" || fail "Bad directory: \"$BINDIR\""
 
-for NAME in isabelle isabelle-process isabelle_scala_script
+for NAME in isabelle isabelle_process isabelle_scala_script
 do
   BIN="$BINDIR/$NAME"
   DIST="$DISTDIR/bin/$NAME"

--- a/lib/scripts/getsettings	Sun Apr 06 16:36:28 2014 +0200
+++ b/lib/scripts/getsettings	Sun Apr 06 16:59:41 2014 +0200
@@ -44,9 +44,14 @@
 export ISABELLE_HOME
 
 #key executables
-ISABELLE_PROCESS="$ISABELLE_HOME/bin/isabelle-process"
+ISABELLE_PROCESS="$ISABELLE_HOME/bin/isabelle_process"
 ISABELLE_TOOL="$ISABELLE_HOME/bin/isabelle"
 
+function isabelle_process ()
+{
+  "$ISABELLE_PROCESS" "$@"
+}
+
 function isabelle ()
 {
   "$ISABELLE_TOOL" "$@"

--- a/src/Doc/System/Basics.thy	Sun Apr 06 16:36:28 2014 +0200
+++ b/src/Doc/System/Basics.thy	Sun Apr 06 16:59:41 2014 +0200
@@ -22,7 +22,7 @@
   and user interfaces).
 
   \item The raw \emph{Isabelle process} (@{executable_ref
-  "isabelle-process"}) runs logic sessions either interactively or in
+  "isabelle_process"}) runs logic sessions either interactively or in
   batch mode.  In particular, this view abstracts over the invocation
   of the actual ML system to be used.  Regular users rarely need to
   care about the low-level process.
@@ -122,7 +122,7 @@
 
   \item @{setting_def ISABELLE_PROCESS} and @{setting_def ISABELLE_TOOL} are set
   automatically to the absolute path names of the @{executable
-  "isabelle-process"} and @{executable isabelle} executables,
+  "isabelle_process"} and @{executable isabelle} executables,
   respectively.
   
   \item @{setting_ref ISABELLE_OUTPUT} will have the identifiers of
@@ -193,7 +193,7 @@
 
   \item[@{setting_def ISABELLE_PROCESS}@{text "\<^sup>*"}, @{setting
   ISABELLE_TOOL}@{text "\<^sup>*"}] are automatically set to the full path
-  names of the @{executable "isabelle-process"} and @{executable
+  names of the @{executable "isabelle_process"} and @{executable
   isabelle} executables, respectively.  Thus other tools and scripts
   need not assume that the @{file "$ISABELLE_HOME/bin"} directory is
   on the current search path of the shell.
@@ -271,7 +271,7 @@
   for displaying @{verbatim dvi} files.
   
   \item[@{setting_def ISABELLE_TMP_PREFIX}@{text "\<^sup>*"}] is the
-  prefix from which any running @{executable "isabelle-process"}
+  prefix from which any running @{executable "isabelle_process"}
   derives an individual directory for temporary files.  The default is
   somewhere in @{file_unchecked "/tmp"}.
   
@@ -353,13 +353,13 @@
 section {* The raw Isabelle process *}
 
 text {*
-  The @{executable_def "isabelle-process"} executable runs bare-bones
+  The @{executable_def "isabelle_process"} executable runs bare-bones
   Isabelle logic sessions --- either interactively or in batch mode.
   It provides an abstraction over the underlying ML system, and over
   the actual heap file locations.  Its usage is:
 
 \begin{ttbox}
-Usage: isabelle-process [OPTIONS] [INPUT] [OUTPUT]
+Usage: isabelle_process [OPTIONS] [INPUT] [OUTPUT]
 
   Options are:
     -I           startup Isar interaction mode
@@ -455,7 +455,7 @@
   Run an interactive session of the default object-logic (as specified
   by the @{setting ISABELLE_LOGIC} setting) like this:
 \begin{ttbox}
-isabelle-process
+isabelle_process
 \end{ttbox}
 
   Usually @{setting ISABELLE_LOGIC} refers to one of the standard
@@ -464,7 +464,7 @@
   directory specified by the @{setting ISABELLE_OUTPUT} setting) ---
   may be invoked as follows:
 \begin{ttbox}
-isabelle-process HOL Test
+isabelle_process HOL Test
 \end{ttbox}
   Ending this session normally (e.g.\ by typing control-D) dumps the
   whole ML system state into @{verbatim Test} (be prepared for more
@@ -473,11 +473,11 @@
   The @{verbatim Test} session may be continued later (still in
   writable state) by:
 \begin{ttbox}
-isabelle-process Test
+isabelle_process Test
 \end{ttbox}
   A read-only @{verbatim Test} session may be started by:
 \begin{ttbox}
-isabelle-process -r Test
+isabelle_process -r Test
 \end{ttbox}
 
   \bigskip The next example demonstrates batch execution of Isabelle.
@@ -485,7 +485,7 @@
   within ML (observe the delicate quoting rules for the Bash shell
   vs.\ ML):
 \begin{ttbox}
-isabelle-process -e 'Thy_Info.get_theory "Main";' -q -r HOL
+isabelle_process -e 'Thy_Info.get_theory "Main";' -q -r HOL
 \end{ttbox}
   Note that the output text will be interspersed with additional junk
   messages by the ML runtime environment.  The @{verbatim "-W"} option

--- a/src/Doc/System/Misc.thy	Sun Apr 06 16:36:28 2014 +0200
+++ b/src/Doc/System/Misc.thy	Sun Apr 06 16:59:41 2014 +0200
@@ -200,7 +200,7 @@
   distribution directory as determined by @{setting ISABELLE_HOME}.
 
   The @{text BINDIR} argument tells where executable wrapper scripts
-  for @{executable "isabelle-process"} and @{executable isabelle}
+  for @{executable "isabelle_process"} and @{executable isabelle}
   should be placed, which is typically a directory in the shell's
   @{setting PATH}, such as @{verbatim "$HOME/bin"}.
 

--- a/src/Doc/System/Presentation.thy	Sun Apr 06 16:36:28 2014 +0200
+++ b/src/Doc/System/Presentation.thy	Sun Apr 06 16:59:41 2014 +0200
@@ -15,7 +15,7 @@
   The tools @{tool_ref mkroot} and @{tool_ref build} provide the
   primary means for managing Isabelle sessions, including proper setup
   for presentation; @{tool build} takes care to have @{executable_ref
-  "isabelle-process"} run any additional stages required for document
+  "isabelle_process"} run any additional stages required for document
   preparation, notably the @{tool_ref document} and @{tool_ref latex}.
   The complete tool chain for managing batch-mode Isabelle sessions is
   illustrated in \figref{fig:session-tools}.
@@ -31,7 +31,7 @@
       @{tool_ref build} & invoked repeatedly by the user to keep
       session output up-to-date (HTML, documents etc.); \\
 
-      @{executable "isabelle-process"} & run through @{tool_ref
+      @{executable "isabelle_process"} & run through @{tool_ref
       build}; \\
 
       @{tool_ref document} & run by the Isabelle process if document