lib/scripts/getfunctions
author wenzelm
Sun, 18 Jul 2021 12:48:31 +0200
changeset 74038 b4f57bfe82e7
parent 74017 b4e6b82fdb9e
child 78939 218929597048
permissions -rw-r--r--
more robust "isabelle build_scala" as separate tool;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
62412
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
73773
ac7f41b66e1b further "unset CDPATH", whenever a new non-interactive bash is started (see also ac07f6be27ea);
wenzelm
parents: 73580
diff changeset
     9
unset CDPATH
ac7f41b66e1b further "unset CDPATH", whenever a new non-interactive bash is started (see also ac07f6be27ea);
wenzelm
parents: 73580
diff changeset
    10
62416
cb6c4e307b1c slightly more robust re-initialization;
wenzelm
parents: 62414
diff changeset
    11
if type splitarray >/dev/null 2>/dev/null
62412
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
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
    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
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
    15
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
    16
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
    17
  function platform_path() { cygpath -i -C UTF8 -w -p "$@"; }
69157
22ae1d926f96 more portable;
wenzelm
parents: 69150
diff changeset
    18
  function standard_path() { cygpath -i -u -p "$@" | tr -d '\r'; }
62412
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
    19
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
    20
  function platform_path() { echo "$@"; }
69157
22ae1d926f96 more portable;
wenzelm
parents: 69150
diff changeset
    21
  function standard_path() { echo "$@"; }
62412
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
fi
69157
22ae1d926f96 more portable;
wenzelm
parents: 69150
diff changeset
    23
export -f platform_path standard_path
62412
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
    24
72894
bd2269b6cd99 updated "macOS" terminology: current Big Sur is already version 11;
wenzelm
parents: 72465
diff changeset
    25
#GNU tar (notably on macOS)
73580
a96564139fa7 more robust bootstrap of components;
wenzelm
parents: 73579
diff changeset
    26
function tar() {
a96564139fa7 more robust bootstrap of components;
wenzelm
parents: 73579
diff changeset
    27
  if [ -f "$ISABELLE_TAR" ]; then
a96564139fa7 more robust bootstrap of components;
wenzelm
parents: 73579
diff changeset
    28
    "$ISABELLE_TAR" "$@"
a96564139fa7 more robust bootstrap of components;
wenzelm
parents: 73579
diff changeset
    29
  else
a96564139fa7 more robust bootstrap of components;
wenzelm
parents: 73579
diff changeset
    30
    "$(type -P tar)" "$@"
a96564139fa7 more robust bootstrap of components;
wenzelm
parents: 73579
diff changeset
    31
  fi
a96564139fa7 more robust bootstrap of components;
wenzelm
parents: 73579
diff changeset
    32
}
73579
8ddf6728ad80 more self-contained support for macOS;
wenzelm
parents: 73513
diff changeset
    33
export -f tar
62412
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
    34
69134
a142ec271d83 isabelle_opam as portable shell function;
wenzelm
parents: 66667
diff changeset
    35
#OCaml management via OPAM
73500
a33e5298aee6 tuned whitespace;
wenzelm
parents: 72894
diff changeset
    36
function isabelle_opam ()
69134
a142ec271d83 isabelle_opam as portable shell function;
wenzelm
parents: 66667
diff changeset
    37
{
a142ec271d83 isabelle_opam as portable shell function;
wenzelm
parents: 66667
diff changeset
    38
  if [ -z "$ISABELLE_OPAM" ]; then
a142ec271d83 isabelle_opam as portable shell function;
wenzelm
parents: 66667
diff changeset
    39
    echo "Unknown ISABELLE_OPAM -- OCaml management tools unavailable" >&2
a142ec271d83 isabelle_opam as portable shell function;
wenzelm
parents: 66667
diff changeset
    40
    return 127
a142ec271d83 isabelle_opam as portable shell function;
wenzelm
parents: 66667
diff changeset
    41
  else
72465
de11c745ebbc tuned messages --- less SPAM;
wenzelm
parents: 72162
diff changeset
    42
    env OPAMROOT="$ISABELLE_OPAM_ROOT" OPAMCOLOR="never" "$ISABELLE_OPAM" "$@"
69134
a142ec271d83 isabelle_opam as portable shell function;
wenzelm
parents: 66667
diff changeset
    43
  fi
a142ec271d83 isabelle_opam as portable shell function;
wenzelm
parents: 66667
diff changeset
    44
}
a142ec271d83 isabelle_opam as portable shell function;
wenzelm
parents: 66667
diff changeset
    45
