lib/scripts/getfunctions
author wenzelm
Wed, 31 Mar 2021 11:24:46 +0200
changeset 73772 d3f2038198ae
parent 73768 b7bb665fe850
child 73835 8ddf6728ad80
permissions -rw-r--r--
clarified (again): local tip could be actually more recent;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
62413
ffdc5cf36dc5 more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff changeset
     1
# -*- shell-script -*- :mode=shellscript:
ffdc5cf36dc5 more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff changeset
     2
#
ffdc5cf36dc5 more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff changeset
     3
# Author: Makarius
ffdc5cf36dc5 more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff changeset
     4
#
ffdc5cf36dc5 more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff changeset
     5
# Isabelle shell functions, with on-demand re-initialization for
ffdc5cf36dc5 more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff changeset
     6
# non-interactive bash processess. NB: bash shell functions are not portable
ffdc5cf36dc5 more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff changeset
     7
# and may be dropped by aggressively POSIX-conformant versions of /bin/sh.
ffdc5cf36dc5 more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff changeset
     8
62417
cb6c4e307b1c slightly more robust re-initialization;
wenzelm
parents: 62415
diff changeset
     9
if type splitarray >/dev/null 2>/dev/null
62413
ffdc5cf36dc5 more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff changeset
    10
then
ffdc5cf36dc5 more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff changeset
    11
  :
ffdc5cf36dc5 more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff changeset
    12
else
ffdc5cf36dc5 more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff changeset
    13
ffdc5cf36dc5 more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff changeset
    14
if [ "$OSTYPE" = cygwin ]; then
ffdc5cf36dc5 more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff changeset
    15
  function platform_path() { cygpath -i -C UTF8 -w -p "$@"; }
69157
22ae1d926f96 more portable;
wenzelm
parents: 69150
diff changeset
    16
  function standard_path() { cygpath -i -u -p "$@" | tr -d '\r'; }
62413
ffdc5cf36dc5 more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff changeset
    17
else
ffdc5cf36dc5 more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff changeset
    18
  function platform_path() { echo "$@"; }
69157
22ae1d926f96 more portable;
wenzelm
parents: 69150
diff changeset
    19
  function standard_path() { echo "$@"; }
62413
ffdc5cf36dc5 more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff changeset
    20
fi
69157
22ae1d926f96 more portable;
wenzelm
parents: 69150
diff changeset
    21
export -f platform_path standard_path
62413
ffdc5cf36dc5 more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff changeset
    22
73131
bd2269b6cd99 updated "macOS" terminology: current Big Sur is already version 11;
wenzelm
parents: 72698
diff changeset
    23
#GNU tar (notably on macOS)
63994
18cbe1b8d859 updated according to 85c83757788c;
wenzelm
parents: 62614
diff changeset
    24
if type -p gnutar >/dev/null
18cbe1b8d859 updated according to 85c83757788c;
wenzelm
parents: 62614
diff changeset
    25
then
18cbe1b8d859 updated according to 85c83757788c;
wenzelm
parents: 62614
diff changeset
    26
  function tar() { gnutar "$@"; }
62414
c6111df4a4f8 avoid global state change;
wenzelm
parents: 62413
diff changeset
    27
  export -f tar
69417
7742cace5dd9 more robust: "gtar" is default name in Homebrew;
wenzelm
parents: 69384
diff changeset
    28
elif type -p gtar >/dev/null
7742cace5dd9 more robust: "gtar" is default name in Homebrew;
wenzelm
parents: 69384
diff changeset
    29
then
7742cace5dd9 more robust: "gtar" is default name in Homebrew;
wenzelm
parents: 69384
diff changeset
    30
  function tar() { gtar "$@"; }
7742cace5dd9 more robust: "gtar" is default name in Homebrew;
wenzelm
parents: 69384
diff changeset
    31
  export -f tar
62413
ffdc5cf36dc5 more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff changeset
    32
fi
ffdc5cf36dc5 more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff changeset
    33
69134
a142ec271d83 isabelle_opam as portable shell function;
wenzelm
parents: 66669
diff changeset
    34
#OCaml management via OPAM
73755
a33e5298aee6 tuned whitespace;
wenzelm
parents: 73131
diff changeset
    35
