lib/scripts/getfunctions
author wenzelm
Sun Oct 02 15:35:56 2016 +0200 (2016-10-02)
changeset 63994 18cbe1b8d859
parent 62614 0a01bc7f0946
child 66667 2e580fcf6522
permissions -rw-r--r--
updated according to 85c83757788c;
     1 # -*- shell-script -*- :mode=shellscript:
     2 #
     3 # Author: Makarius
     4 #
     5 # Isabelle shell functions, with on-demand re-initialization for
     6 # non-interactive bash processess. NB: bash shell functions are not portable
     7 # and may be dropped by aggressively POSIX-conformant versions of /bin/sh.
     8 
     9 if type splitarray >/dev/null 2>/dev/null
    10 then
    11   :
    12 else
    13 
    14 if [ "$OSTYPE" = cygwin ]; then
    15   function platform_path() { cygpath -i -C UTF8 -w -p "$@"; }
    16 else
    17   function platform_path() { echo "$@"; }
    18 fi
    19 export -f platform_path
    20 
    21 #GNU tar (notably on Mac OS X)
    22 if type -p gnutar >/dev/null
    23 then
    24   function tar() { gnutar "$@"; }
    25   export -f tar
    26 fi
    27 
    28 #robust invocation via ISABELLE_JDK_HOME
    29 function isabelle_jdk ()
    30 {
    31   if [ -z "$ISABELLE_JDK_HOME" ]; then
    32     echo "Unknown ISABELLE_JDK_HOME -- Java development tools unavailable" >&2
    33     return 127
    34   else
    35     local PRG="$1"; shift
    36     "$ISABELLE_JDK_HOME/bin/$PRG" "$@"
    37   fi
    38 }
    39 export -f isabelle_jdk
    40 
    41 #robust invocation via JAVA_HOME
    42 function isabelle_java ()
    43 {
    44   if [ -z "$JAVA_HOME" ]; then
    45     echo "Unknown JAVA_HOME -- Java unavailable" >&2
    46     return 127
    47   else
    48     local PRG="$1"; shift
    49     "$JAVA_HOME/bin/$PRG" "$@"
    50   fi
    51 }
    52 export -f isabelle_java
    53 
    54 #robust invocation via SCALA_HOME
    55 function isabelle_scala ()
    56 {
    57   if [ -z "$JAVA_HOME" ]; then
    58     echo "Unknown JAVA_HOME -- Java unavailable" >&2
    59     return 127
    60   elif [ -z "$SCALA_HOME" ]; then
    61     echo "Unknown SCALA_HOME -- Scala unavailable" >&2
    62     return 127
    63   else
    64     local PRG="$1"; shift
    65     "$SCALA_HOME/bin/$PRG" "$@"
    66   fi
    67 }
    68 export -f isabelle_scala
    69 
    70 #classpath
    71 function classpath ()
    72 {
    73   for X in "$@"
    74   do
    75     if [ -z "$ISABELLE_CLASSPATH" ]; then
    76       ISABELLE_CLASSPATH="$X"
    77     else
    78       ISABELLE_CLASSPATH="$ISABELLE_CLASSPATH:$X"
    79     fi
    80   done
    81   export ISABELLE_CLASSPATH
    82 }
    83 export -f classpath
    84 
    85 #administrative build
    86 if [ -e "$ISABELLE_HOME/Admin/build" ]; then
    87   function isabelle_admin_build ()
    88   {
    89     "$ISABELLE_HOME/Admin/build" "$@"
    90   }
    91 else
    92   function isabelle_admin_build () { return 0; }
    93 fi
    94 export -f isabelle_admin_build
    95 
    96 #arrays
    97 function splitarray ()
    98 {
    99   SPLITARRAY=()
   100   local IFS="$1"; shift
   101   for X in $*
   102   do
   103     SPLITARRAY["${#SPLITARRAY[@]}"]="$X"
   104   done
   105 }
   106 export -f splitarray
   107 
   108 #init component tree
   109 function init_component ()
   110 {
   111   local COMPONENT="$1"
   112   case "$COMPONENT" in
   113     /*) ;;
   114     *)
   115       echo >&2 "Absolute component path required: \"$COMPONENT\""
   116       exit 2
   117       ;;
   118   esac
   119 
   120   if [ -d "$COMPONENT" ]; then
   121     if [ -z "$ISABELLE_COMPONENTS" ]; then
   122       ISABELLE_COMPONENTS="$COMPONENT"
   123     else
   124       ISABELLE_COMPONENTS="$ISABELLE_COMPONENTS:$COMPONENT"
   125     fi
   126   else
   127     echo >&2 "### Missing Isabelle component: \"$COMPONENT\""
   128     if [ -z "$ISABELLE_COMPONENTS_MISSING" ]; then
   129       ISABELLE_COMPONENTS_MISSING="$COMPONENT"
   130     else
   131       ISABELLE_COMPONENTS_MISSING="$ISABELLE_COMPONENTS_MISSING:$COMPONENT"
   132     fi
   133   fi
   134 
   135   if [ -f "$COMPONENT/etc/settings" ]; then
   136     source "$COMPONENT/etc/settings"
   137     local RC="$?"
   138     if [ "$RC" -ne 0 ]; then
   139       echo >&2 "Return code $RC from bash script: \"$COMPONENT/etc/settings\""
   140       exit 2
   141     fi
   142   fi
   143   if [ -f "$COMPONENT/etc/components" ]; then
   144     init_components "$COMPONENT" "$COMPONENT/etc/components"
   145   fi
   146 }
   147 export -f init_component
   148 
   149 #init component forest
   150 function init_components ()
   151 {
   152   local BASE="$1"
   153   local CATALOG="$2"
   154   local COMPONENT=""
   155   local -a COMPONENTS=()
   156 
   157   if [ ! -f "$CATALOG" ]; then
   158     echo >&2 "Bad component catalog file: \"$CATALOG\""
   159     exit 2
   160   fi
   161 
   162   {
   163     while { unset REPLY; read -r; test "$?" = 0 -o -n "$REPLY"; }
   164     do
   165       case "$REPLY" in
   166         \#* | "") ;;
   167         /*) COMPONENTS["${#COMPONENTS[@]}"]="$REPLY" ;;
   168         *) COMPONENTS["${#COMPONENTS[@]}"]="$BASE/$REPLY" ;;
   169       esac
   170     done
   171   } < "$CATALOG"
   172 
   173   for COMPONENT in "${COMPONENTS[@]}"
   174   do
   175     init_component "$COMPONENT"
   176   done
   177 }
   178 export -f init_components
   179 
   180 fi