export -f isabelle_opam
a142ec271d83 isabelle_opam as portable shell function;
wenzelm
parents: 66667
diff changeset
    46
69150
wenzelm
parents: 69147
diff changeset
    47
#GHC management via Stack
73500
a33e5298aee6 tuned whitespace;
wenzelm
parents: 72894
diff changeset
    48
function isabelle_stack ()
69147
6f4d561ea621 isabelle_stack as portable shell function;
wenzelm
parents: 69134
diff changeset
    49
{
6f4d561ea621 isabelle_stack as portable shell function;
wenzelm
parents: 69134
diff changeset
    50
  if [ -z "$ISABELLE_STACK" ]; then
69150
wenzelm
parents: 69147
diff changeset
    51
    echo "Unknown ISABELLE_STACK -- GHC management tools unavailable" >&2
69147
6f4d561ea621 isabelle_stack as portable shell function;
wenzelm
parents: 69134
diff changeset
    52
    return 127
6f4d561ea621 isabelle_stack as portable shell function;
wenzelm
parents: 69134
diff changeset
    53
  else
69267
517655a528fe always insist in specified resolver/compiler version;
wenzelm
parents: 69255
diff changeset
    54
    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
    55
  fi
6f4d561ea621 isabelle_stack as portable shell function;
wenzelm
parents: 69134
diff changeset
    56
}
6f4d561ea621 isabelle_stack as portable shell function;
wenzelm
parents: 69134
diff changeset
    57
export -f isabelle_stack
6f4d561ea621 isabelle_stack as portable shell function;
wenzelm
parents: 69134
diff changeset
    58
62412
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
#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
    60
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
    61
{
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
  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
    63
    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
    64
    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
    65
  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
    66
    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
    67
    "$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
    68
  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
    69
}
62413
c6111df4a4f8 avoid global state change;
wenzelm
parents: 62412
diff changeset
    70
export -f isabelle_jdk
62412
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
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
#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
    73
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
    74
{
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
  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
    76
    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
    77
    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
    78
  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
    79
    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
    80
    "$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
    81
  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
    82
}
62413
c6111df4a4f8 avoid global state change;
wenzelm
parents: 62412
diff changeset
    83
export -f isabelle_java
62412
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
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
#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
    86
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
    87
{
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
  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
    89
    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
    90
    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
    91
  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
    92
    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
    93
    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
    94
  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
    95
    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
    96
    "$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
    97
  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
    98
}
62413
c6111df4a4f8 avoid global state change;
wenzelm
parents: 62412
diff changeset
    99
export -f isabelle_scala
62412
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
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
#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
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
   103
{
66667
2e580fcf6522 avoid local shell variables intruding the resulting environment (via "set -o allexport" in getsettings);
wenzelm
parents: 63994
diff changeset
   104
  local X=""
62412
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
  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
   106
  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
   107
    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
   108
      ISABELLE_CLASSPATH="$X"
73989
842fc354c031 more robust classpath: skip empty entries;
wenzelm
parents: 73988
diff changeset
   109
    elif [ -n "$X" ]; then
62412
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
      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
   111
    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
   112
  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
   113
  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
   114
}
62413
c6111df4a4f8 avoid global state change;
wenzelm
parents: 62412
diff changeset
   115
export -f classpath
62412
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
   116
73513
b7bb665fe850 more systematic java_library: avoid empty entries, declaration order as for other bash functions;
wenzelm
parents: 73500
diff changeset
   117