function isabelle_opam ()
69134
a142ec271d83 isabelle_opam as portable shell function;
wenzelm
parents: 66669
diff changeset
    36
{
a142ec271d83 isabelle_opam as portable shell function;
wenzelm
parents: 66669
diff changeset
    37
  if [ -z "$ISABELLE_OPAM" ]; then
a142ec271d83 isabelle_opam as portable shell function;
wenzelm
parents: 66669
diff changeset
    38
    echo "Unknown ISABELLE_OPAM -- OCaml management tools unavailable" >&2
a142ec271d83 isabelle_opam as portable shell function;
wenzelm
parents: 66669
diff changeset
    39
    return 127
a142ec271d83 isabelle_opam as portable shell function;
wenzelm
parents: 66669
diff changeset
    40
  else
72698
de11c745ebbc tuned messages --- less SPAM;
wenzelm
parents: 72395
diff changeset
    41
    env OPAMROOT="$ISABELLE_OPAM_ROOT" OPAMCOLOR="never" "$ISABELLE_OPAM" "$@"
69134
a142ec271d83 isabelle_opam as portable shell function;
wenzelm
parents: 66669
diff changeset
    42
  fi
a142ec271d83 isabelle_opam as portable shell function;
wenzelm
parents: 66669
diff changeset
    43
}
a142ec271d83 isabelle_opam as portable shell function;
wenzelm
parents: 66669
diff changeset
    44
export -f isabelle_opam
a142ec271d83 isabelle_opam as portable shell function;
wenzelm
parents: 66669
diff changeset
    45
69150
wenzelm
parents: 69147
diff changeset
    46
#GHC management via Stack
73755
a33e5298aee6 tuned whitespace;
wenzelm
parents: 73131
diff changeset
    47
function isabelle_stack ()
69147
6f4d561ea621 isabelle_stack as portable shell function;
wenzelm
parents: 69134
diff changeset
    48
{
6f4d561ea621 isabelle_stack as portable shell function;
wenzelm
parents: 69134
diff changeset
    49
  if [ -z "$ISABELLE_STACK" ]; then
69150
wenzelm
parents: 69147
diff changeset
    50
    echo "Unknown ISABELLE_STACK -- GHC management tools unavailable" >&2
69147
6f4d561ea621 isabelle_stack as portable shell function;
wenzelm
parents: 69134
diff changeset
    51
    return 127
6f4d561ea621 isabelle_stack as portable shell function;
wenzelm
parents: 69134
diff changeset
    52
  else
69272
517655a528fe always insist in specified resolver/compiler version;
wenzelm
parents: 69260
diff changeset
    53
    env STACK_ROOT="$(platform_path "$ISABELLE_STACK_ROOT")" "$ISABELLE_STACK" --resolver "$ISABELLE_STACK_RESOLVER" --compiler "$ISABELLE_GHC_VERSION" "$@"
69147
6f4d561ea621 isabelle_stack as portable shell function;
wenzelm
parents: 69134
diff changeset
    54
  fi
6f4d561ea621 isabelle_stack as portable shell function;
wenzelm
parents: 69134
diff changeset
    55
}
6f4d561ea621 isabelle_stack as portable shell function;
wenzelm
parents: 69134
diff changeset
    56
export -f isabelle_stack
6f4d561ea621 isabelle_stack as portable shell function;
wenzelm
parents: 69134
diff changeset
    57
62413
ffdc5cf36dc5 more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff changeset
    58
#robust invocation via ISABELLE_JDK_HOME
ffdc5cf36dc5 more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff changeset
    59
function isabelle_jdk ()
ffdc5cf36dc5 more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff changeset
    60
{
ffdc5cf36dc5 more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff changeset
    61
  if [ -z "$ISABELLE_JDK_HOME" ]; then
ffdc5cf36dc5 more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff changeset
    62
    echo "Unknown ISABELLE_JDK_HOME -- Java development tools unavailable" >&2
ffdc5cf36dc5 more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff changeset
    63
    return 127
ffdc5cf36dc5 more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff changeset
    64
  else
ffdc5cf36dc5 more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff changeset
    65
    local PRG="$1"; shift
ffdc5cf36dc5 more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff changeset
    66
    "$ISABELLE_JDK_HOME/bin/$PRG" "$@"
ffdc5cf36dc5 more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff changeset
    67
  fi
ffdc5cf36dc5 more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff changeset
    68
}
62414
c6111df4a4f8 avoid global state change;
wenzelm
parents: 62413
diff changeset
    69
export -f isabelle_jdk
62413
ffdc5cf36dc5 more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff changeset
    70
ffdc5cf36dc5 more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff changeset
    71
#robust invocation via JAVA_HOME
ffdc5cf36dc5 more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff changeset
    72
