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