lib/Tools/keywords

clarified "state" (accumulated data) vs. "exec" (execution that produces data);
generic type Document.id (ML) / Document.ID;

#!/usr/bin/env bash
#
# 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
  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))


## main

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

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