function isabelle_java ()
ffdc5cf36dc5 more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff changeset
    73
{
ffdc5cf36dc5 more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff changeset
    74
  if [ -z "$JAVA_HOME" ]; then
ffdc5cf36dc5 more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff changeset
    75
    echo "Unknown JAVA_HOME -- Java unavailable" >&2
ffdc5cf36dc5 more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff changeset
    76
    return 127
ffdc5cf36dc5 more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff changeset
    77
  else
ffdc5cf36dc5 more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff changeset
    78
    local PRG="$1"; shift
ffdc5cf36dc5 more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff changeset
    79
    "$JAVA_HOME/bin/$PRG" "$@"
ffdc5cf36dc5 more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff changeset
    80
  fi
ffdc5cf36dc5 more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff changeset
    81
}
62414
c6111df4a4f8 avoid global state change;
wenzelm
parents: 62413
diff changeset
    82
export -f isabelle_java
62413
ffdc5cf36dc5 more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff changeset
    83
ffdc5cf36dc5 more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff changeset
    84
#robust invocation via SCALA_HOME
ffdc5cf36dc5 more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff changeset
    85
function isabelle_scala ()
ffdc5cf36dc5 more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff changeset
    86
{
ffdc5cf36dc5 more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff changeset
    87
  if [ -z "$JAVA_HOME" ]; then
ffdc5cf36dc5 more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff changeset
    88
    echo "Unknown JAVA_HOME -- Java unavailable" >&2
ffdc5cf36dc5 more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff changeset
    89
    return 127
ffdc5cf36dc5 more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff changeset
    90
  elif [ -z "$SCALA_HOME" ]; then
ffdc5cf36dc5 more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff changeset
    91
    echo "Unknown SCALA_HOME -- Scala unavailable" >&2
ffdc5cf36dc5 more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff changeset
    92
    return 127
ffdc5cf36dc5 more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff changeset
    93
  else
ffdc5cf36dc5 more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff changeset
    94
    local PRG="$1"; shift
ffdc5cf36dc5 more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff changeset
    95
    "$SCALA_HOME/bin/$PRG" "$@"
ffdc5cf36dc5 more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff changeset
    96
  fi
ffdc5cf36dc5 more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff changeset
    97
}
62414
c6111df4a4f8 avoid global state change;
wenzelm
parents: 62413
diff changeset
    98
export -f isabelle_scala
62413
ffdc5cf36dc5 more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff changeset
    99
ffdc5cf36dc5 more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff changeset
   100
#classpath
ffdc5cf36dc5 more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff changeset
   101
function classpath ()
ffdc5cf36dc5 more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff changeset
   102
{
66669
2e580fcf6522 avoid local shell variables intruding the resulting environment (via "set -o allexport" in getsettings);
wenzelm
parents: 63994
diff changeset
   103
  local X=""
62413
ffdc5cf36dc5 more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff changeset
   104
  for X in "$@"
ffdc5cf36dc5 more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff changeset
   105
  do
ffdc5cf36dc5 more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff changeset
   106
    if [ -z "$ISABELLE_CLASSPATH" ]; then
ffdc5cf36dc5 more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff changeset
   107
      ISABELLE_CLASSPATH="$X"
ffdc5cf36dc5 more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff changeset
   108
    else
ffdc5cf36dc5 more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff changeset
   109
      ISABELLE_CLASSPATH="$ISABELLE_CLASSPATH:$X"
ffdc5cf36dc5 more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff changeset
   110
    fi
ffdc5cf36dc5 more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff changeset
   111
  done
ffdc5cf36dc5 more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff changeset
   112
  export ISABELLE_CLASSPATH
ffdc5cf36dc5 more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff changeset
   113
}
62414
c6111df4a4f8 avoid global state change;
wenzelm
parents: 62413
diff changeset
   114
export -f classpath
62413
ffdc5cf36dc5 more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff changeset
   115
73768
b7bb665fe850 more systematic java_library: avoid empty entries, declaration order as for other bash functions;
wenzelm
parents: 73755
diff changeset
   116
#java_library
b7bb665fe850 more systematic java_library: avoid empty entries, declaration order as for other bash functions;
wenzelm
parents: 73755
diff changeset
   117
