lib/Tools/findlogics
changeset 9788 df671fa2562a
parent 3007 e5efa177ee0c
child 10555 2323ec838401
equal deleted inserted replaced
9787:fb8c5a66dbe8 9788:df671fa2562a
     1 #!/bin/bash
     1 #!/bin/bash
     2 #
     2 #
     3 # $Id$
     3 # $Id$
       
     4 # Author: Markus Wenzel, TU Muenchen
       
     5 # License: GPL (GNU GENERAL PUBLIC LICENSE)
     4 #
     6 #
     5 # DESCRIPTION: collect heap names from ISABELLE_PATH
     7 # DESCRIPTION: collect heap names from ISABELLE_PATH
     6 
     8 
     7 
     9 
     8 PRG=$(basename $0)
    10 PRG=$(basename "$0")
     9 
    11 
    10 function usage()
    12 function usage()
    11 {
    13 {
    12   echo
    14   echo
    13   echo "Usage: $PRG"
    15   echo "Usage: $PRG"
    18 }
    20 }
    19 
    21 
    20 
    22 
    21 ## main
    23 ## main
    22 
    24 
    23 [ $# -ne 0 ] && usage
    25 [ "$#" -ne 0 ] && usage
    24 
    26 
    25 
    27 
    26 LOGICS=""
    28 LOGICS=""
    27 
    29 
    28 for DIR in $(echo $ISABELLE_PATH | tr : " ")
    30 ORIG_IFS="$IFS"
       
    31 IFS=":"
       
    32 for DIR in $ISABELLE_PATH
    29 do
    33 do
    30   for FILE in $DIR/*
    34   DIR="$DIR/$ML_IDENTIFIER"
       
    35   for FILE in "$DIR"/*
    31   do
    36   do
    32     if [ -f "$FILE" ]; then
    37     if [ -f "$FILE" ]; then
    33       NAME=$(basename "$FILE")
    38       NAME=$(basename "$FILE")
    34       LOGICS="$LOGICS $NAME"
    39       LOGICS="$LOGICS $NAME"
    35     fi
    40     fi
    36   done
    41   done
    37 done
    42 done
       
    43 IFS="$ORIG_IFS"
    38 
    44 
    39 echo $({ for L in $LOGICS; do echo $L; done; } | sort | uniq)
    45 echo $({ for L in $LOGICS; do echo "$L"; done; } | sort | uniq)