lib/scripts/getfunctions
author wenzelm
Wed Oct 31 15:50:45 2018 +0100 (9 months ago)
changeset 69215 ab94035ba6ea
parent 69157 22ae1d926f96
child 69255 800b1ce96fce
permissions -rw-r--r--
tuned;
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@69157
    16
  function standard_path() { cygpath -i -u -p "$@" | tr -d '\r'; }
wenzelm@62412
    17
else
wenzelm@62412
    18
  function platform_path() { echo "$@"; }
wenzelm@69157
    19
  function standard_path() { echo "$@"; }
wenzelm@62412
    20
fi
wenzelm@69157
    21
export -f platform_path standard_path
wenzelm@62412
    22
wenzelm@62412
    23
#GNU tar (notably on Mac OS X)
wenzelm@63994
    24
if type -p gnutar >/dev/null
wenzelm@63994
    25
then
wenzelm@63994
    26
  function tar() { gnutar "$@"; }
wenzelm@62413
    27
  export -f tar
wenzelm@62412
    28
fi
wenzelm@62412
    29
wenzelm@69134
    30
#OCaml management via OPAM
wenzelm@69134
    31
function isabelle_opam()
wenzelm@69134
    32
{
wenzelm@69134
    33
  if [ -z "$ISABELLE_OPAM" ]; then
wenzelm@69134
    34
    echo "Unknown ISABELLE_OPAM -- OCaml management tools unavailable" >&2
wenzelm@69134
    35
    return 127
wenzelm@69134
    36
  else
wenzelm@69134
    37
    env OPAMROOT="$ISABELLE_OPAM_ROOT" "$ISABELLE_OPAM" "$@"
wenzelm@69134
    38
  fi
wenzelm@69134
    39
}
wenzelm@69134
    40
export -f isabelle_opam
wenzelm@69134
    41
wenzelm@69150
    42
#GHC management via Stack
wenzelm@69147
    43
function isabelle_stack()
wenzelm@69147
    44
{
wenzelm@69147
    45
  if [ -z "$ISABELLE_STACK" ]; then
wenzelm@69150
    46
    echo "Unknown ISABELLE_STACK -- GHC management tools unavailable" >&2
wenzelm@69147
    47
    return 127
wenzelm@69147
    48
  else
wenzelm@69147
    49
    env STACK_ROOT="$(platform_path "$ISABELLE_STACK_ROOT")" "$ISABELLE_STACK" "$@"
wenzelm@69147
    50
  fi
wenzelm@69147
    51
}
wenzelm@69147
    52
export -f isabelle_stack
wenzelm@69147
    53
wenzelm@62412
    54
#robust invocation via ISABELLE_JDK_HOME
wenzelm@62412
    55
function isabelle_jdk ()
wenzelm@62412
    56
{
wenzelm@62412
    57
  if [ -z "$ISABELLE_JDK_HOME" ]; then
wenzelm@62412
    58
    echo "Unknown ISABELLE_JDK_HOME -- Java development tools unavailable" >&2
wenzelm@62412
    59
    return 127
wenzelm@62412
    60
  else
wenzelm@62412
    61
    local PRG="$1"; shift
wenzelm@62412
    62
    "$ISABELLE_JDK_HOME/bin/$PRG" "$@"
wenzelm@62412
    63
  fi
wenzelm@62412
    64
}
wenzelm@62413
    65
export -f isabelle_jdk
wenzelm@62412
    66
wenzelm@62412
    67
#robust invocation via JAVA_HOME
wenzelm@62412
    68
function isabelle_java ()
wenzelm@62412
    69
{
wenzelm@62412
    70
  if [ -z "$JAVA_HOME" ]; then
wenzelm@62412
    71
    echo "Unknown JAVA_HOME -- Java unavailable" >&2
wenzelm@62412
    72
    return 127
wenzelm@62412
    73
  else
wenzelm@62412
    74
    local PRG="$1"; shift
wenzelm@62412
    75
    "$JAVA_HOME/bin/$PRG" "$@"
wenzelm@62412
    76
  fi
wenzelm@62412
    77
}
wenzelm@62413
    78