function java_library ()
b7bb665fe850 more systematic java_library: avoid empty entries, declaration order as for other bash functions;
wenzelm
parents: 73755
diff changeset
   118
{
b7bb665fe850 more systematic java_library: avoid empty entries, declaration order as for other bash functions;
wenzelm
parents: 73755
diff changeset
   119
  local X=""
b7bb665fe850 more systematic java_library: avoid empty entries, declaration order as for other bash functions;
wenzelm
parents: 73755
diff changeset
   120
  for X in "$@"
b7bb665fe850 more systematic java_library: avoid empty entries, declaration order as for other bash functions;
wenzelm
parents: 73755
diff changeset
   121
  do
b7bb665fe850 more systematic java_library: avoid empty entries, declaration order as for other bash functions;
wenzelm
parents: 73755
diff changeset
   122
    case "$ISABELLE_PLATFORM_FAMILY" in
b7bb665fe850 more systematic java_library: avoid empty entries, declaration order as for other bash functions;
wenzelm
parents: 73755
diff changeset
   123
      linux)
b7bb665fe850 more systematic java_library: avoid empty entries, declaration order as for other bash functions;
wenzelm
parents: 73755
diff changeset
   124
        if [ -z "$LD_LIBRARY_PATH" ]; then
b7bb665fe850 more systematic java_library: avoid empty entries, declaration order as for other bash functions;
wenzelm
parents: 73755
diff changeset
   125
          export LD_LIBRARY_PATH="$X"
b7bb665fe850 more systematic java_library: avoid empty entries, declaration order as for other bash functions;
wenzelm
parents: 73755
diff changeset
   126
        else
b7bb665fe850 more systematic java_library: avoid empty entries, declaration order as for other bash functions;
wenzelm
parents: 73755
diff changeset
   127
          export LD_LIBRARY_PATH="$LD_LIBRARY_PATH:$X"
b7bb665fe850 more systematic java_library: avoid empty entries, declaration order as for other bash functions;
wenzelm
parents: 73755
diff changeset
   128
        fi
b7bb665fe850 more systematic java_library: avoid empty entries, declaration order as for other bash functions;
wenzelm
parents: 73755
diff changeset
   129
        ;;
b7bb665fe850 more systematic java_library: avoid empty entries, declaration order as for other bash functions;
wenzelm
parents: 73755
diff changeset
   130
      macos)
b7bb665fe850 more systematic java_library: avoid empty entries, declaration order as for other bash functions;
wenzelm
parents: 73755
diff changeset
   131
        if [ -z "$JAVA_LIBRARY_PATH" ]; then
b7bb665fe850 more systematic java_library: avoid empty entries, declaration order as for other bash functions;
wenzelm
parents: 73755
diff changeset
   132
          export JAVA_LIBRARY_PATH="$X"
b7bb665fe850 more systematic java_library: avoid empty entries, declaration order as for other bash functions;
wenzelm
parents: 73755
diff changeset
   133
        else
b7bb665fe850 more systematic java_library: avoid empty entries, declaration order as for other bash functions;
wenzelm
parents: 73755
diff changeset
   134
          export JAVA_LIBRARY_PATH="$JAVA_LIBRARY_PATH:$X"
b7bb665fe850 more systematic java_library: avoid empty entries, declaration order as for other bash functions;
wenzelm
parents: 73755
diff changeset
   135
        fi
b7bb665fe850 more systematic java_library: avoid empty entries, declaration order as for other bash functions;
wenzelm
parents: 73755
diff changeset
   136
        ;;
b7bb665fe850 more systematic java_library: avoid empty entries, declaration order as for other bash functions;
wenzelm
parents: 73755
diff changeset
   137
      windows)
b7bb665fe850 more systematic java_library: avoid empty entries, declaration order as for other bash functions;
wenzelm
parents: 73755
diff changeset
   138
        if [ -z "$PATH" ]; then
b7bb665fe850 more systematic java_library: avoid empty entries, declaration order as for other bash functions;
wenzelm
parents: 73755
diff changeset
   139
          export PATH="$X"
b7bb665fe850 more systematic java_library: avoid empty entries, declaration order as for other bash functions;
wenzelm
parents: 73755
diff changeset
   140
        else
b7bb665fe850 more systematic java_library: avoid empty entries, declaration order as for other bash functions;
wenzelm
parents: 73755
diff changeset
   141
          export PATH="$PATH:$X"
b7bb665fe850 more systematic java_library: avoid empty entries, declaration order as for other bash functions;
wenzelm
parents: 73755
diff changeset
   142
        fi
b7bb665fe850 more systematic java_library: avoid empty entries, declaration order as for other bash functions;
wenzelm
parents: 73755
diff changeset
   143
        ;;
b7bb665fe850 more systematic java_library: avoid empty entries, declaration order as for other bash functions;
wenzelm
parents: 73755
diff changeset
   144
    esac
b7bb665fe850 more systematic java_library: avoid empty entries, declaration order as for other bash functions;
wenzelm
parents: 73755
diff changeset
   145
  done
