| author | wenzelm | 
| Tue, 20 Apr 2010 17:07:53 +0200 | |
| changeset 36238 | 344377ce2e0a | 
| 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)
 |