| 10555 |      1 | #!/usr/bin/env bash
 | 
| 2333 |      2 | #
 | 
|  |      3 | # $Id$
 | 
| 9788 |      4 | # Author: Markus Wenzel, TU Muenchen
 | 
| 2333 |      5 | #
 | 
|  |      6 | # DESCRIPTION: collect heap names from ISABELLE_PATH
 | 
|  |      7 | 
 | 
|  |      8 | 
 | 
| 9788 |      9 | PRG=$(basename "$0")
 | 
| 2333 |     10 | 
 | 
|  |     11 | function usage()
 | 
|  |     12 | {
 | 
|  |     13 |   echo
 | 
|  |     14 |   echo "Usage: $PRG"
 | 
|  |     15 |   echo
 | 
|  |     16 |   echo "  Collect heap file names from ISABELLE_PATH."
 | 
|  |     17 |   echo
 | 
|  |     18 |   exit 1
 | 
|  |     19 | }
 | 
|  |     20 | 
 | 
|  |     21 | 
 | 
|  |     22 | ## main
 | 
|  |     23 | 
 | 
| 9788 |     24 | [ "$#" -ne 0 ] && usage
 | 
| 2333 |     25 | 
 | 
|  |     26 | 
 | 
|  |     27 | LOGICS=""
 | 
|  |     28 | 
 | 
| 9788 |     29 | ORIG_IFS="$IFS"
 | 
|  |     30 | IFS=":"
 | 
|  |     31 | for DIR in $ISABELLE_PATH
 | 
| 2333 |     32 | do
 | 
| 9788 |     33 |   DIR="$DIR/$ML_IDENTIFIER"
 | 
|  |     34 |   for FILE in "$DIR"/*
 | 
| 2333 |     35 |   do
 | 
|  |     36 |     if [ -f "$FILE" ]; then
 | 
|  |     37 |       NAME=$(basename "$FILE")
 | 
|  |     38 |       LOGICS="$LOGICS $NAME"
 | 
|  |     39 |     fi
 | 
|  |     40 |   done
 | 
|  |     41 | done
 | 
| 9788 |     42 | IFS="$ORIG_IFS"
 | 
| 2333 |     43 | 
 | 
| 9788 |     44 | echo $({ for L in $LOGICS; do echo "$L"; done; } | sort | uniq)
 |