b7bb665fe850 more systematic java_library: avoid empty entries, declaration order as for other bash functions;
wenzelm
parents: 73755
diff changeset
   146
  export ISABELLE_CLASSPATH
b7bb665fe850 more systematic java_library: avoid empty entries, declaration order as for other bash functions;
wenzelm
parents: 73755
diff changeset
   147
}
b7bb665fe850 more systematic java_library: avoid empty entries, declaration order as for other bash functions;
wenzelm
parents: 73755
diff changeset
   148
export -f java_library
b7bb665fe850 more systematic java_library: avoid empty entries, declaration order as for other bash functions;
wenzelm
parents: 73755
diff changeset
   149
69352
fa981730b964 more shell functions;
wenzelm
parents: 69282
diff changeset
   150
#Isabelle fonts
fa981730b964 more shell functions;
wenzelm
parents: 69282
diff changeset
   151
function isabelle_fonts ()
fa981730b964 more shell functions;
wenzelm
parents: 69282
diff changeset
   152
{
fa981730b964 more shell functions;
wenzelm
parents: 69282
diff changeset
   153
  local X=""
fa981730b964 more shell functions;
wenzelm
parents: 69282
diff changeset
   154
  for X in "$@"
fa981730b964 more shell functions;
wenzelm
parents: 69282
diff changeset
   155
  do
fa981730b964 more shell functions;
wenzelm
parents: 69282
diff changeset
   156
    if [ -z "$ISABELLE_FONTS" ]; then
fa981730b964 more shell functions;
wenzelm
parents: 69282
diff changeset
   157
      ISABELLE_FONTS="$X"
fa981730b964 more shell functions;
wenzelm
parents: 69282
diff changeset
   158
    else
fa981730b964 more shell functions;
wenzelm
parents: 69282
diff changeset
   159
      ISABELLE_FONTS="$ISABELLE_FONTS:$X"
fa981730b964 more shell functions;
wenzelm
parents: 69282
diff changeset
   160
    fi
fa981730b964 more shell functions;
wenzelm
parents: 69282
diff changeset
   161
  done
fa981730b964 more shell functions;
wenzelm
parents: 69282
diff changeset
   162
  export ISABELLE_FONTS
fa981730b964 more shell functions;
wenzelm
parents: 69282
diff changeset
   163
}
fa981730b964 more shell functions;
wenzelm
parents: 69282
diff changeset
   164
export -f isabelle_fonts
fa981730b964 more shell functions;
wenzelm
parents: 69282
diff changeset
   165
69384
ab66951166f3 clarified "hidden" terminology;
wenzelm
parents: 69352
diff changeset
   166
function isabelle_fonts_hidden ()
ab66951166f3 clarified "hidden" terminology;
wenzelm
parents: 69352
diff changeset
   167
{
ab66951166f3 clarified "hidden" terminology;
wenzelm
parents: 69352
diff changeset
   168
  local X=""
ab66951166f3 clarified "hidden" terminology;
wenzelm
parents: 69352
diff changeset
   169
  for X in "$@"
ab66951166f3 clarified "hidden" terminology;
wenzelm
parents: 69352
diff changeset
   170
  do
ab66951166f3 clarified "hidden" terminology;
wenzelm
parents: 69352
diff changeset
   171
    if [ -z "$ISABELLE_FONTS_HIDDEN" ]; then
ab66951166f3 clarified "hidden" terminology;
wenzelm
parents: 69352
diff changeset
   172
      ISABELLE_FONTS_HIDDEN="$X"
ab66951166f3 clarified "hidden" terminology;
wenzelm
parents: 69352
diff changeset
   173
    else
ab66951166f3 clarified "hidden" terminology;
wenzelm
parents: 69352
diff changeset
   174
      ISABELLE_FONTS_HIDDEN="$ISABELLE_FONTS_HIDDEN:$X"
ab66951166f3 clarified "hidden" terminology;
wenzelm
parents: 69352
diff changeset
   175
    fi
ab66951166f3 clarified "hidden" terminology;
wenzelm
parents: 69352
diff changeset
   176
  done
ab66951166f3 clarified "hidden" terminology;
wenzelm
parents: 69352
diff changeset
   177
  export ISABELLE_FONTS_HIDDEN
ab66951166f3 clarified "hidden" terminology;
wenzelm
parents: 69352
diff changeset
   178
}
ab66951166f3 clarified "hidden" terminology;
wenzelm
parents: 69352
diff changeset
   179
export -f isabelle_fonts_hidden
ab66951166f3 clarified "hidden" terminology;
wenzelm
parents: 69352
diff changeset
   180