#java_library
b7bb665fe850 more systematic java_library: avoid empty entries, declaration order as for other bash functions;
wenzelm
parents: 73500
diff changeset
   118
function java_library ()
b7bb665fe850 more systematic java_library: avoid empty entries, declaration order as for other bash functions;
wenzelm
parents: 73500
diff changeset
   119
{
b7bb665fe850 more systematic java_library: avoid empty entries, declaration order as for other bash functions;
wenzelm
parents: 73500
diff changeset
   120
  local X=""
b7bb665fe850 more systematic java_library: avoid empty entries, declaration order as for other bash functions;
wenzelm
parents: 73500
diff changeset
   121
  for X in "$@"
b7bb665fe850 more systematic java_library: avoid empty entries, declaration order as for other bash functions;
wenzelm
parents: 73500
diff changeset
   122
  do
b7bb665fe850 more systematic java_library: avoid empty entries, declaration order as for other bash functions;
wenzelm
parents: 73500
diff changeset
   123
    case "$ISABELLE_PLATFORM_FAMILY" in
b7bb665fe850 more systematic java_library: avoid empty entries, declaration order as for other bash functions;
wenzelm
parents: 73500
diff changeset
   124
      linux)
b7bb665fe850 more systematic java_library: avoid empty entries, declaration order as for other bash functions;
wenzelm
parents: 73500
diff changeset
   125
        if [ -z "$LD_LIBRARY_PATH" ]; then
b7bb665fe850 more systematic java_library: avoid empty entries, declaration order as for other bash functions;
wenzelm
parents: 73500
diff changeset
   126
          export LD_LIBRARY_PATH="$X"
b7bb665fe850 more systematic java_library: avoid empty entries, declaration order as for other bash functions;
wenzelm
parents: 73500
diff changeset
   127
        else
b7bb665fe850 more systematic java_library: avoid empty entries, declaration order as for other bash functions;
wenzelm
parents: 73500
diff changeset
   128
          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: 73500
diff changeset
   129
        fi
b7bb665fe850 more systematic java_library: avoid empty entries, declaration order as for other bash functions;
wenzelm
parents: 73500
diff changeset
   130
        ;;
b7bb665fe850 more systematic java_library: avoid empty entries, declaration order as for other bash functions;
wenzelm
parents: 73500
diff changeset
   131
      macos)
b7bb665fe850 more systematic java_library: avoid empty entries, declaration order as for other bash functions;
wenzelm
parents: 73500
diff changeset
   132
        if [ -z "$JAVA_LIBRARY_PATH" ]; then
b7bb665fe850 more systematic java_library: avoid empty entries, declaration order as for other bash functions;
wenzelm
parents: 73500
diff changeset
   133
          export JAVA_LIBRARY_PATH="$X"
b7bb665fe850 more systematic java_library: avoid empty entries, declaration order as for other bash functions;
wenzelm
parents: 73500
diff changeset
   134
        else
b7bb665fe850 more systematic java_library: avoid empty entries, declaration order as for other bash functions;
wenzelm
parents: 73500
diff changeset
   135
          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: 73500
diff changeset
   136
        fi
b7bb665fe850 more systematic java_library: avoid empty entries, declaration order as for other bash functions;
wenzelm
parents: 73500
diff changeset
   137
        ;;
b7bb665fe850 more systematic java_library: avoid empty entries, declaration order as for other bash functions;
wenzelm
parents: 73500
diff changeset
   138
      windows)
b7bb665fe850 more systematic java_library: avoid empty entries, declaration order as for other bash functions;
wenzelm
parents: 73500
diff changeset
   139
        if [ -z "$PATH" ]; then
b7bb665fe850 more systematic java_library: avoid empty entries, declaration order as for other bash functions;
wenzelm
parents: 73500
diff changeset
   140
          export PATH="$X"
b7bb665fe850 more systematic java_library: avoid empty entries, declaration order as for other bash functions;
wenzelm
parents: 73500
diff changeset
   141
        else
b7bb665fe850 more systematic java_library: avoid empty entries, declaration order as for other bash functions;
wenzelm
parents: 73500
diff changeset
   142
          export PATH="$PATH:$X"