export -f isabelle_java
wenzelm@62412
    79
wenzelm@62412
    80
#robust invocation via SCALA_HOME
wenzelm@62412
    81
function isabelle_scala ()
wenzelm@62412
    82
{
wenzelm@62412
    83
  if [ -z "$JAVA_HOME" ]; then
wenzelm@62412
    84
    echo "Unknown JAVA_HOME -- Java unavailable" >&2
wenzelm@62412
    85
    return 127
wenzelm@62412
    86
  elif [ -z "$SCALA_HOME" ]; then
wenzelm@62412
    87
    echo "Unknown SCALA_HOME -- Scala unavailable" >&2
wenzelm@62412
    88
    return 127
wenzelm@62412
    89
  else
wenzelm@62412
    90
    local PRG="$1"; shift
wenzelm@62412
    91
    "$SCALA_HOME/bin/$PRG" "$@"
wenzelm@62412
    92
  fi
wenzelm@62412
    93
}
wenzelm@62413
    94
export -f isabelle_scala
wenzelm@62412
    95
wenzelm@62412
    96
#classpath
wenzelm@62412
    97
function classpath ()
wenzelm@62412
    98
{
wenzelm@66667
    99
  local X=""
wenzelm@62412
   100
  for X in "$@"
wenzelm@62412
   101
  do
wenzelm@62412
   102
    if [ -z "$ISABELLE_CLASSPATH" ]; then
wenzelm@62412
   103
      ISABELLE_CLASSPATH="$X"
wenzelm@62412
   104
    else
wenzelm@62412
   105
      ISABELLE_CLASSPATH="$ISABELLE_CLASSPATH:$X"
wenzelm@62412
   106
    fi
wenzelm@62412
   107
  done
wenzelm@62412
   108
  export ISABELLE_CLASSPATH
wenzelm@62412
   109
}
wenzelm@62413
   110
export -f classpath
wenzelm@62412
   111
wenzelm@62412
   112
#administrative build
wenzelm@62412
   113
if [ -e "$ISABELLE_HOME/Admin/build" ]; then
wenzelm@62412
   114
  function isabelle_admin_build ()
wenzelm@62412
   115
  {
wenzelm@62412
   116
    "$ISABELLE_HOME/Admin/build" "$@"
wenzelm@62412
   117
  }
wenzelm@62412
   118
else
wenzelm@62412
   119
  function isabelle_admin_build () { return 0; }
wenzelm@62412
   120
fi
wenzelm@62413
   121
export -f isabelle_admin_build
wenzelm@62412
   122
wenzelm@62412
   123
#arrays
wenzelm@62412
   124
function splitarray ()
wenzelm@62412
   125
{
wenzelm@62412
   126
  SPLITARRAY=()
wenzelm@62412
   127
  local IFS="$1"; shift
wenzelm@66667
   128
  local X=""
wenzelm@62412
   129
  for X in $*
wenzelm@62412
   130
  do
wenzelm@62412
   131
    SPLITARRAY["${#SPLITARRAY[@]}"]="$X"
wenzelm@62412
   132
  done
wenzelm@62412
   133
}
wenzelm@62413
   134
export -f splitarray
wenzelm@62412
   135
wenzelm@62412
   136
#init component tree
wenzelm@62412
   137
