1# -*- shell-script -*- :mode=shellscript:
2#
3# Author: Makarius
4#
5# Isabelle shell functions, with on-demand re-initialization for
6# non-interactive bash processess. NB: bash shell functions are not portable
7# and may be dropped by aggressively POSIX-conformant versions of /bin/sh.
8
9if type splitarray >/dev/null 2>/dev/null
10then
11  :
12else
13
14if [ "$OSTYPE" = cygwin ]; then
15  function platform_path() { cygpath -i -C UTF8 -w -p "$@"; }
16else
17  function platform_path() { echo "$@"; }
18fi
19export -f platform_path
20
21#GNU tar (notably on Mac OS X)
22if type -p gnutar >/dev/null
23then
24  function tar() { gnutar "$@"; }
25  export -f tar
26fi
27
28#robust invocation via ISABELLE_JDK_HOME
29function isabelle_jdk ()
30{
31  if [ -z "$ISABELLE_JDK_HOME" ]; then
32    echo "Unknown ISABELLE_JDK_HOME -- Java development tools unavailable" >&2
33    return 127
34  else
35    local PRG="$1"; shift
36    "$ISABELLE_JDK_HOME/bin/$PRG" "$@"
37  fi
38}
39export -f isabelle_jdk
40
41#robust invocation via JAVA_HOME
42function isabelle_java ()
43{
44  if [ -z "$JAVA_HOME" ]; then
45    echo "Unknown JAVA_HOME -- Java unavailable" >&2
46    return 127
47  else
48    local PRG="$1"; shift
49    "$JAVA_HOME/bin/$PRG" "$@"
50  fi
51}
52export -f isabelle_java
53
54#robust invocation via SCALA_HOME
55function isabelle_scala ()
56{
57  if [ -z "$JAVA_HOME" ]; then
58    echo "Unknown JAVA_HOME -- Java unavailable" >&2
59    return 127
60  elif [ -z "$SCALA_HOME" ]; then
61    echo "Unknown SCALA_HOME -- Scala unavailable" >&2
62    return 127
63  else
64    local PRG="$1"; shift
65    "$SCALA_HOME/bin/$PRG" "$@"
66  fi
67}
68export -f isabelle_scala
69
70#classpath
71function classpath ()
72{
73  local X=""
74  for X in "$@"
75  do
76    if [ -z "$ISABELLE_CLASSPATH" ]; then
77      ISABELLE_CLASSPATH="$X"
78    else
79      ISABELLE_CLASSPATH="$ISABELLE_CLASSPATH:$X"
80    fi
81  done
82  export ISABELLE_CLASSPATH
83}
84export -f classpath
85
86#administrative build
87if [ -e "$ISABELLE_HOME/Admin/build" ]; then
88  function isabelle_admin_build ()
89  {
90    "$ISABELLE_HOME/Admin/build" "$@"
91  }
92else
93  function isabelle_admin_build () { return 0; }
94fi
95export -f isabelle_admin_build
96
97#arrays
98function splitarray ()
99{
100  SPLITARRAY=()
101  local IFS="$1"; shift
102  local X=""
103  for X in $*
104  do
105    SPLITARRAY["${#SPLITARRAY[@]}"]="$X"
106  done
107}
108export -f splitarray
109
110#init component tree
111function init_component ()
112{
113  local COMPONENT="$1"
114  case "$COMPONENT" in
115    /*) ;;
116    *)
117      echo >&2 "Absolute component path required: \"$COMPONENT\""
118      exit 2
119      ;;
120  esac
121
122  if [ -d "$COMPONENT" ]; then
123    if [ -z "$ISABELLE_COMPONENTS" ]; then
124      ISABELLE_COMPONENTS="$COMPONENT"
125    else
126      ISABELLE_COMPONENTS="$ISABELLE_COMPONENTS:$COMPONENT"
127    fi
128  else
129    echo >&2 "### Missing Isabelle component: \"$COMPONENT\""
130    if [ -z "$ISABELLE_COMPONENTS_MISSING" ]; then
131      ISABELLE_COMPONENTS_MISSING="$COMPONENT"
132    else
133      ISABELLE_COMPONENTS_MISSING="$ISABELLE_COMPONENTS_MISSING:$COMPONENT"
134    fi
135  fi
136
137  if [ -f "$COMPONENT/etc/settings" ]; then
138    source "$COMPONENT/etc/settings"
139    local RC="$?"
140    if [ "$RC" -ne 0 ]; then
141      echo >&2 "Return code $RC from bash script: \"$COMPONENT/etc/settings\""
142      exit 2
143    fi
144  fi
145  if [ -f "$COMPONENT/etc/components" ]; then
146    init_components "$COMPONENT" "$COMPONENT/etc/components"
147  fi
148}
149export -f init_component
150
151#init component forest
152function init_components ()
153{
154  local REPLY=""
155  local BASE="$1"
156  local CATALOG="$2"
157  local COMPONENT=""
158  local -a COMPONENTS=()
159
160  if [ ! -f "$CATALOG" ]; then
161    echo >&2 "Bad component catalog file: \"$CATALOG\""
162    exit 2
163  fi
164
165  {
166    while { unset REPLY; read -r; test "$?" = 0 -o -n "$REPLY"; }
167    do
168      case "$REPLY" in
169        \#* | "") ;;
170        /*) COMPONENTS["${#COMPONENTS[@]}"]="$REPLY" ;;
171        *) COMPONENTS["${#COMPONENTS[@]}"]="$BASE/$REPLY" ;;
172      esac
173    done
174  } < "$CATALOG"
175
176  for COMPONENT in "${COMPONENTS[@]}"
177  do
178    init_component "$COMPONENT"
179  done
180}
181export -f init_components
182
183fi
184