b7bb665fe850 more systematic java_library: avoid empty entries, declaration order as for other bash functions;
wenzelm
parents: 73500
diff changeset
   143
        fi
b7bb665fe850 more systematic java_library: avoid empty entries, declaration order as for other bash functions;
wenzelm
parents: 73500
diff changeset
   144
        ;;
b7bb665fe850 more systematic java_library: avoid empty entries, declaration order as for other bash functions;
wenzelm
parents: 73500
diff changeset
   145
    esac
b7bb665fe850 more systematic java_library: avoid empty entries, declaration order as for other bash functions;
wenzelm
parents: 73500
diff changeset
   146
  done
b7bb665fe850 more systematic java_library: avoid empty entries, declaration order as for other bash functions;
wenzelm
parents: 73500
diff changeset
   147
  export ISABELLE_CLASSPATH
b7bb665fe850 more systematic java_library: avoid empty entries, declaration order as for other bash functions;
wenzelm
parents: 73500
diff changeset
   148
}
b7bb665fe850 more systematic java_library: avoid empty entries, declaration order as for other bash functions;
wenzelm
parents: 73500
diff changeset
   149
export -f java_library
b7bb665fe850 more systematic java_library: avoid empty entries, declaration order as for other bash functions;
wenzelm
parents: 73500
diff changeset
   150
69342
fa981730b964 more shell functions;
wenzelm
parents: 69277
diff changeset
   151
#Isabelle fonts
fa981730b964 more shell functions;
wenzelm
parents: 69277
diff changeset
   152
function isabelle_fonts ()
fa981730b964 more shell functions;
wenzelm
parents: 69277
diff changeset
   153
{
fa981730b964 more shell functions;
wenzelm
parents: 69277
diff changeset
   154
  local X=""
fa981730b964 more shell functions;
wenzelm
parents: 69277
diff changeset
   155
  for X in "$@"
fa981730b964 more shell functions;
wenzelm
parents: 69277
diff changeset
   156
  do
fa981730b964 more shell functions;
wenzelm
parents: 69277
diff changeset
   157
    if [ -z "$ISABELLE_FONTS" ]; then
fa981730b964 more shell functions;
wenzelm
parents: 69277
diff changeset
   158
      ISABELLE_FONTS="$X"
fa981730b964 more shell functions;
wenzelm
parents: 69277
diff changeset
   159
    else
fa981730b964 more shell functions;
wenzelm
parents: 69277
diff changeset
   160
      ISABELLE_FONTS="$ISABELLE_FONTS:$X"
fa981730b964 more shell functions;
wenzelm
parents: 69277
diff changeset
   161
    fi
fa981730b964 more shell functions;
wenzelm
parents: 69277
diff changeset
   162
  done
fa981730b964 more shell functions;
wenzelm
parents: 69277
diff changeset
   163
  export ISABELLE_FONTS
fa981730b964 more shell functions;
wenzelm
parents: 69277
diff changeset
   164
}
fa981730b964 more shell functions;
wenzelm
parents: 69277
diff changeset
   165
export -f isabelle_fonts
fa981730b964 more shell functions;
wenzelm
parents: 69277
diff changeset
   166
69374
ab66951166f3 clarified "hidden" terminology;
wenzelm
parents: 69342
diff changeset
   167
