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