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