71949
6c470c918aad more general support for isabelle_scala_service;
wenzelm
parents: 69417
diff changeset
   181
#Isabelle/Scala services
6c470c918aad more general support for isabelle_scala_service;
wenzelm
parents: 69417
diff changeset
   182
function isabelle_scala_service ()
69260
800b1ce96fce more general support for Isabelle/PIDE file formats -- less hardwired Bibtex operations;
wenzelm
parents: 69157
diff changeset
   183
{
800b1ce96fce more general support for Isabelle/PIDE file formats -- less hardwired Bibtex operations;
wenzelm
parents: 69157
diff changeset
   184
  local X=""
800b1ce96fce more general support for Isabelle/PIDE file formats -- less hardwired Bibtex operations;
wenzelm
parents: 69157
diff changeset
   185
  for X in "$@"
800b1ce96fce more general support for Isabelle/PIDE file formats -- less hardwired Bibtex operations;
wenzelm
parents: 69157
diff changeset
   186
  do
71949
6c470c918aad more general support for isabelle_scala_service;
wenzelm
parents: 69417
diff changeset
   187
    if [ -z "$ISABELLE_SCALA_SERVICES" ]; then
6c470c918aad more general support for isabelle_scala_service;
wenzelm
parents: 69417
diff changeset
   188
      ISABELLE_SCALA_SERVICES="$X"
69260
800b1ce96fce more general support for Isabelle/PIDE file formats -- less hardwired Bibtex operations;
wenzelm
parents: 69157
diff changeset
   189
    else
71949
6c470c918aad more general support for isabelle_scala_service;
wenzelm
parents: 69417
diff changeset
   190
      ISABELLE_SCALA_SERVICES="$ISABELLE_SCALA_SERVICES:$X"
69260
800b1ce96fce more general support for Isabelle/PIDE file formats -- less hardwired Bibtex operations;
wenzelm
parents: 69157
diff changeset
   191
    fi
800b1ce96fce more general support for Isabelle/PIDE file formats -- less hardwired Bibtex operations;
wenzelm
parents: 69157
diff changeset
   192
  done
71949
6c470c918aad more general support for isabelle_scala_service;
wenzelm
parents: 69417
diff changeset
   193
  export ISABELLE_SCALA_SERVICES
69260
800b1ce96fce more general support for Isabelle/PIDE file formats -- less hardwired Bibtex operations;
wenzelm
parents: 69157
diff changeset
   194
}
71949
6c470c918aad more general support for isabelle_scala_service;
wenzelm
parents: 69417
diff changeset
   195
export -f isabelle_scala_service
69260
800b1ce96fce more general support for Isabelle/PIDE file formats -- less hardwired Bibtex operations;
wenzelm
parents: 69157
diff changeset
   196
72395
5894859c5c84 more systematic support for special directories;
wenzelm
parents: 71952
diff changeset
   197
#Special directories
5894859c5c84 more systematic support for special directories;
wenzelm
parents: 71952
diff changeset
   198
function isabelle_directory ()
5894859c5c84 more systematic support for special directories;
wenzelm
parents: 71952
diff changeset
   199
{
5894859c5c84 more systematic support for special directories;
wenzelm
parents: 71952
diff changeset
   200
  local X=""
5894859c5c84 more systematic support for special directories;
wenzelm
parents: 71952
diff changeset
   201
  for X in "$@"
5894859c5c84 more systematic support for special directories;
wenzelm
parents: 71952
diff changeset
   202
  do
5894859c5c84 more systematic support for special directories;
wenzelm
parents: 71952
diff changeset
   203
    if [ -z "$ISABELLE_DIRECTORIES" ]; then
5894859c5c84 more systematic support for special directories;
wenzelm
parents: 71952
diff changeset
   204
      ISABELLE_DIRECTORIES="$X"
5894859c5c84 more systematic support for special directories;
wenzelm
parents: 71952
diff changeset
   205
    else
5894859c5c84 more systematic support for special directories;
wenzelm
parents: 71952
diff changeset
   206
      ISABELLE_DIRECTORIES="$ISABELLE_DIRECTORIES:$X"
5894859c5c84 more systematic support for special directories;
wenzelm
parents: 71952
diff changeset
   207
    fi
5894859c5c84 more systematic support for special directories;
wenzelm
parents: 71952
diff changeset
   208
  done
5894859c5c84 more systematic support for special directories;
wenzelm
parents: 71952
diff changeset
   209
  export ISABELLE_DIRECTORIES
5894859c5c84 more systematic support for special directories;
wenzelm
parents: 71952
diff changeset
   210
}
5894859c5c84 more systematic support for special directories;
wenzelm
parents: 71952
diff changeset
   211
