lib/Tools/keywords
author wenzelm
Sun, 07 Oct 2007 13:32:15 +0200
changeset 24885 0fc7ba713a27
parent 24879 48e2168b0ea9
child 26576 fc76b7b79ba9
permissions -rwxr-xr-x
added target tool specification; no special treatment of Pure session;
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
#set by configure
8e6ca75bf5aa generate outer syntax keyword files from session logs;
wenzelm
parents:
diff changeset
    61
AUTO_PERL=perl
8e6ca75bf5aa generate outer syntax keyword files from session logs;
wenzelm
parents:
diff changeset
    62
8e6ca75bf5aa generate outer syntax keyword files from session logs;
wenzelm
parents:
diff changeset
    63
SESSIONS=""
8e6ca75bf5aa generate outer syntax keyword files from session logs;
wenzelm
parents:
diff changeset
    64
for LOG in $LOGS
8e6ca75bf5aa generate outer syntax keyword files from session logs;
wenzelm
parents:
diff changeset
    65
do
8e6ca75bf5aa generate outer syntax keyword files from session logs;
wenzelm
parents:
diff changeset
    66
  NAME="$(basename "$LOG" .gz)"
24885
0fc7ba713a27 added target tool specification;
wenzelm
parents: 24879
diff changeset
    67
  if [ -z "$SESSIONS" ]; then
0fc7ba713a27 added target tool specification;
wenzelm
parents: 24879
diff changeset
    68
    SESSIONS="$NAME"
0fc7ba713a27 added target tool specification;
wenzelm
parents: 24879
diff changeset
    69
  else
0fc7ba713a27 added target tool specification;
wenzelm
parents: 24879
diff changeset
    70
    SESSIONS="$SESSIONS + $NAME"
24875
8e6ca75bf5aa generate outer syntax keyword files from session logs;
wenzelm
parents:
diff changeset
    71
  fi
8e6ca75bf5aa generate outer syntax keyword files from session logs;
wenzelm
parents:
diff changeset
    72
done
8e6ca75bf5aa generate outer syntax keyword files from session logs;
wenzelm
parents:
diff changeset
    73
8e6ca75bf5aa generate outer syntax keyword files from session logs;
wenzelm
parents:
diff changeset
    74
for LOG in $LOGS
8e6ca75bf5aa generate outer syntax keyword files from session logs;
wenzelm
parents:
diff changeset
    75
do
8e6ca75bf5aa generate outer syntax keyword files from session logs;
wenzelm
parents:
diff changeset
    76
  if [ "${LOG%.gz}" = "$LOG" ]; then
8e6ca75bf5aa generate outer syntax keyword files from session logs;
wenzelm
parents:
diff changeset
    77
    cat "$LOG"
8e6ca75bf5aa generate outer syntax keyword files from session logs;
wenzelm
parents:
diff changeset
    78
  else
8e6ca75bf5aa generate outer syntax keyword files from session logs;
wenzelm
parents:
diff changeset
    79
    gzip -dc "$LOG"
8e6ca75bf5aa generate outer syntax keyword files from session logs;
wenzelm
parents:
diff changeset
    80
  fi
8e6ca75bf5aa generate outer syntax keyword files from session logs;
wenzelm
parents:
diff changeset
    81
  echo
24885
0fc7ba713a27 added target tool specification;
wenzelm
parents: 24879
diff changeset
    82
done | \
0fc7ba713a27 added target tool specification;
wenzelm
parents: 24879
diff changeset
    83
"$AUTO_PERL" -w "$ISABELLE_HOME/lib/scripts/keywords.pl" "$KEYWORDS_NAME" "$TARGET_TOOL" "$SESSIONS"