function isabelle_fonts_hidden ()
ab66951166f3 clarified "hidden" terminology;
wenzelm
parents: 69342
diff changeset
   168
{
ab66951166f3 clarified "hidden" terminology;
wenzelm
parents: 69342
diff changeset
   169
  local X=""
ab66951166f3 clarified "hidden" terminology;
wenzelm
parents: 69342
diff changeset
   170
  for X in "$@"
ab66951166f3 clarified "hidden" terminology;
wenzelm
parents: 69342
diff changeset
   171
  do
ab66951166f3 clarified "hidden" terminology;
wenzelm
parents: 69342
diff changeset
   172
    if [ -z "$ISABELLE_FONTS_HIDDEN" ]; then
ab66951166f3 clarified "hidden" terminology;
wenzelm
parents: 69342
diff changeset
   173
      ISABELLE_FONTS_HIDDEN="$X"
ab66951166f3 clarified "hidden" terminology;
wenzelm
parents: 69342
diff changeset
   174
    else
ab66951166f3 clarified "hidden" terminology;
wenzelm
parents: 69342
diff changeset
   175
      ISABELLE_FONTS_HIDDEN="$ISABELLE_FONTS_HIDDEN:$X"
ab66951166f3 clarified "hidden" terminology;
wenzelm
parents: 69342
diff changeset
   176
    fi
ab66951166f3 clarified "hidden" terminology;
wenzelm
parents: 69342
diff changeset
   177
  done
ab66951166f3 clarified "hidden" terminology;
wenzelm
parents: 69342
diff changeset
   178
  export ISABELLE_FONTS_HIDDEN
ab66951166f3 clarified "hidden" terminology;
wenzelm
parents: 69342
diff changeset
   179
}
ab66951166f3 clarified "hidden" terminology;
wenzelm
parents: 69342
diff changeset
   180
export -f isabelle_fonts_hidden
ab66951166f3 clarified "hidden" terminology;
wenzelm
parents: 69342
diff changeset
   181
71733
6c470c918aad more general support for isabelle_scala_service;
wenzelm
parents: 69407
diff changeset
   182
#Isabelle/Scala services
6c470c918aad more general support for isabelle_scala_service;
wenzelm
parents: 69407
diff changeset
   183
function isabelle_scala_service ()
69255
800b1ce96fce more general support for Isabelle/PIDE file formats -- less hardwired Bibtex operations;
wenzelm
parents: 69157
diff changeset
   184
{
800b1ce96fce more general support for Isabelle/PIDE file formats -- less hardwired Bibtex operations;
wenzelm
parents: 69157
diff changeset
   185
  local X=""
800b1ce96fce more general support for Isabelle/PIDE file formats -- less hardwired Bibtex operations;
wenzelm
parents: 69157
diff changeset
   186
  for X in "$@"
800b1ce96fce more general support for Isabelle/PIDE file formats -- less hardwired Bibtex operations;
wenzelm
parents: 69157
diff changeset
   187
  do
71733
6c470c918aad more general support for isabelle_scala_service;
wenzelm
parents: 69407
diff changeset
   188
    if [ -z "$ISABELLE_SCALA_SERVICES" ]; then
6c470c918aad more general support for isabelle_scala_service;
wenzelm
parents: 69407
diff changeset
   189
      ISABELLE_SCALA_SERVICES="$X"
69255
800b1ce96fce more general support for Isabelle/PIDE file formats -- less hardwired Bibtex operations;
wenzelm
parents: 69157
diff changeset
   190
    else
71733
6c470c918aad more general support for isabelle_scala_service;
wenzelm
parents: 69407
diff changeset
   191
      ISABELLE_SCALA_SERVICES="$ISABELLE_SCALA_SERVICES:$X"
69255
800b1ce96fce more general support for Isabelle/PIDE file formats -- less hardwired Bibtex operations;
wenzelm
parents: 69157
diff changeset
   192
    fi
800b1ce96fce more general support for Isabelle/PIDE file formats -- less hardwired Bibtex operations;
wenzelm
parents: 69157
diff changeset
   193
  done
71733
6c470c918aad more general support for isabelle_scala_service;
wenzelm
parents: 69407
diff changeset
   194
  export ISABELLE_SCALA_SERVICES
69255
800b1ce96fce more general support for Isabelle/PIDE file formats -- less hardwired Bibtex operations;
wenzelm
parents: 69157
diff changeset
   195
}
71733
6c470c918aad more general support for isabelle_scala_service;
wenzelm
parents: 69407
diff changeset
   196
export -f isabelle_scala_service
69255
800b1ce96fce more general support for Isabelle/PIDE file formats -- less hardwired Bibtex operations;
wenzelm
parents: 69157
diff changeset
   197