export -f isabelle_directory
5894859c5c84 more systematic support for special directories;
wenzelm
parents: 71952
diff changeset
   212
62413
ffdc5cf36dc5 more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff changeset
   213
#administrative build
ffdc5cf36dc5 more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff changeset
   214
if [ -e "$ISABELLE_HOME/Admin/build" ]; then
ffdc5cf36dc5 more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff changeset
   215
  function isabelle_admin_build ()
ffdc5cf36dc5 more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff changeset
   216
  {
ffdc5cf36dc5 more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff changeset
   217
    "$ISABELLE_HOME/Admin/build" "$@"
ffdc5cf36dc5 more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff changeset
   218
  }
ffdc5cf36dc5 more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff changeset
   219
else
ffdc5cf36dc5 more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff changeset
   220
  function isabelle_admin_build () { return 0; }
ffdc5cf36dc5 more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff changeset
   221
fi
62414
c6111df4a4f8 avoid global state change;
wenzelm
parents: 62413
diff changeset
   222
export -f isabelle_admin_build
62413
ffdc5cf36dc5 more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff changeset
   223
ffdc5cf36dc5 more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff changeset
   224
#arrays
ffdc5cf36dc5 more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff changeset
   225
function splitarray ()
ffdc5cf36dc5 more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff changeset
   226
{
ffdc5cf36dc5 more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff changeset
   227
  SPLITARRAY=()
ffdc5cf36dc5 more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff changeset
   228
  local IFS="$1"; shift
66669
2e580fcf6522 avoid local shell variables intruding the resulting environment (via "set -o allexport" in getsettings);
wenzelm
parents: 63994
diff changeset
   229
  local X=""
62413
ffdc5cf36dc5 more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff changeset
   230
  for X in $*
ffdc5cf36dc5 more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff changeset
   231
  do
ffdc5cf36dc5 more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff changeset
   232
    SPLITARRAY["${#SPLITARRAY[@]}"]="$X"
ffdc5cf36dc5 more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff changeset
   233
  done
ffdc5cf36dc5 more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff changeset
   234
}
62414
c6111df4a4f8 avoid global state change;
wenzelm
parents: 62413
diff changeset
   235
export -f splitarray
62413
ffdc5cf36dc5 more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff changeset
   236
ffdc5cf36dc5 more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff changeset
   237
#init component tree
ffdc5cf36dc5 more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff changeset
   238
