lib/Tools/keywords
author wenzelm
Sat Jul 25 10:31:27 2009 +0200 (2009-07-25)
changeset 32187 cca43ca13f4f
parent 29143 72c960b2b83e
child 33684 29d8aaeb56e5
permissions -rwxr-xr-x
renamed structure Display_Goal to Goal_Display;
wenzelm@24875
     1
#!/usr/bin/env bash
wenzelm@24875
     2
#
wenzelm@24875
     3
# Author: Makarius
wenzelm@24875
     4
#
wenzelm@24875
     5
# DESCRIPTION: generate outer syntax keyword files from session logs
wenzelm@24875
     6
wenzelm@24875
     7
wenzelm@24875
     8
## diagnostics
wenzelm@24875
     9
wenzelm@24875
    10
PRG="$(basename "$0")"
wenzelm@24875
    11
wenzelm@24875
    12
function usage()
wenzelm@24875
    13
{
wenzelm@24875
    14
  echo
wenzelm@28650
    15
  echo "Usage: isabelle $PRG [OPTIONS] [LOGS ...]"
wenzelm@24875
    16
  echo
wenzelm@24875
    17
  echo "  Options are:"
wenzelm@24875
    18
  echo "    -k NAME      specific name of keywords collection (default: empty)"
wenzelm@24885
    19
  echo "    -t TARGET    target tool (default: emacs)"
wenzelm@24875
    20
  echo
wenzelm@24875
    21
  echo "  Generate outer syntax keyword files from (compressed) session LOGS."
wenzelm@24875
    22
  echo
wenzelm@24875
    23
  exit 1
wenzelm@24875
    24
}
wenzelm@24875
    25
wenzelm@24875
    26
wenzelm@24875
    27
## process command line
wenzelm@24875
    28
wenzelm@24875
    29
# options
wenzelm@24875
    30
wenzelm@24875
    31
KEYWORDS_NAME=""
wenzelm@24885
    32
TARGET_TOOL="emacs"
wenzelm@24875
    33
wenzelm@24885
    34
while getopts "k:t:" OPT
wenzelm@24875
    35
do
wenzelm@24875
    36
  case "$OPT" in
wenzelm@24875
    37
    k)
wenzelm@24875
    38
      KEYWORDS_NAME="$OPTARG"
wenzelm@24875
    39
      ;;
wenzelm@24885
    40
    t)
wenzelm@24885
    41
      TARGET_TOOL="$OPTARG"
wenzelm@24885
    42
      ;;
wenzelm@24875
    43
    \?)
wenzelm@24875
    44
      usage
wenzelm@24875
    45
      ;;
wenzelm@24875
    46
  esac
wenzelm@24875
    47
done
wenzelm@24875
    48
wenzelm@24875
    49
shift $(($OPTIND - 1))
wenzelm@24875
    50
wenzelm@24875
    51
wenzelm@24875
    52
# args
wenzelm@24875
    53
wenzelm@24875
    54
LOGS="$@"; shift "$#"
wenzelm@24875
    55
wenzelm@24875
    56
wenzelm@24875
    57
## main
wenzelm@24875
    58
wenzelm@24875
    59
SESSIONS=""
wenzelm@24875
    60
for LOG in $LOGS
wenzelm@24875
    61
do
wenzelm@24875
    62
  NAME="$(basename "$LOG" .gz)"
wenzelm@24885
    63
  if [ -z "$SESSIONS" ]; then
wenzelm@24885
    64
    SESSIONS="$NAME"
wenzelm@24885
    65
  else
wenzelm@24885
    66
    SESSIONS="$SESSIONS + $NAME"
wenzelm@24875
    67
  fi
wenzelm@24875
    68
done
wenzelm@24875
    69
wenzelm@24875
    70
for LOG in $LOGS
wenzelm@24875
    71
do
wenzelm@24875
    72
  if [ "${LOG%.gz}" = "$LOG" ]; then
wenzelm@24875
    73
    cat "$LOG"
wenzelm@24875
    74
  else
wenzelm@24875
    75
    gzip -dc "$LOG"
wenzelm@24875
    76
  fi
wenzelm@24875
    77
  echo
wenzelm@24885
    78
done | \
wenzelm@26576
    79
perl -w "$ISABELLE_HOME/lib/scripts/keywords.pl" "$KEYWORDS_NAME" "$TARGET_TOOL" "$SESSIONS"