| author | wenzelm |
| Tue, 08 Apr 2014 19:17:28 +0200 | |
| changeset 56470 | 8eda56033203 |
| 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)
|