function init_component ()
wenzelm@62412
   138
{
wenzelm@62412
   139
  local COMPONENT="$1"
wenzelm@62412
   140
  case "$COMPONENT" in
wenzelm@62412
   141
    /*) ;;
wenzelm@62412
   142
    *)
wenzelm@62412
   143
      echo >&2 "Absolute component path required: \"$COMPONENT\""
wenzelm@62412
   144
      exit 2
wenzelm@62412
   145
      ;;
wenzelm@62412
   146
  esac
wenzelm@62412
   147
wenzelm@62412
   148
  if [ -d "$COMPONENT" ]; then
wenzelm@62412
   149
    if [ -z "$ISABELLE_COMPONENTS" ]; then
wenzelm@62412
   150
      ISABELLE_COMPONENTS="$COMPONENT"
wenzelm@62412
   151
    else
wenzelm@62412
   152
      ISABELLE_COMPONENTS="$ISABELLE_COMPONENTS:$COMPONENT"
wenzelm@62412
   153
    fi
wenzelm@62412
   154
  else
wenzelm@62412
   155
    echo >&2 "### Missing Isabelle component: \"$COMPONENT\""
wenzelm@62412
   156
    if [ -z "$ISABELLE_COMPONENTS_MISSING" ]; then
wenzelm@62412
   157
      ISABELLE_COMPONENTS_MISSING="$COMPONENT"
wenzelm@62412
   158
    else
wenzelm@62412
   159
      ISABELLE_COMPONENTS_MISSING="$ISABELLE_COMPONENTS_MISSING:$COMPONENT"
wenzelm@62412
   160
    fi
wenzelm@62412
   161
  fi
wenzelm@62412
   162
wenzelm@62412
   163
  if [ -f "$COMPONENT/etc/settings" ]; then
wenzelm@62412
   164
    source "$COMPONENT/etc/settings"
wenzelm@62412
   165
    local RC="$?"
wenzelm@62412
   166
    if [ "$RC" -ne 0 ]; then
wenzelm@62412
   167
      echo >&2 "Return code $RC from bash script: \"$COMPONENT/etc/settings\""
wenzelm@62412
   168
      exit 2
wenzelm@62412
   169
    fi
wenzelm@62412
   170
  fi
wenzelm@62412
   171
  if [ -f "$COMPONENT/etc/components" ]; then
wenzelm@62412
   172
    init_components "$COMPONENT" "$COMPONENT/etc/components"
wenzelm@62412
   173
  fi
wenzelm@62412
   174
}
wenzelm@62413
   175
export -f init_component
wenzelm@62412
   176
wenzelm@62412
   177
#init component forest
wenzelm@62412
   178
function init_components ()
wenzelm@62412
   179
{
wenzelm@66667
   180
  local REPLY=""
wenzelm@62412
   181
  local BASE="$1"
wenzelm@62412
   182
  local CATALOG="$2"
wenzelm@62412
   183
  local COMPONENT=""
wenzelm@62412
   184
  local -a COMPONENTS=()
wenzelm@62412
   185
wenzelm@62412
   186
  if [ ! -f "$CATALOG" ]; then
wenzelm@62412
   187
    echo >&2 "Bad component catalog file: \"$CATALOG\""
wenzelm@62412
   188
    exit 2
wenzelm@62412
   189
  fi
wenzelm@62412
   190
wenzelm@62412
   191
  {
wenzelm@62412
   192
    while { unset REPLY; read -r; test "$?" = 0 -o -n "$REPLY"; }
wenzelm@62412
   193
    do
wenzelm@62412
   194
      case "$REPLY" in
wenzelm@62412
   195
        \#* | "") ;;
wenzelm@62412
   196
        /*) COMPONENTS["${#COMPONENTS[@]}"]="$REPLY" ;;
wenzelm@62412
   197
        *) COMPONENTS["${#COMPONENTS[@]}"]="$BASE/$REPLY" ;;
wenzelm@62412
   198
      esac
wenzelm@62412
   199
    done
wenzelm@62412
   200
  } < "$CATALOG"
wenzelm@62412
   201
wenzelm@62412
   202
  for COMPONENT in "${COMPONENTS[@]}"
wenzelm@62412
   203
  do
wenzelm@62412
   204
    init_component "$COMPONENT"
wenzelm@62412
   205
  done
wenzelm@62412
   206
}
wenzelm@62413
   207
export -f init_components
wenzelm@62412
   208
wenzelm@62412
   209
fi