lib/Tools/keywords

generate outer syntax keyword files from session logs;

#!/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: $PRG [OPTIONS] [LOGS ...]"
  echo
  echo "  Options are:"
  echo "    -k NAME      specific name of keywords collection (default: empty)"
  echo
  echo "  Generate outer syntax keyword files from (compressed) session LOGS."
  echo "  Targets Emacs Proof General."
  echo
  exit 1
}


## process command line

# options

KEYWORDS_NAME=""

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

shift $(($OPTIND - 1))


# args

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


## main

#set by configure
AUTO_PERL=perl

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

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