lib/scripts/getfunctions
author wenzelm
Wed Nov 01 17:29:14 2017 +0100 (19 months ago)
changeset 66980 8947cf58cb86
parent 66667 2e580fcf6522
child 69134 a142ec271d83
permissions -rw-r--r--
tuned output;
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@66667
    73
  local X=""
wenzelm@62412
    74
  for X in "$@"
wenzelm@62412
    75
  do
wenzelm@62412
    76
    if [ -z "$ISABELLE_CLASSPATH" ]; then
wenzelm@62412
    77
      ISABELLE_CLASSPATH="$X"
wenzelm@62412
    78
    else
wenzelm@62412
    79
      ISABELLE_CLASSPATH="$ISABELLE_CLASSPATH:$X"
wenzelm@62412
    80
    fi
wenzelm@62412
    81
  done
wenzelm@62412
    82
  export ISABELLE_CLASSPATH
wenzelm@62412
    83
}
wenzelm@62413
    84
export -f classpath
wenzelm@62412
    85
wenzelm@62412
    86
#administrative build
wenzelm@62412
    87
if [ -e "$ISABELLE_HOME/Admin/build" ]; then
wenzelm@62412
    88
  function isabelle_admin_build ()
wenzelm@62412
    89
  {
wenzelm@62412
    90
    "$ISABELLE_HOME/Admin/build" "$@"
wenzelm@62412
    91
  }
wenzelm@62412
    92
else
wenzelm@62412
    93
  function isabelle_admin_build () { return 0; }
wenzelm@62412
    94
fi
wenzelm@62413
    95
export -f isabelle_admin_build
wenzelm@62412
    96
wenzelm@62412
    97
#arrays
wenzelm@62412
    98
function splitarray ()
wenzelm@62412
    99
{
wenzelm@62412
   100
  SPLITARRAY=()
wenzelm@62412
   101
  local IFS="$1"; shift
wenzelm@66667
   102
  local X=""
wenzelm@62412
   103
  for X in $*
wenzelm@62412
   104
  do
wenzelm@62412
   105
    SPLITARRAY["${#SPLITARRAY[@]}"]="$X"
wenzelm@62412
   106
  done
wenzelm@62412
   107
}
wenzelm@62413
   108
export -f splitarray
wenzelm@62412
   109
wenzelm@62412
   110
#init component tree
wenzelm@62412
   111
function init_component ()
wenzelm@62412
   112
{
wenzelm@62412
   113
  local COMPONENT="$1"
wenzelm@62412
   114
  case "$COMPONENT" in
wenzelm@62412
   115
    /*) ;;
wenzelm@62412
   116
    *)
wenzelm@62412
   117
      echo >&2 "Absolute component path required: \"$COMPONENT\""
wenzelm@62412
   118
      exit 2
wenzelm@62412
   119
      ;;
wenzelm@62412
   120
  esac
wenzelm@62412
   121
wenzelm@62412
   122
  if [ -d "$COMPONENT" ]; then
wenzelm@62412
   123
    if [ -z "$ISABELLE_COMPONENTS" ]; then
wenzelm@62412
   124
      ISABELLE_COMPONENTS="$COMPONENT"
wenzelm@62412
   125
    else
wenzelm@62412
   126
      ISABELLE_COMPONENTS="$ISABELLE_COMPONENTS:$COMPONENT"
wenzelm@62412
   127
    fi
wenzelm@62412
   128
  else
wenzelm@62412
   129
    echo >&2 "### Missing Isabelle component: \"$COMPONENT\""
wenzelm@62412
   130
    if [ -z "$ISABELLE_COMPONENTS_MISSING" ]; then
wenzelm@62412
   131
      ISABELLE_COMPONENTS_MISSING="$COMPONENT"
wenzelm@62412
   132
    else
wenzelm@62412
   133
      ISABELLE_COMPONENTS_MISSING="$ISABELLE_COMPONENTS_MISSING:$COMPONENT"
wenzelm@62412
   134
    fi
wenzelm@62412
   135
  fi
wenzelm@62412
   136
wenzelm@62412
   137
  if [ -f "$COMPONENT/etc/settings" ]; then
wenzelm@62412
   138
    source "$COMPONENT/etc/settings"
wenzelm@62412
   139
    local RC="$?"
wenzelm@62412
   140
    if [ "$RC" -ne 0 ]; then
wenzelm@62412
   141
      echo >&2 "Return code $RC from bash script: \"$COMPONENT/etc/settings\""
wenzelm@62412
   142
      exit 2
wenzelm@62412
   143
    fi
wenzelm@62412
   144
  fi
wenzelm@62412
   145
  if [ -f "$COMPONENT/etc/components" ]; then
wenzelm@62412
   146
    init_components "$COMPONENT" "$COMPONENT/etc/components"
wenzelm@62412
   147
  fi
wenzelm@62412
   148
}
wenzelm@62413
   149
export -f init_component
wenzelm@62412
   150
wenzelm@62412
   151
#init component forest
wenzelm@62412
   152
function init_components ()
wenzelm@62412
   153
{
wenzelm@66667
   154
  local REPLY=""
wenzelm@62412
   155
  local BASE="$1"
wenzelm@62412
   156
  local CATALOG="$2"
wenzelm@62412
   157
  local COMPONENT=""
wenzelm@62412
   158
  local -a COMPONENTS=()
wenzelm@62412
   159
wenzelm@62412
   160
  if [ ! -f "$CATALOG" ]; then
wenzelm@62412
   161
    echo >&2 "Bad component catalog file: \"$CATALOG\""
wenzelm@62412
   162
    exit 2
wenzelm@62412
   163
  fi
wenzelm@62412
   164
wenzelm@62412
   165
  {
wenzelm@62412
   166
    while { unset REPLY; read -r; test "$?" = 0 -o -n "$REPLY"; }
wenzelm@62412
   167
    do
wenzelm@62412
   168
      case "$REPLY" in
wenzelm@62412
   169
        \#* | "") ;;
wenzelm@62412
   170
        /*) COMPONENTS["${#COMPONENTS[@]}"]="$REPLY" ;;
wenzelm@62412
   171
        *) COMPONENTS["${#COMPONENTS[@]}"]="$BASE/$REPLY" ;;
wenzelm@62412
   172
      esac
wenzelm@62412
   173
    done
wenzelm@62412
   174
  } < "$CATALOG"
wenzelm@62412
   175
wenzelm@62412
   176
  for COMPONENT in "${COMPONENTS[@]}"
wenzelm@62412
   177
  do
wenzelm@62412
   178
    init_component "$COMPONENT"
wenzelm@62412
   179
  done
wenzelm@62412
   180
}
wenzelm@62413
   181
export -f init_components
wenzelm@62412
   182
wenzelm@62412
   183
fi