function init_component ()
ffdc5cf36dc5 more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff changeset
   239
{
ffdc5cf36dc5 more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff changeset
   240
  local COMPONENT="$1"
ffdc5cf36dc5 more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff changeset
   241
  case "$COMPONENT" in
ffdc5cf36dc5 more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff changeset
   242
    /*) ;;
ffdc5cf36dc5 more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff changeset
   243
    *)
ffdc5cf36dc5 more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff changeset
   244
      echo >&2 "Absolute component path required: \"$COMPONENT\""
ffdc5cf36dc5 more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff changeset
   245
      exit 2
ffdc5cf36dc5 more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff changeset
   246
      ;;
ffdc5cf36dc5 more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff changeset
   247
  esac
ffdc5cf36dc5 more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff changeset
   248
ffdc5cf36dc5 more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff changeset
   249
  if [ -d "$COMPONENT" ]; then
ffdc5cf36dc5 more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff changeset
   250
    if [ -z "$ISABELLE_COMPONENTS" ]; then
ffdc5cf36dc5 more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff changeset
   251
      ISABELLE_COMPONENTS="$COMPONENT"
ffdc5cf36dc5 more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff changeset
   252
    else
ffdc5cf36dc5 more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff changeset
   253
      ISABELLE_COMPONENTS="$ISABELLE_COMPONENTS:$COMPONENT"
ffdc5cf36dc5 more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff changeset
   254
    fi
ffdc5cf36dc5 more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff changeset
   255
  else
ffdc5cf36dc5 more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff changeset
   256
    echo >&2 "### Missing Isabelle component: \"$COMPONENT\""
ffdc5cf36dc5 more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff changeset
   257
    if [ -z "$ISABELLE_COMPONENTS_MISSING" ]; then
ffdc5cf36dc5 more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff changeset
   258
      ISABELLE_COMPONENTS_MISSING="$COMPONENT"
ffdc5cf36dc5 more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff changeset
   259
    else
ffdc5cf36dc5 more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff changeset
   260
      ISABELLE_COMPONENTS_MISSING="$ISABELLE_COMPONENTS_MISSING:$COMPONENT"
ffdc5cf36dc5 more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff changeset
   261
    fi
ffdc5cf36dc5 more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff changeset
   262
  fi
ffdc5cf36dc5 more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff changeset
   263
ffdc5cf36dc5 more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff changeset
   264
  if [ -f "$COMPONENT/etc/settings" ]; then
ffdc5cf36dc5 more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff changeset
   265
    source "$COMPONENT/etc/settings"
ffdc5cf36dc5 more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff changeset
   266
    local RC="$?"
ffdc5cf36dc5 more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff changeset
   267
    if [ "$RC" -ne 0 ]; then
ffdc5cf36dc5 more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff changeset
   268
      echo >&2 "Return code $RC from bash script: \"$COMPONENT/etc/settings\""
ffdc5cf36dc5 more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff changeset
   269
      exit 2
ffdc5cf36dc5 more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff changeset
   270
    fi
ffdc5cf36dc5 more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff changeset
   271
  fi
ffdc5cf36dc5 more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff changeset
   272
  if [ -f "$COMPONENT/etc/components" ]; then
ffdc5cf36dc5 more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff changeset
   273
    init_components "$COMPONENT" "$COMPONENT/etc/components"
ffdc5cf36dc5 more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff changeset
   274
  fi
ffdc5cf36dc5 more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff changeset
   275
}
62414
c6111df4a4f8 avoid global state change;
wenzelm
parents: 62413
diff changeset
   276
export -f init_component
62413
ffdc5cf36dc5 more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff changeset
   277
ffdc5cf36dc5 more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff changeset
   278
#init component forest
ffdc5cf36dc5 more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff changeset
   279
function init_components ()
ffdc5cf36dc5 more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff changeset
   280
{
66669
2e580fcf6522 avoid local shell variables intruding the resulting environment (via "set -o allexport" in getsettings);
wenzelm
parents: 63994
diff changeset
   281
  local REPLY=""
62413
ffdc5cf36dc5 more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff changeset
   282
  local BASE="$1"
ffdc5cf36dc5 more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff changeset
   283
  local CATALOG="$2"
ffdc5cf36dc5 more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff changeset
   284
  local COMPONENT=""
ffdc5cf36dc5 more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff changeset
   285
  local -a COMPONENTS=()
ffdc5cf36dc5 more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff changeset
   286
ffdc5cf36dc5 more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff changeset
   287
  if [ ! -f "$CATALOG" ]; then
ffdc5cf36dc5 more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff changeset
   288
    echo >&2 "Bad component catalog file: \"$CATALOG\""
ffdc5cf36dc5 more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff changeset
   289
    exit 2
ffdc5cf36dc5 more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff changeset
   290
  fi
ffdc5cf36dc5 more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff changeset
   291
ffdc5cf36dc5 more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff changeset
   292
  {
ffdc5cf36dc5 more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff changeset
   293
    while { unset REPLY; read -r; test "$?" = 0 -o -n "$REPLY"; }
ffdc5cf36dc5 more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff changeset
   294
    do
ffdc5cf36dc5 more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff changeset
   295
      case "$REPLY" in
ffdc5cf36dc5 more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff changeset
   296
        \#* | "") ;;
ffdc5cf36dc5 more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff changeset
   297
        /*) COMPONENTS["${#COMPONENTS[@]}"]="$REPLY" ;;
ffdc5cf36dc5 more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff changeset
   298
        *) COMPONENTS["${#COMPONENTS[@]}"]="$BASE/$REPLY" ;;
ffdc5cf36dc5 more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff changeset
   299
      esac
ffdc5cf36dc5 more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff changeset
   300
    done
ffdc5cf36dc5 more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff changeset
   301
  } < "$CATALOG"
ffdc5cf36dc5 more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff changeset
   302
ffdc5cf36dc5 more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff changeset
   303
  for COMPONENT in "${COMPONENTS[@]}"
ffdc5cf36dc5 more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff changeset
   304
  do
ffdc5cf36dc5 more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff changeset
   305
    init_component "$COMPONENT"
ffdc5cf36dc5 more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff changeset
   306
  done
ffdc5cf36dc5 more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff changeset
   307
}
62414
c6111df4a4f8 avoid global state change;
wenzelm
parents: 62413
diff changeset
   308
export -f init_components
62413
ffdc5cf36dc5 more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff changeset
   309
ffdc5cf36dc5 more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff changeset
   310
fi