lib/Tools/findlogics
author wenzelm
Thu, 04 Jun 2009 17:31:38 +0200
changeset 31427 5a07cc86675d
parent 29143 72c960b2b83e
child 32322 45cb4a86eca2
permissions -rwxr-xr-x
reraise exceptions to preserve original position (ML system specific);
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
#
9788
wenzelm
parents: 3007
diff changeset
     3
# Author: Markus Wenzel, TU Muenchen
2333
f1159f38ba4f findlogics: collect heap names from ISABELLE_PATH;
wenzelm
parents:
diff changeset
     4
#
f1159f38ba4f findlogics: collect heap names from ISABELLE_PATH;
wenzelm
parents:
diff changeset
     5
# DESCRIPTION: collect heap names from ISABELLE_PATH
f1159f38ba4f findlogics: collect heap names from ISABELLE_PATH;
wenzelm
parents:
diff changeset
     6
f1159f38ba4f findlogics: collect heap names from ISABELLE_PATH;
wenzelm
parents:
diff changeset
     7
9788
wenzelm
parents: 3007
diff changeset
     8
PRG=$(basename "$0")
2333
f1159f38ba4f findlogics: collect heap names from ISABELLE_PATH;
wenzelm
parents:
diff changeset
     9
f1159f38ba4f findlogics: collect heap names from ISABELLE_PATH;
wenzelm
parents:
diff changeset
    10
function usage()
f1159f38ba4f findlogics: collect heap names from ISABELLE_PATH;
wenzelm
parents:
diff changeset
    11
{
f1159f38ba4f findlogics: collect heap names from ISABELLE_PATH;
wenzelm
parents:
diff changeset
    12
  echo
28650
a7ba12e0d3b7 tuned usage line;
wenzelm
parents: 27201
diff changeset
    13
  echo "Usage: isabelle $PRG"
2333
f1159f38ba4f findlogics: collect heap names from ISABELLE_PATH;
wenzelm
parents:
diff changeset
    14
  echo
f1159f38ba4f findlogics: collect heap names from ISABELLE_PATH;
wenzelm
parents:
diff changeset
    15
  echo "  Collect heap file names from ISABELLE_PATH."
f1159f38ba4f findlogics: collect heap names from ISABELLE_PATH;
wenzelm
parents:
diff changeset
    16
  echo
f1159f38ba4f findlogics: collect heap names from ISABELLE_PATH;
wenzelm
parents:
diff changeset
    17
  exit 1
f1159f38ba4f findlogics: collect heap names from ISABELLE_PATH;
wenzelm
parents:
diff changeset
    18
}
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
## main
f1159f38ba4f findlogics: collect heap names from ISABELLE_PATH;
wenzelm
parents:
diff changeset
    22
9788
wenzelm
parents: 3007
diff changeset
    23
[ "$#" -ne 0 ] && usage
2333
f1159f38ba4f findlogics: collect heap names from ISABELLE_PATH;
wenzelm
parents:
diff changeset
    24
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
LOGICS=""
f1159f38ba4f findlogics: collect heap names from ISABELLE_PATH;
wenzelm
parents:
diff changeset
    27
9788
wenzelm
parents: 3007
diff changeset
    28
ORIG_IFS="$IFS"
wenzelm
parents: 3007
diff changeset
    29
IFS=":"
wenzelm
parents: 3007
diff changeset
    30
for DIR in $ISABELLE_PATH
2333
f1159f38ba4f findlogics: collect heap names from ISABELLE_PATH;
wenzelm
parents:
diff changeset
    31
do
9788
wenzelm
parents: 3007
diff changeset
    32
  DIR="$DIR/$ML_IDENTIFIER"
wenzelm
parents: 3007
diff changeset
    33
  for FILE in "$DIR"/*
2333
f1159f38ba4f findlogics: collect heap names from ISABELLE_PATH;
wenzelm
parents:
diff changeset
    34
  do
f1159f38ba4f findlogics: collect heap names from ISABELLE_PATH;
wenzelm
parents:
diff changeset
    35
    if [ -f "$FILE" ]; then
27201
e0323036bcf2 removed obsolete ML_SUFFIX;
wenzelm
parents: 17792
diff changeset
    36
      NAME=$(basename "$FILE")
2333
f1159f38ba4f findlogics: collect heap names from ISABELLE_PATH;
wenzelm
parents:
diff changeset
    37
      LOGICS="$LOGICS $NAME"
f1159f38ba4f findlogics: collect heap names from ISABELLE_PATH;
wenzelm
parents:
diff changeset
    38
    fi
f1159f38ba4f findlogics: collect heap names from ISABELLE_PATH;
wenzelm
parents:
diff changeset
    39
  done
f1159f38ba4f findlogics: collect heap names from ISABELLE_PATH;
wenzelm
parents:
diff changeset
    40
done
9788
wenzelm
parents: 3007
diff changeset
    41
IFS="$ORIG_IFS"
2333
f1159f38ba4f findlogics: collect heap names from ISABELLE_PATH;
wenzelm
parents:
diff changeset
    42
9788
wenzelm
parents: 3007
diff changeset
    43
echo $({ for L in $LOGICS; do echo "$L"; done; } | sort | uniq)