lib/Tools/findlogics
author wenzelm
Mon, 20 Nov 2006 23:47:10 +0100
changeset 21426 87ac12bed1ab
parent 17792 4a34fd6884b1
child 27201 e0323036bcf2
permissions -rwxr-xr-x
converted legacy ML scripts;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
10555
2323ec838401 /usr/bin/env bash;
wenzelm
parents: 9788
diff changeset
     1
#!/usr/bin/env bash
2333
f1159f38ba4f findlogics: collect heap names from ISABELLE_PATH;
wenzelm
parents:
diff changeset
     2
#
f1159f38ba4f findlogics: collect heap names from ISABELLE_PATH;
wenzelm
parents:
diff changeset
     3
# $Id$
9788
wenzelm
parents: 3007
diff changeset
     4
# Author: Markus Wenzel, TU Muenchen
2333
f1159f38ba4f findlogics: collect heap names from ISABELLE_PATH;
wenzelm
parents:
diff changeset
     5
#
f1159f38ba4f findlogics: collect heap names from ISABELLE_PATH;
wenzelm
parents:
diff changeset
     6
# DESCRIPTION: collect heap names from ISABELLE_PATH
f1159f38ba4f findlogics: collect heap names from ISABELLE_PATH;
wenzelm
parents:
diff changeset
     7
f1159f38ba4f findlogics: collect heap names from ISABELLE_PATH;
wenzelm
parents:
diff changeset
     8
9788
wenzelm
parents: 3007
diff changeset
     9
PRG=$(basename "$0")
2333
f1159f38ba4f findlogics: collect heap names from ISABELLE_PATH;
wenzelm
parents:
diff changeset
    10
f1159f38ba4f findlogics: collect heap names from ISABELLE_PATH;
wenzelm
parents:
diff changeset
    11
function usage()
f1159f38ba4f findlogics: collect heap names from ISABELLE_PATH;
wenzelm
parents:
diff changeset
    12
{
f1159f38ba4f findlogics: collect heap names from ISABELLE_PATH;
wenzelm
parents:
diff changeset
    13
  echo
f1159f38ba4f findlogics: collect heap names from ISABELLE_PATH;
wenzelm
parents:
diff changeset
    14
  echo "Usage: $PRG"
f1159f38ba4f findlogics: collect heap names from ISABELLE_PATH;
wenzelm
parents:
diff changeset
    15
  echo
f1159f38ba4f findlogics: collect heap names from ISABELLE_PATH;
wenzelm
parents:
diff changeset
    16
  echo "  Collect heap file names from ISABELLE_PATH."
f1159f38ba4f findlogics: collect heap names from ISABELLE_PATH;
wenzelm
parents:
diff changeset
    17
  echo
f1159f38ba4f findlogics: collect heap names from ISABELLE_PATH;
wenzelm
parents:
diff changeset
    18
  exit 1
f1159f38ba4f findlogics: collect heap names from ISABELLE_PATH;
wenzelm
parents:
diff changeset
    19
}
f1159f38ba4f findlogics: collect heap names from ISABELLE_PATH;
wenzelm
parents:
diff changeset
    20
f1159f38ba4f findlogics: collect heap names from ISABELLE_PATH;
wenzelm
parents:
diff changeset
    21
f1159f38ba4f findlogics: collect heap names from ISABELLE_PATH;
wenzelm
parents:
diff changeset
    22
## main
f1159f38ba4f findlogics: collect heap names from ISABELLE_PATH;
wenzelm
parents:
diff changeset
    23
9788
wenzelm
parents: 3007
diff changeset
    24
[ "$#" -ne 0 ] && usage
2333
f1159f38ba4f findlogics: collect heap names from ISABELLE_PATH;
wenzelm
parents:
diff changeset
    25
f1159f38ba4f findlogics: collect heap names from ISABELLE_PATH;
wenzelm
parents:
diff changeset
    26
f1159f38ba4f findlogics: collect heap names from ISABELLE_PATH;
wenzelm
parents:
diff changeset
    27
LOGICS=""
f1159f38ba4f findlogics: collect heap names from ISABELLE_PATH;
wenzelm
parents:
diff changeset
    28
9788
wenzelm
parents: 3007
diff changeset
    29
ORIG_IFS="$IFS"
wenzelm
parents: 3007
diff changeset
    30
IFS=":"
wenzelm
parents: 3007
diff changeset
    31
for DIR in $ISABELLE_PATH
2333
f1159f38ba4f findlogics: collect heap names from ISABELLE_PATH;
wenzelm
parents:
diff changeset
    32
do
9788
wenzelm
parents: 3007
diff changeset
    33
  DIR="$DIR/$ML_IDENTIFIER"
wenzelm
parents: 3007
diff changeset
    34
  for FILE in "$DIR"/*
2333
f1159f38ba4f findlogics: collect heap names from ISABELLE_PATH;
wenzelm
parents:
diff changeset
    35
  do
f1159f38ba4f findlogics: collect heap names from ISABELLE_PATH;
wenzelm
parents:
diff changeset
    36
    if [ -f "$FILE" ]; then
17792
4a34fd6884b1 support ML_SUFFIX;
wenzelm
parents: 14981
diff changeset
    37
      NAME=$(basename "$FILE" "$ML_SUFFIX")
2333
f1159f38ba4f findlogics: collect heap names from ISABELLE_PATH;
wenzelm
parents:
diff changeset
    38
      LOGICS="$LOGICS $NAME"
f1159f38ba4f findlogics: collect heap names from ISABELLE_PATH;
wenzelm
parents:
diff changeset
    39
    fi
f1159f38ba4f findlogics: collect heap names from ISABELLE_PATH;
wenzelm
parents:
diff changeset
    40
  done
f1159f38ba4f findlogics: collect heap names from ISABELLE_PATH;
wenzelm
parents:
diff changeset
    41
done
9788
wenzelm
parents: 3007
diff changeset
    42
IFS="$ORIG_IFS"
2333
f1159f38ba4f findlogics: collect heap names from ISABELLE_PATH;
wenzelm
parents:
diff changeset
    43
9788
wenzelm
parents: 3007
diff changeset
    44
echo $({ for L in $LOGICS; do echo "$L"; done; } | sort | uniq)