diff --git a/lib/scripts/getfunctions b/lib/scripts/getfunctions
--- a/lib/scripts/getfunctions
+++ b/lib/scripts/getfunctions
@@ -1,276 +1,276 @@
 # -*- 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 "$@"; }
   function standard_path() { cygpath -i -u -p "$@" | tr -d '\r'; }
 else
   function platform_path() { echo "$@"; }
   function standard_path() { echo "$@"; }
 fi
 export -f platform_path standard_path
 
 #GNU tar (notably on macOS)
 if type -p gnutar >/dev/null
 then
   function tar() { gnutar "$@"; }
   export -f tar
 elif type -p gtar >/dev/null
 then
   function tar() { gtar "$@"; }
   export -f tar
 fi
 
 #OCaml management via OPAM
-function isabelle_opam()
+function isabelle_opam ()
 {
   if [ -z "$ISABELLE_OPAM" ]; then
     echo "Unknown ISABELLE_OPAM -- OCaml management tools unavailable" >&2
     return 127
   else
     env OPAMROOT="$ISABELLE_OPAM_ROOT" OPAMCOLOR="never" "$ISABELLE_OPAM" "$@"
   fi
 }
 export -f isabelle_opam
 
 #GHC management via Stack
-function isabelle_stack()
+function isabelle_stack ()
 {
   if [ -z "$ISABELLE_STACK" ]; then
     echo "Unknown ISABELLE_STACK -- GHC management tools unavailable" >&2
     return 127
   else
     env STACK_ROOT="$(platform_path "$ISABELLE_STACK_ROOT")" "$ISABELLE_STACK" --resolver "$ISABELLE_STACK_RESOLVER" --compiler "$ISABELLE_GHC_VERSION" "$@"
   fi
 }
 export -f isabelle_stack
 
 #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 ()
 {
   local X=""
   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
 
 #Isabelle fonts
 function isabelle_fonts ()
 {
   local X=""
   for X in "$@"
   do
     if [ -z "$ISABELLE_FONTS" ]; then
       ISABELLE_FONTS="$X"
     else
       ISABELLE_FONTS="$ISABELLE_FONTS:$X"
     fi
   done
   export ISABELLE_FONTS
 }
 export -f isabelle_fonts
 
 function isabelle_fonts_hidden ()
 {
   local X=""
   for X in "$@"
   do
     if [ -z "$ISABELLE_FONTS_HIDDEN" ]; then
       ISABELLE_FONTS_HIDDEN="$X"
     else
       ISABELLE_FONTS_HIDDEN="$ISABELLE_FONTS_HIDDEN:$X"
     fi
   done
   export ISABELLE_FONTS_HIDDEN
 }
 export -f isabelle_fonts_hidden
 
 #Isabelle/Scala services
 function isabelle_scala_service ()
 {
   local X=""
   for X in "$@"
   do
     if [ -z "$ISABELLE_SCALA_SERVICES" ]; then
       ISABELLE_SCALA_SERVICES="$X"
     else
       ISABELLE_SCALA_SERVICES="$ISABELLE_SCALA_SERVICES:$X"
     fi
   done
   export ISABELLE_SCALA_SERVICES
 }
 export -f isabelle_scala_service
 
 #Special directories
 function isabelle_directory ()
 {
   local X=""
   for X in "$@"
   do
     if [ -z "$ISABELLE_DIRECTORIES" ]; then
       ISABELLE_DIRECTORIES="$X"
     else
       ISABELLE_DIRECTORIES="$ISABELLE_DIRECTORIES:$X"
     fi
   done
   export ISABELLE_DIRECTORIES
 }
 export -f isabelle_directory
 
 #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
   local X=""
   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 REPLY=""
   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