72162
5894859c5c84 more systematic support for special directories;
wenzelm
parents: 71736
diff changeset
   198
#Special directories
5894859c5c84 more systematic support for special directories;
wenzelm
parents: 71736
diff changeset
   199
function isabelle_directory ()
5894859c5c84 more systematic support for special directories;
wenzelm
parents: 71736
diff changeset
   200
{
5894859c5c84 more systematic support for special directories;
wenzelm
parents: 71736
diff changeset
   201
  local X=""
5894859c5c84 more systematic support for special directories;
wenzelm
parents: 71736
diff changeset
   202
  for X in "$@"
5894859c5c84 more systematic support for special directories;
wenzelm
parents: 71736
diff changeset
   203
  do
5894859c5c84 more systematic support for special directories;
wenzelm
parents: 71736
diff changeset
   204
    if [ -z "$ISABELLE_DIRECTORIES" ]; then
5894859c5c84 more systematic support for special directories;
wenzelm
parents: 71736
diff changeset
   205
      ISABELLE_DIRECTORIES="$X"
5894859c5c84 more systematic support for special directories;
wenzelm
parents: 71736
diff changeset
   206
    else
5894859c5c84 more systematic support for special directories;
wenzelm
parents: 71736
diff changeset
   207
      ISABELLE_DIRECTORIES="$ISABELLE_DIRECTORIES:$X"
5894859c5c84 more systematic support for special directories;
wenzelm
parents: 71736
diff changeset
   208
    fi
5894859c5c84 more systematic support for special directories;
wenzelm
parents: 71736
diff changeset
   209
  done
5894859c5c84 more systematic support for special directories;
wenzelm
parents: 71736
diff changeset
   210
  export ISABELLE_DIRECTORIES
5894859c5c84 more systematic support for special directories;
wenzelm
parents: 71736
diff changeset
   211
}
5894859c5c84 more systematic support for special directories;
wenzelm
parents: 71736
diff changeset
   212
export -f isabelle_directory
5894859c5c84 more systematic support for special directories;
wenzelm
parents: 71736
diff changeset
   213
62412
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
#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
   215
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
   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
  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
   218
  local IFS="$1"; shift
66667
2e580fcf6522 avoid local shell variables intruding the resulting environment (via "set -o allexport" in getsettings);
wenzelm
parents: 63994
diff changeset
   219
  local X=""
62412
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
  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
   221
  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
   222
    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
   223
  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
   224
}
62413
c6111df4a4f8 avoid global state change;
wenzelm
parents: 62412
diff changeset
   225
export -f splitarray
62412
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
#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
   228
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
   229
{
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
  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
   231
  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
   232
    /*) ;;
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
    *)
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
      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
   235
      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
   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
  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
   238
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
  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
   240
    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
   241
      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
   242
    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
   243
      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
   244
    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
   245
  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
   246
    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
   247
    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
   248
      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
   249
    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
   250
      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
   251
    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
   252
  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
   253
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
  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
   255
    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
   256
    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
   257
    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
   258
      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
   259
      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
   260
    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
   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
  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
   263
    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
   264
  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
   265
}
62413
c6111df4a4f8 avoid global state change;
wenzelm
parents: 62412
diff changeset
   266
export -f init_component
62412
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
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
#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
   269
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
   270
{
66667
2e580fcf6522 avoid local shell variables intruding the resulting environment (via "set -o allexport" in getsettings);
wenzelm
parents: 63994
diff changeset
   271
  local REPLY=""
62412
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
  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
   273
  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
   274
  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
   275
  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
   276
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
  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
   278
    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
   279
    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
   280
  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
   281
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
  {
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
    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
   284
    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
   285
      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
   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
        /*) 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
   288
        *) 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
   289
      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
   290
    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
   291
  } < "$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
   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
  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
   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
    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
   296
  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
   297
}
62413
c6111df4a4f8 avoid global state change;
wenzelm
parents: 62412
diff changeset
   298
export -f init_components
62412
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
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
fi