lib/scripts/getsettings
changeset 62412 ffdc5cf36dc5
parent 62354 fdd6989cc8a0
child 62413 c6111df4a4f8
     1.1 --- a/lib/scripts/getsettings	Thu Feb 25 16:16:29 2016 +0100
     1.2 +++ b/lib/scripts/getsettings	Thu Feb 25 17:49:04 2016 +0100
     1.3 @@ -1,8 +1,8 @@
     1.4  # -*- shell-script -*- :mode=shellscript:
     1.5  #
     1.6 -# Author: Markus Wenzel, TU Muenchen
     1.7 +# Author: Makarius
     1.8  #
     1.9 -# getsettings - bash source script to augment current env.
    1.10 +# Static Isabelle environment for root of process tree.
    1.11  
    1.12  if [ -z "$ISABELLE_SETTINGS_PRESENT" ]
    1.13  then
    1.14 @@ -11,10 +11,9 @@
    1.15  
    1.16  ISABELLE_SETTINGS_PRESENT=true
    1.17  
    1.18 -#GNU tar (notably on Mac OS X)
    1.19 -if [ -x /usr/bin/gnutar ]; then
    1.20 -  function tar() { /usr/bin/gnutar "$@"; }
    1.21 -fi
    1.22 +BASH_ENV="$ISABELLE_HOME/lib/scripts/getfunctions"
    1.23 +source "$BASH_ENV"
    1.24 +set -o allexport
    1.25  
    1.26  #sane environment defaults (notably on Mac OS X)
    1.27  if [ "$ISABELLE_APP" = true -a -x /usr/libexec/path_helper ]; then
    1.28 @@ -36,7 +35,6 @@
    1.29      USER_HOME="$(cygpath -u "$USERPROFILE")"
    1.30    fi
    1.31  
    1.32 -  function platform_path() { cygpath -i -C UTF8 -w -p "$@"; }
    1.33    CYGWIN_ROOT="$(platform_path "/")"
    1.34    ISABELLE_ROOT="$(platform_path "$ISABELLE_HOME")"
    1.35  
    1.36 @@ -49,34 +47,17 @@
    1.37  
    1.38    ISABELLE_ROOT="$ISABELLE_HOME"
    1.39  
    1.40 -  function platform_path() { echo "$@"; }
    1.41 -
    1.42    ISABELLE_CLASSPATH="$CLASSPATH"
    1.43    unset CLASSPATH
    1.44  fi
    1.45  
    1.46  export ISABELLE_HOME
    1.47  
    1.48 -#key executables
    1.49 +#main executables
    1.50  ISABELLE_TOOL="$ISABELLE_HOME/bin/isabelle"
    1.51  ISABELLE_PROCESS="$ISABELLE_HOME/bin/isabelle_process"
    1.52  ISABELLE_SCALA_SCRIPT="$ISABELLE_HOME/bin/isabelle_scala_script"
    1.53  
    1.54 -function isabelle ()
    1.55 -{
    1.56 -  "$ISABELLE_TOOL" "$@"
    1.57 -}
    1.58 -
    1.59 -function isabelle_process ()
    1.60 -{
    1.61 -  "$ISABELLE_PROCESS" "$@"
    1.62 -}
    1.63 -
    1.64 -function isabelle_scala_script ()
    1.65 -{
    1.66 -  "$ISABELLE_SCALA_SCRIPT" "$@"
    1.67 -}
    1.68 -
    1.69  #platform
    1.70  source "$ISABELLE_HOME/lib/scripts/isabelle-platform"
    1.71  if [ -z "$ISABELLE_PLATFORM" ]; then
    1.72 @@ -88,186 +69,12 @@
    1.73  ISABELLE_ID=""
    1.74  [ -z "$ISABELLE_IDENTIFIER" ] && ISABELLE_IDENTIFIER=""
    1.75  
    1.76 -#sometimes users put strange things in here ...
    1.77 -unset ENV
    1.78 -unset BASH_ENV
    1.79 -
    1.80 -#shared library convenience
    1.81 -function librarypath ()
    1.82 -{
    1.83 -  for X in "$@"
    1.84 -  do
    1.85 -    case "$ISABELLE_PLATFORM" in
    1.86 -      *-darwin)
    1.87 -        if [ -z "$DYLD_LIBRARY_PATH" ]; then
    1.88 -          DYLD_LIBRARY_PATH="$X"
    1.89 -        else
    1.90 -          DYLD_LIBRARY_PATH="$X:$DYLD_LIBRARY_PATH"
    1.91 -        fi
    1.92 -        export DYLD_LIBRARY_PATH
    1.93 -        ;;
    1.94 -      *)
    1.95 -        if [ -z "$LD_LIBRARY_PATH" ]; then
    1.96 -          LD_LIBRARY_PATH="$X"
    1.97 -        else
    1.98 -          LD_LIBRARY_PATH="$X:$LD_LIBRARY_PATH"
    1.99 -        fi
   1.100 -        export LD_LIBRARY_PATH
   1.101 -        ;;
   1.102 -    esac
   1.103 -  done
   1.104 -}
   1.105 -
   1.106 -#robust invocation via ISABELLE_JDK_HOME
   1.107 -function isabelle_jdk ()
   1.108 -{
   1.109 -  if [ -z "$ISABELLE_JDK_HOME" ]; then
   1.110 -    echo "Unknown ISABELLE_JDK_HOME -- Java development tools unavailable" >&2
   1.111 -    return 127
   1.112 -  else
   1.113 -    local PRG="$1"; shift
   1.114 -    "$ISABELLE_JDK_HOME/bin/$PRG" "$@"
   1.115 -  fi
   1.116 -}
   1.117 -
   1.118 -#robust invocation via JAVA_HOME
   1.119 -function isabelle_java ()
   1.120 -{
   1.121 -  if [ -z "$JAVA_HOME" ]; then
   1.122 -    echo "Unknown JAVA_HOME -- Java unavailable" >&2
   1.123 -    return 127
   1.124 -  else
   1.125 -    local PRG="$1"; shift
   1.126 -    "$JAVA_HOME/bin/$PRG" "$@"
   1.127 -  fi
   1.128 -}
   1.129 -
   1.130 -#robust invocation via SCALA_HOME
   1.131 -function isabelle_scala ()
   1.132 -{
   1.133 -  if [ -z "$JAVA_HOME" ]; then
   1.134 -    echo "Unknown JAVA_HOME -- Java unavailable" >&2
   1.135 -    return 127
   1.136 -  elif [ -z "$SCALA_HOME" ]; then
   1.137 -    echo "Unknown SCALA_HOME -- Scala unavailable" >&2
   1.138 -    return 127
   1.139 -  else
   1.140 -    local PRG="$1"; shift
   1.141 -    "$SCALA_HOME/bin/$PRG" "$@"
   1.142 -  fi
   1.143 -}
   1.144 -
   1.145 -#administrative build
   1.146 -if [ -e "$ISABELLE_HOME/Admin/build" ]; then
   1.147 -  function isabelle_admin_build ()
   1.148 -  {
   1.149 -    "$ISABELLE_HOME/Admin/build" "$@"
   1.150 -  }
   1.151 -else
   1.152 -  function isabelle_admin_build () { return 0; }
   1.153 -fi
   1.154 -
   1.155 -#classpath
   1.156 -function classpath ()
   1.157 -{
   1.158 -  for X in "$@"
   1.159 -  do
   1.160 -    if [ -z "$ISABELLE_CLASSPATH" ]; then
   1.161 -      ISABELLE_CLASSPATH="$X"
   1.162 -    else
   1.163 -      ISABELLE_CLASSPATH="$ISABELLE_CLASSPATH:$X"
   1.164 -    fi
   1.165 -  done
   1.166 -  export ISABELLE_CLASSPATH
   1.167 -}
   1.168 -
   1.169 -#arrays
   1.170 -function splitarray ()
   1.171 -{
   1.172 -  SPLITARRAY=()
   1.173 -  local IFS="$1"; shift
   1.174 -  for X in $*
   1.175 -  do
   1.176 -    SPLITARRAY["${#SPLITARRAY[@]}"]="$X"
   1.177 -  done
   1.178 -}
   1.179 -
   1.180  
   1.181  # components
   1.182  
   1.183  ISABELLE_COMPONENTS=""
   1.184  ISABELLE_COMPONENTS_MISSING=""
   1.185  
   1.186 -#init component tree
   1.187 -function init_component ()
   1.188 -{
   1.189 -  local COMPONENT="$1"
   1.190 -  case "$COMPONENT" in
   1.191 -    /*) ;;
   1.192 -    *)
   1.193 -      echo >&2 "Absolute component path required: \"$COMPONENT\""
   1.194 -      exit 2
   1.195 -      ;;
   1.196 -  esac
   1.197 -
   1.198 -  if [ -d "$COMPONENT" ]; then
   1.199 -    if [ -z "$ISABELLE_COMPONENTS" ]; then
   1.200 -      ISABELLE_COMPONENTS="$COMPONENT"
   1.201 -    else
   1.202 -      ISABELLE_COMPONENTS="$ISABELLE_COMPONENTS:$COMPONENT"
   1.203 -    fi
   1.204 -  else
   1.205 -    echo >&2 "### Missing Isabelle component: \"$COMPONENT\""
   1.206 -    if [ -z "$ISABELLE_COMPONENTS_MISSING" ]; then
   1.207 -      ISABELLE_COMPONENTS_MISSING="$COMPONENT"
   1.208 -    else
   1.209 -      ISABELLE_COMPONENTS_MISSING="$ISABELLE_COMPONENTS_MISSING:$COMPONENT"
   1.210 -    fi
   1.211 -  fi
   1.212 -
   1.213 -  if [ -f "$COMPONENT/etc/settings" ]; then
   1.214 -    source "$COMPONENT/etc/settings"
   1.215 -    local RC="$?"
   1.216 -    if [ "$RC" -ne 0 ]; then
   1.217 -      echo >&2 "Return code $RC from bash script: \"$COMPONENT/etc/settings\""
   1.218 -      exit 2
   1.219 -    fi
   1.220 -  fi
   1.221 -  if [ -f "$COMPONENT/etc/components" ]; then
   1.222 -    init_components "$COMPONENT" "$COMPONENT/etc/components"
   1.223 -  fi
   1.224 -}
   1.225 -
   1.226 -#init component forest
   1.227 -function init_components ()
   1.228 -{
   1.229 -  local BASE="$1"
   1.230 -  local CATALOG="$2"
   1.231 -  local COMPONENT=""
   1.232 -  local -a COMPONENTS=()
   1.233 -
   1.234 -  if [ ! -f "$CATALOG" ]; then
   1.235 -    echo >&2 "Bad component catalog file: \"$CATALOG\""
   1.236 -    exit 2
   1.237 -  fi
   1.238 -
   1.239 -  {
   1.240 -    while { unset REPLY; read -r; test "$?" = 0 -o -n "$REPLY"; }
   1.241 -    do
   1.242 -      case "$REPLY" in
   1.243 -        \#* | "") ;;
   1.244 -        /*) COMPONENTS["${#COMPONENTS[@]}"]="$REPLY" ;;
   1.245 -        *) COMPONENTS["${#COMPONENTS[@]}"]="$BASE/$REPLY" ;;
   1.246 -      esac
   1.247 -    done
   1.248 -  } < "$CATALOG"
   1.249 -
   1.250 -  for COMPONENT in "${COMPONENTS[@]}"
   1.251 -  do
   1.252 -    init_component "$COMPONENT"
   1.253 -  done
   1.254 -}
   1.255 -
   1.256  #main components
   1.257  init_component "$ISABELLE_HOME"
   1.258  [ -d "$ISABELLE_HOME/Admin" ] && init_component "$ISABELLE_HOME/Admin"