| 24875 |      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
 | 
| 28650 |     15 |   echo "Usage: isabelle $PRG [OPTIONS] [LOGS ...]"
 | 
| 24875 |     16 |   echo
 | 
|  |     17 |   echo "  Options are:"
 | 
|  |     18 |   echo "    -k NAME      specific name of keywords collection (default: empty)"
 | 
| 24885 |     19 |   echo "    -t TARGET    target tool (default: emacs)"
 | 
| 24875 |     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=""
 | 
| 24885 |     32 | TARGET_TOOL="emacs"
 | 
| 24875 |     33 | 
 | 
| 24885 |     34 | while getopts "k:t:" OPT
 | 
| 24875 |     35 | do
 | 
|  |     36 |   case "$OPT" in
 | 
|  |     37 |     k)
 | 
|  |     38 |       KEYWORDS_NAME="$OPTARG"
 | 
|  |     39 |       ;;
 | 
| 24885 |     40 |     t)
 | 
|  |     41 |       TARGET_TOOL="$OPTARG"
 | 
|  |     42 |       ;;
 | 
| 24875 |     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)"
 | 
| 24885 |     63 |   if [ -z "$SESSIONS" ]; then
 | 
|  |     64 |     SESSIONS="$NAME"
 | 
|  |     65 |   else
 | 
|  |     66 |     SESSIONS="$SESSIONS + $NAME"
 | 
| 24875 |     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
 | 
| 24885 |     78 | done | \
 | 
| 26576 |     79 | perl -w "$ISABELLE_HOME/lib/scripts/keywords.pl" "$KEYWORDS_NAME" "$TARGET_TOOL" "$SESSIONS"
 |