lib/Tools/findlogics
author wenzelm
Sun, 20 Jan 2013 13:59:13 +0100
changeset 50990 11996ea98bbe
parent 33915 44a10fe6bd10
child 57414 fe1be2844fda
permissions -rwxr-xr-x
tuned;
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
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
f1159f38ba4f findlogics: collect heap names from ISABELLE_PATH;
wenzelm
parents:
diff changeset
    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
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")
32391
5b9d7e578756 less ambitious array operations -- for improved compatibility with older versions of bash;
wenzelm
parents: 32390
diff changeset
    37
      LOGICS["${#LOGICS[@]}"]="$NAME"
2333
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
f1159f38ba4f findlogics: collect heap names from ISABELLE_PATH;
wenzelm
parents:
diff changeset
    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)