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