lib/scripts/getfunctions
author wenzelm
Thu, 25 Oct 2018 22:42:17 +0200
changeset 69188 2fd73a1a0937
parent 69157 22ae1d926f96
child 69255 800b1ce96fce
permissions -rw-r--r--
updated to jedit_build-20181025 according to patches/macos (Java 11), patches/putenv; proper update of jEdit environment -- avoid warnings in Java 11; activate jdk-11+28;
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
62416
cb6c4e307b1c slightly more robust re-initialization;
wenzelm
parents: 62414
diff changeset
     9
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
    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'; }
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
    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 "$@"; }
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
    20
fi
69157
22ae1d926f96 more portable;
wenzelm
parents: 69150
diff changeset
    21
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
    22
ffdc5cf36dc5 more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff changeset
    23
#GNU tar (notably on Mac OS X)
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 "$@"; }
62413
c6111df4a4f8 avoid global state change;
wenzelm
parents: 62412
diff changeset
    27
  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
    28
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
    29
69134
a142ec271d83 isabelle_opam as portable shell function;
wenzelm
parents: 66667
diff changeset
    30
#OCaml management via OPAM
a142ec271d83 isabelle_opam as portable shell function;
wenzelm
parents: 66667
diff changeset
    31
function isabelle_opam()
a142ec271d83 isabelle_opam as portable shell function;
wenzelm
parents: 66667
diff changeset
    32
{
a142ec271d83 isabelle_opam as portable shell function;
wenzelm
parents: 66667
diff changeset
    33
  if [ -z "$ISABELLE_OPAM" ]; then
a142ec271d83 isabelle_opam as portable shell function;
wenzelm
parents: 66667
diff changeset
    34
    echo "Unknown ISABELLE_OPAM -- OCaml management tools unavailable" >&2
a142ec271d83 isabelle_opam as portable shell function;
wenzelm
parents: 66667
diff changeset
    35
    return 127
a142ec271d83 isabelle_opam as portable shell function;
wenzelm
parents: 66667
diff changeset
    36
  else
a142ec271d83 isabelle_opam as portable shell function;
wenzelm
parents: 66667
diff changeset
    37
    env OPAMROOT="$ISABELLE_OPAM_ROOT" "$ISABELLE_OPAM" "$@"
a142ec271d83 isabelle_opam as portable shell function;
wenzelm
parents: 66667
diff changeset
    38
  fi
a142ec271d83 isabelle_opam as portable shell function;
wenzelm
parents: 66667
diff changeset
    39
}
a142ec271d83 isabelle_opam as portable shell function;
wenzelm
parents: 66667
diff changeset
    40
export -f isabelle_opam
a142ec271d83 isabelle_opam as portable shell function;
wenzelm
parents: 66667
diff changeset
    41
69150
wenzelm
parents: 69147
diff changeset
    42
#GHC management via Stack
69147
6f4d561ea621 isabelle_stack as portable shell function;
wenzelm
parents: 69134
diff changeset
    43
function isabelle_stack()
6f4d561ea621 isabelle_stack as portable shell function;
wenzelm
parents: 69134
diff changeset
    44
{
6f4d561ea621 isabelle_stack as portable shell function;
wenzelm
parents: 69134
diff changeset
    45
  if [ -z "$ISABELLE_STACK" ]; then
69150
wenzelm
parents: 69147
diff changeset
    46
    echo "Unknown ISABELLE_STACK -- GHC management tools unavailable" >&2
69147
6f4d561ea621 isabelle_stack as portable shell function;
wenzelm
parents: 69134
diff changeset
    47
    return 127
6f4d561ea621 isabelle_stack as portable shell function;
wenzelm
parents: 69134
diff changeset
    48
  else
6f4d561ea621 isabelle_stack as portable shell function;
wenzelm
parents: 69134
diff changeset
    49
    env STACK_ROOT="$(platform_path "$ISABELLE_STACK_ROOT")" "$ISABELLE_STACK" "$@"
6f4d561ea621 isabelle_stack as portable shell function;
wenzelm
parents: 69134
diff changeset
    50
  fi
6f4d561ea621 isabelle_stack as portable shell function;
wenzelm
parents: 69134
diff changeset
    51
}
6f4d561ea621 isabelle_stack as portable shell function;
wenzelm
parents: 69134
diff changeset
    52
export -f isabelle_stack
6f4d561ea621 isabelle_stack as portable shell function;
wenzelm
parents: 69134
diff changeset
    53
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
    54
