lib/Tools/keywords
changeset 24875 8e6ca75bf5aa
child 24879 48e2168b0ea9
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/lib/Tools/keywords	Sat Oct 06 21:25:58 2007 +0200
@@ -0,0 +1,80 @@
+#!/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"