lib/scripts/getsettings
changeset 62412 ffdc5cf36dc5
parent 62354 fdd6989cc8a0
child 62413 c6111df4a4f8
equal deleted inserted replaced
62409:e391528eff3b 62412:ffdc5cf36dc5
     1 # -*- shell-script -*- :mode=shellscript:
     1 # -*- shell-script -*- :mode=shellscript:
     2 #
     2 #
     3 # Author: Markus Wenzel, TU Muenchen
     3 # Author: Makarius
     4 #
     4 #
     5 # getsettings - bash source script to augment current env.
     5 # Static Isabelle environment for root of process tree.
     6 
     6 
     7 if [ -z "$ISABELLE_SETTINGS_PRESENT" ]
     7 if [ -z "$ISABELLE_SETTINGS_PRESENT" ]
     8 then
     8 then
     9 
     9 
    10 set -o allexport
    10 set -o allexport
    11 
    11 
    12 ISABELLE_SETTINGS_PRESENT=true
    12 ISABELLE_SETTINGS_PRESENT=true
    13 
    13 
    14 #GNU tar (notably on Mac OS X)
    14 BASH_ENV="$ISABELLE_HOME/lib/scripts/getfunctions"
    15 if [ -x /usr/bin/gnutar ]; then
    15 source "$BASH_ENV"
    16   function tar() { /usr/bin/gnutar "$@"; }
    16 set -o allexport
    17 fi
       
    18 
    17 
    19 #sane environment defaults (notably on Mac OS X)
    18 #sane environment defaults (notably on Mac OS X)
    20 if [ "$ISABELLE_APP" = true -a -x /usr/libexec/path_helper ]; then
    19 if [ "$ISABELLE_APP" = true -a -x /usr/libexec/path_helper ]; then
    21   eval $(/usr/libexec/path_helper -s)
    20   eval $(/usr/libexec/path_helper -s)
    22 fi
    21 fi
    34 
    33 
    35   if [ -z "$USER_HOME" ]; then
    34   if [ -z "$USER_HOME" ]; then
    36     USER_HOME="$(cygpath -u "$USERPROFILE")"
    35     USER_HOME="$(cygpath -u "$USERPROFILE")"
    37   fi
    36   fi
    38 
    37 
    39   function platform_path() { cygpath -i -C UTF8 -w -p "$@"; }
       
    40   CYGWIN_ROOT="$(platform_path "/")"
    38   CYGWIN_ROOT="$(platform_path "/")"
    41   ISABELLE_ROOT="$(platform_path "$ISABELLE_HOME")"
    39   ISABELLE_ROOT="$(platform_path "$ISABELLE_HOME")"
    42 
    40 
    43   ISABELLE_CLASSPATH="$(cygpath -i -u -p "$CLASSPATH")"
    41   ISABELLE_CLASSPATH="$(cygpath -i -u -p "$CLASSPATH")"
    44   unset CLASSPATH
    42   unset CLASSPATH
    47     USER_HOME="$HOME"
    45     USER_HOME="$HOME"
    48   fi
    46   fi
    49 
    47 
    50   ISABELLE_ROOT="$ISABELLE_HOME"
    48   ISABELLE_ROOT="$ISABELLE_HOME"
    51 
    49 
    52   function platform_path() { echo "$@"; }
       
    53 
       
    54   ISABELLE_CLASSPATH="$CLASSPATH"
    50   ISABELLE_CLASSPATH="$CLASSPATH"
    55   unset CLASSPATH
    51   unset CLASSPATH
    56 fi
    52 fi
    57 
    53 
    58 export ISABELLE_HOME
    54 export ISABELLE_HOME
    59 
    55 
    60 #key executables
    56 #main executables
    61 ISABELLE_TOOL="$ISABELLE_HOME/bin/isabelle"
    57 ISABELLE_TOOL="$ISABELLE_HOME/bin/isabelle"
    62 ISABELLE_PROCESS="$ISABELLE_HOME/bin/isabelle_process"
    58 ISABELLE_PROCESS="$ISABELLE_HOME/bin/isabelle_process"
    63 ISABELLE_SCALA_SCRIPT="$ISABELLE_HOME/bin/isabelle_scala_script"
    59 ISABELLE_SCALA_SCRIPT="$ISABELLE_HOME/bin/isabelle_scala_script"
    64 
       
    65 function isabelle ()
       
    66 {
       
    67   "$ISABELLE_TOOL" "$@"
       
    68 }
       
    69 
       
    70 function isabelle_process ()
       
    71 {
       
    72   "$ISABELLE_PROCESS" "$@"
       
    73 }
       
    74 
       
    75 function isabelle_scala_script ()
       
    76 {
       
    77   "$ISABELLE_SCALA_SCRIPT" "$@"
       
    78 }
       
    79 
    60 
    80 #platform
    61 #platform
    81 source "$ISABELLE_HOME/lib/scripts/isabelle-platform"
    62 source "$ISABELLE_HOME/lib/scripts/isabelle-platform"
    82 if [ -z "$ISABELLE_PLATFORM" ]; then
    63 if [ -z "$ISABELLE_PLATFORM" ]; then
    83   echo 1>&2 "Failed to determine hardware and operating system type!"
    64   echo 1>&2 "Failed to determine hardware and operating system type!"
    86 
    67 
    87 #Isabelle distribution identifier -- filled in automatically!
    68 #Isabelle distribution identifier -- filled in automatically!
    88 ISABELLE_ID=""
    69 ISABELLE_ID=""
    89 [ -z "$ISABELLE_IDENTIFIER" ] && ISABELLE_IDENTIFIER=""
    70 [ -z "$ISABELLE_IDENTIFIER" ] && ISABELLE_IDENTIFIER=""
    90 
    71 
    91 #sometimes users put strange things in here ...
       
    92 unset ENV
       
    93 unset BASH_ENV
       
    94 
       
    95 #shared library convenience
       
    96 function librarypath ()
       
    97 {
       
    98   for X in "$@"
       
    99   do
       
   100     case "$ISABELLE_PLATFORM" in
       
   101       *-darwin)
       
   102         if [ -z "$DYLD_LIBRARY_PATH" ]; then
       
   103           DYLD_LIBRARY_PATH="$X"
       
   104         else
       
   105           DYLD_LIBRARY_PATH="$X:$DYLD_LIBRARY_PATH"
       
   106         fi
       
   107         export DYLD_LIBRARY_PATH
       
   108         ;;
       
   109       *)
       
   110         if [ -z "$LD_LIBRARY_PATH" ]; then
       
   111           LD_LIBRARY_PATH="$X"
       
   112         else
       
   113           LD_LIBRARY_PATH="$X:$LD_LIBRARY_PATH"
       
   114         fi
       
   115         export LD_LIBRARY_PATH
       
   116         ;;
       
   117     esac
       
   118   done
       
   119 }
       
   120 
       
   121 #robust invocation via ISABELLE_JDK_HOME
       
   122 function isabelle_jdk ()
       
   123 {
       
   124   if [ -z "$ISABELLE_JDK_HOME" ]; then
       
   125     echo "Unknown ISABELLE_JDK_HOME -- Java development tools unavailable" >&2
       
   126     return 127
       
   127   else
       
   128     local PRG="$1"; shift
       
   129     "$ISABELLE_JDK_HOME/bin/$PRG" "$@"
       
   130   fi
       
   131 }
       
   132 
       
   133 #robust invocation via JAVA_HOME
       
   134 function isabelle_java ()
       
   135 {
       
   136   if [ -z "$JAVA_HOME" ]; then
       
   137     echo "Unknown JAVA_HOME -- Java unavailable" >&2
       
   138     return 127
       
   139   else
       
   140     local PRG="$1"; shift
       
   141     "$JAVA_HOME/bin/$PRG" "$@"
       
   142   fi
       
   143 }
       
   144 
       
   145 #robust invocation via SCALA_HOME
       
   146 function isabelle_scala ()
       
   147 {
       
   148   if [ -z "$JAVA_HOME" ]; then
       
   149     echo "Unknown JAVA_HOME -- Java unavailable" >&2
       
   150     return 127
       
   151   elif [ -z "$SCALA_HOME" ]; then
       
   152     echo "Unknown SCALA_HOME -- Scala unavailable" >&2
       
   153     return 127
       
   154   else
       
   155     local PRG="$1"; shift
       
   156     "$SCALA_HOME/bin/$PRG" "$@"
       
   157   fi
       
   158 }
       
   159 
       
   160 #administrative build
       
   161 if [ -e "$ISABELLE_HOME/Admin/build" ]; then
       
   162   function isabelle_admin_build ()
       
   163   {
       
   164     "$ISABELLE_HOME/Admin/build" "$@"
       
   165   }
       
   166 else
       
   167   function isabelle_admin_build () { return 0; }
       
   168 fi
       
   169 
       
   170 #classpath
       
   171 function classpath ()
       
   172 {
       
   173   for X in "$@"
       
   174   do
       
   175     if [ -z "$ISABELLE_CLASSPATH" ]; then
       
   176       ISABELLE_CLASSPATH="$X"
       
   177     else
       
   178       ISABELLE_CLASSPATH="$ISABELLE_CLASSPATH:$X"
       
   179     fi
       
   180   done
       
   181   export ISABELLE_CLASSPATH
       
   182 }
       
   183 
       
   184 #arrays
       
   185 function splitarray ()
       
   186 {
       
   187   SPLITARRAY=()
       
   188   local IFS="$1"; shift
       
   189   for X in $*
       
   190   do
       
   191     SPLITARRAY["${#SPLITARRAY[@]}"]="$X"
       
   192   done
       
   193 }
       
   194 
       
   195 
    72 
   196 # components
    73 # components
   197 
    74 
   198 ISABELLE_COMPONENTS=""
    75 ISABELLE_COMPONENTS=""
   199 ISABELLE_COMPONENTS_MISSING=""
    76 ISABELLE_COMPONENTS_MISSING=""
   200 
       
   201 #init component tree
       
   202 function init_component ()
       
   203 {
       
   204   local COMPONENT="$1"
       
   205   case "$COMPONENT" in
       
   206     /*) ;;
       
   207     *)
       
   208       echo >&2 "Absolute component path required: \"$COMPONENT\""
       
   209       exit 2
       
   210       ;;
       
   211   esac
       
   212 
       
   213   if [ -d "$COMPONENT" ]; then
       
   214     if [ -z "$ISABELLE_COMPONENTS" ]; then
       
   215       ISABELLE_COMPONENTS="$COMPONENT"
       
   216     else
       
   217       ISABELLE_COMPONENTS="$ISABELLE_COMPONENTS:$COMPONENT"
       
   218     fi
       
   219   else
       
   220     echo >&2 "### Missing Isabelle component: \"$COMPONENT\""
       
   221     if [ -z "$ISABELLE_COMPONENTS_MISSING" ]; then
       
   222       ISABELLE_COMPONENTS_MISSING="$COMPONENT"
       
   223     else
       
   224       ISABELLE_COMPONENTS_MISSING="$ISABELLE_COMPONENTS_MISSING:$COMPONENT"
       
   225     fi
       
   226   fi
       
   227 
       
   228   if [ -f "$COMPONENT/etc/settings" ]; then
       
   229     source "$COMPONENT/etc/settings"
       
   230     local RC="$?"
       
   231     if [ "$RC" -ne 0 ]; then
       
   232       echo >&2 "Return code $RC from bash script: \"$COMPONENT/etc/settings\""
       
   233       exit 2
       
   234     fi
       
   235   fi
       
   236   if [ -f "$COMPONENT/etc/components" ]; then
       
   237     init_components "$COMPONENT" "$COMPONENT/etc/components"
       
   238   fi
       
   239 }
       
   240 
       
   241 #init component forest
       
   242 function init_components ()
       
   243 {
       
   244   local BASE="$1"
       
   245   local CATALOG="$2"
       
   246   local COMPONENT=""
       
   247   local -a COMPONENTS=()
       
   248 
       
   249   if [ ! -f "$CATALOG" ]; then
       
   250     echo >&2 "Bad component catalog file: \"$CATALOG\""
       
   251     exit 2
       
   252   fi
       
   253 
       
   254   {
       
   255     while { unset REPLY; read -r; test "$?" = 0 -o -n "$REPLY"; }
       
   256     do
       
   257       case "$REPLY" in
       
   258         \#* | "") ;;
       
   259         /*) COMPONENTS["${#COMPONENTS[@]}"]="$REPLY" ;;
       
   260         *) COMPONENTS["${#COMPONENTS[@]}"]="$BASE/$REPLY" ;;
       
   261       esac
       
   262     done
       
   263   } < "$CATALOG"
       
   264 
       
   265   for COMPONENT in "${COMPONENTS[@]}"
       
   266   do
       
   267     init_component "$COMPONENT"
       
   268   done
       
   269 }
       
   270 
    77 
   271 #main components
    78 #main components
   272 init_component "$ISABELLE_HOME"
    79 init_component "$ISABELLE_HOME"
   273 [ -d "$ISABELLE_HOME/Admin" ] && init_component "$ISABELLE_HOME/Admin"
    80 [ -d "$ISABELLE_HOME/Admin" ] && init_component "$ISABELLE_HOME/Admin"
   274 if [ -d "$ISABELLE_HOME_USER" ]; then
    81 if [ -d "$ISABELLE_HOME_USER" ]; then