#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
    55
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
    56
{
ffdc5cf36dc5 more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff changeset
    57
  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
    58
    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
    59
    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
    60
  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
    61
    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
    62
    "$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
    63
  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
    64
}
62413
c6111df4a4f8 avoid global state change;
wenzelm
parents: 62412
diff changeset
    65
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
    66
ffdc5cf36dc5 more robust treatment of 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
#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
    68
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
    69
{
ffdc5cf36dc5 more robust treatment of 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
  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
    71
    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
    72
    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
    73
  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
    74
    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
    75
    "$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
    76
  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
    77
}
62413
c6111df4a4f8 avoid global state change;
wenzelm
parents: 62412
diff changeset
    78
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
    79
ffdc5cf36dc5 more robust treatment of 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
#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
    81
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
    82
{
ffdc5cf36dc5 more robust treatment of 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
  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
    84
    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
    85
    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
    86
  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
    87
    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
    88
    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
    89
  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
    90
    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
    91
    "$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
    92
  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
    93
}
62413
c6111df4a4f8 avoid global state change;
wenzelm
parents: 62412
diff changeset
    94
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
    95
ffdc5cf36dc5 more robust treatment of 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
#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
    97
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
    98
{
66667
2e580fcf6522 avoid local shell variables intruding the resulting environment (via "set -o allexport" in getsettings);
wenzelm
parents: 63994
diff changeset
    99
  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
   100
  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
   101
  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
   102
    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
   103
      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
   104
    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
   105
      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
   106
    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
   107
  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
   108
  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
   109
}
62413
c6111df4a4f8 avoid global state change;
wenzelm
parents: 62412
diff changeset
   110
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
   111
ffdc5cf36dc5 more robust treatment of 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
#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
   113
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
   114
  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
   115
  {
ffdc5cf36dc5 more robust treatment of 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
    "$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
   117
  }
ffdc5cf36dc5 more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff changeset
   118
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
   119
  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
   120
fi
62413
c6111df4a4f8 avoid global state change;
wenzelm
parents: 62412
diff changeset
   121
export -f isabelle_admin_build
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
   122
ffdc5cf36dc5 more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff changeset
   123
#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
   124
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
   125
{
ffdc5cf36dc5 more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff changeset
   126
  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
   127
  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
   128
  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
   129
  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
   130
  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
   131
    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
   132
  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
   133
}
62413
c6111df4a4f8 avoid global state change;
wenzelm
parents: 62412
diff changeset
   134
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
   135
ffdc5cf36dc5 more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff changeset
   136
#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
   137
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
   138
{
ffdc5cf36dc5 more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff changeset
   139
  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
   140
  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
   141
    /*) ;;
ffdc5cf36dc5 more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff changeset
   142
    *)
ffdc5cf36dc5 more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff changeset
   143
      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
   144
      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
   145
      ;;
ffdc5cf36dc5 more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff changeset
   146
  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
   147
ffdc5cf36dc5 more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff changeset
   148
  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
   149
    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
   150
      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
   151
    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
   152
      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
   153
    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
   154
  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
   155
    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
   156
    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
   157
      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
   158
    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
   159
      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
   160
    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
   161
  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
   162
ffdc5cf36dc5 more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff changeset
   163
  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
   164
    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
   165
    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
   166
    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
   167
      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
   168
      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
   169
    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
   170
  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
   171
  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
   172
    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
   173
  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
   174
}
62413
c6111df4a4f8 avoid global state change;
wenzelm
parents: 62412
diff changeset
   175
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
   176
ffdc5cf36dc5 more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff changeset
   177
#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
   178
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
   179
{
66667
2e580fcf6522 avoid local shell variables intruding the resulting environment (via "set -o allexport" in getsettings);
wenzelm
parents: 63994
diff changeset
   180
  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
   181
  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
   182
  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
   183
  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
   184
  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
   185
ffdc5cf36dc5 more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff changeset
   186
  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
   187
    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
   188
    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
   189
  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
   190
ffdc5cf36dc5 more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff changeset
   191
  {
ffdc5cf36dc5 more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff changeset
   192
    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
   193
    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
   194
      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
   195
        \#* | "") ;;
ffdc5cf36dc5 more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff changeset
   196
        /*) 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
   197
        *) 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
   198
      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
   199
    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
   200
  } < "$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
   201
ffdc5cf36dc5 more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff changeset
   202
  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
   203
  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
   204
    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
   205
  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
   206
}
62413
c6111df4a4f8 avoid global state change;
wenzelm
parents: 62412
diff changeset
   207
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
   208
ffdc5cf36dc5 more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff changeset
   209
fi