author | blanchet |
Wed, 21 Apr 2010 14:02:19 +0200 | |
changeset 36266 | 28188e3650ee |
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:
29143
diff
changeset
|
25 |
declare -a LOGICS=() |
45cb4a86eca2
change IFS only locally -- thanks to bash arrays;
wenzelm
parents:
29143
diff
changeset
|
26 |
declare -a ISABELLE_PATHS=() |
2333 | 27 |
|
32390
468eff174a77
function splitarray: splightly more abstract version that accomodates older bashes;
wenzelm
parents:
32322
diff
changeset
|
28 |
splitarray ":" "$ISABELLE_PATH"; ISABELLE_PATHS=("${SPLITARRAY[@]}") |
32322
45cb4a86eca2
change IFS only locally -- thanks to bash arrays;
wenzelm
parents:
29143
diff
changeset
|
29 |
|
45cb4a86eca2
change IFS only locally -- thanks to bash arrays;
wenzelm
parents:
29143
diff
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:
32390
diff
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:
32391
diff
changeset
|
42 |
echo $({ for L in "${LOGICS[@]}"; do echo "$L"; done; } | sort | uniq) |