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