lib/Tools/findlogics
author wenzelm
Thu Apr 24 00:29:55 2014 +0200 (2014-04-24)
changeset 56686 2386d1a3ca8f
parent 33915 44a10fe6bd10
child 57414 fe1be2844fda
permissions -rwxr-xr-x
canonical list operations, as in ML;
avoid odd mutable data structures;
wenzelm@10555
     1
#!/usr/bin/env bash
wenzelm@2333
     2
#
wenzelm@9788
     3
# Author: Markus Wenzel, TU Muenchen
wenzelm@2333
     4
#
wenzelm@2333
     5
# DESCRIPTION: collect heap names from ISABELLE_PATH
wenzelm@2333
     6
wenzelm@2333
     7
wenzelm@9788
     8
PRG=$(basename "$0")
wenzelm@2333
     9
wenzelm@2333
    10
function usage()
wenzelm@2333
    11
{
wenzelm@2333
    12
  echo
wenzelm@28650
    13
  echo "Usage: isabelle $PRG"
wenzelm@2333
    14
  echo
wenzelm@2333
    15
  echo "  Collect heap file names from ISABELLE_PATH."
wenzelm@2333
    16
  echo
wenzelm@2333
    17
  exit 1
wenzelm@2333
    18
}
wenzelm@2333
    19
wenzelm@2333
    20
wenzelm@2333
    21
## main
wenzelm@2333
    22
wenzelm@9788
    23
[ "$#" -ne 0 ] && usage
wenzelm@2333
    24
wenzelm@32322
    25
declare -a LOGICS=()
wenzelm@32322
    26
declare -a ISABELLE_PATHS=()
wenzelm@2333
    27
wenzelm@32390
    28
splitarray ":" "$ISABELLE_PATH"; ISABELLE_PATHS=("${SPLITARRAY[@]}")
wenzelm@32322
    29
wenzelm@32322
    30
for DIR in "${ISABELLE_PATHS[@]}"
wenzelm@2333
    31
do
wenzelm@9788
    32
  DIR="$DIR/$ML_IDENTIFIER"
wenzelm@9788
    33
  for FILE in "$DIR"/*
wenzelm@2333
    34
  do
wenzelm@2333
    35
    if [ -f "$FILE" ]; then
wenzelm@27201
    36
      NAME=$(basename "$FILE")
wenzelm@32391
    37
      LOGICS["${#LOGICS[@]}"]="$NAME"
wenzelm@2333
    38
    fi
wenzelm@2333
    39
  done
wenzelm@2333
    40
done
wenzelm@2333
    41
wenzelm@33915
    42
echo $({ for L in "${LOGICS[@]}"; do echo "$L"; done; } | sort | uniq)