author | wenzelm |
Tue, 04 Aug 2009 15:05:34 +0200 | |
changeset 32322 | 45cb4a86eca2 |
parent 29143 | 72c960b2b83e |
child 32390 | 468eff174a77 |
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 |
|
32322
45cb4a86eca2
change IFS only locally -- thanks to bash arrays;
wenzelm
parents:
29143
diff
changeset
|
28 |
ORIG_IFS="$IFS"; IFS=":"; ISABELLE_PATHS=($ISABELLE_PATH); IFS=$ORIG_IFS |
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") |
32322
45cb4a86eca2
change IFS only locally -- thanks to bash arrays;
wenzelm
parents:
29143
diff
changeset
|
37 |
LOGICS+=("$NAME") |
2333 | 38 |
fi |
39 |
done |
|
40 |
done |
|
41 |
||
32322
45cb4a86eca2
change IFS only locally -- thanks to bash arrays;
wenzelm
parents:
29143
diff
changeset
|
42 |
echo $({ for L in ${LOGICS[@]}; do echo "$L"; done; } | sort | uniq) |