| author | wenzelm | 
| Wed, 13 Feb 2013 12:06:21 +0100 | |
| changeset 51089 | ced7163f1fe4 | 
| parent 33915 | 44a10fe6bd10 | 
| child 57414 | fe1be2844fda | 
| permissions | -rwxr-xr-x | 
| 10555 | 1 | #!/usr/bin/env bash | 
| 2333 | 2 | # | 
| 9788 | 3 | # Author: Markus Wenzel, TU Muenchen | 
| 2333 | 4 | # | 
| 5 | # DESCRIPTION: collect heap names from ISABELLE_PATH | |
| 6 | ||
| 7 | ||
| 9788 | 8 | PRG=$(basename "$0") | 
| 2333 | 9 | |
| 10 | function usage() | |
| 11 | {
 | |
| 12 | echo | |
| 28650 | 13 | echo "Usage: isabelle $PRG" | 
| 2333 | 14 | echo | 
| 15 | echo " Collect heap file names from ISABELLE_PATH." | |
| 16 | echo | |
| 17 | exit 1 | |
| 18 | } | |
| 19 | ||
| 20 | ||
| 21 | ## main | |
| 22 | ||
| 9788 | 23 | [ "$#" -ne 0 ] && usage | 
| 2333 | 24 | |
| 32322 
45cb4a86eca2
change IFS only locally -- thanks to bash arrays;
 wenzelm parents: 
29143diff
changeset | 25 | declare -a LOGICS=() | 
| 
45cb4a86eca2
change IFS only locally -- thanks to bash arrays;
 wenzelm parents: 
29143diff
changeset | 26 | declare -a ISABELLE_PATHS=() | 
| 2333 | 27 | |
| 32390 
468eff174a77
function splitarray: splightly more abstract version that accomodates older bashes;
 wenzelm parents: 
32322diff
changeset | 28 | splitarray ":" "$ISABELLE_PATH"; ISABELLE_PATHS=("${SPLITARRAY[@]}")
 | 
| 32322 
45cb4a86eca2
change IFS only locally -- thanks to bash arrays;
 wenzelm parents: 
29143diff
changeset | 29 | |
| 
45cb4a86eca2
change IFS only locally -- thanks to bash arrays;
 wenzelm parents: 
29143diff
changeset | 30 | for DIR in "${ISABELLE_PATHS[@]}"
 | 
| 2333 | 31 | do | 
| 9788 | 32 | DIR="$DIR/$ML_IDENTIFIER" | 
| 33 | for FILE in "$DIR"/* | |
| 2333 | 34 | do | 
| 35 | if [ -f "$FILE" ]; then | |
| 27201 | 36 | NAME=$(basename "$FILE") | 
| 32391 
5b9d7e578756
less ambitious array operations -- for improved compatibility with older versions of bash;
 wenzelm parents: 
32390diff
changeset | 37 |       LOGICS["${#LOGICS[@]}"]="$NAME"
 | 
| 2333 | 38 | fi | 
| 39 | done | |
| 40 | done | |
| 41 | ||
| 33915 
44a10fe6bd10
proper quoting of array expansion -- allow spaces in components;
 wenzelm parents: 
32391diff
changeset | 42 | echo $({ for L in "${LOGICS[@]}"; do echo "$L"; done; } | sort | uniq)
 |