lib/Tools/keywords

tuned usage line;

#!/usr/bin/env bash
#
# $Id$
# Author: Makarius
#
# DESCRIPTION: generate outer syntax keyword files from session logs


## diagnostics

PRG="$(basename "$0")"

function usage()
{
  echo
  echo "Usage: isabelle $PRG [OPTIONS] [LOGS ...]"
  echo
  echo "  Options are:"
  echo "    -k NAME      specific name of keywords collection (default: empty)"
  echo "    -t TARGET    target tool (default: emacs)"
  echo
  echo "  Generate outer syntax keyword files from (compressed) session LOGS."
  echo
  exit 1
}


## process command line

# options

KEYWORDS_NAME=""
TARGET_TOOL="emacs"

while getopts "k:t:" OPT
do
  case "$OPT" in
    k)
      KEYWORDS_NAME="$OPTARG"
      ;;
    t)
      TARGET_TOOL="$OPTARG"
      ;;
    \?)
      usage
      ;;
  esac
done

shift $(($OPTIND - 1))


# args

LOGS="$@"; shift "$#"


## main

SESSIONS=""
for LOG in $LOGS
do
  NAME="$(basename "$LOG" .gz)"
  if [ -z "$SESSIONS" ]; then
    SESSIONS="$NAME"
  else
    SESSIONS="$SESSIONS + $NAME"
  fi
done

for LOG in $LOGS
do
  if [ "${LOG%.gz}" = "$LOG" ]; then
    cat "$LOG"
  else
    gzip -dc "$LOG"
  fi
  echo
done | \
perl -w "$ISABELLE_HOME/lib/scripts/keywords.pl" "$KEYWORDS_NAME" "$TARGET_TOOL" "$SESSIONS"