generate outer syntax keyword files from session logs;

--- /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"

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/lib/scripts/keywords.pl	Sat Oct 06 21:25:58 2007 +0200
@@ -0,0 +1,119 @@
+#
+# $Id$
+# Author: Makarius
+#
+# keywords.pl - generate outer syntax keyword files from session logs
+#
+
+## global parameters
+
+my ($keywords_name, $sessions) = @ARGV;
+
+my @kinds = (
+  "major",
+  "minor",
+  "control",
+  "diag",
+  "theory-begin",
+  "theory-switch",
+  "theory-end",
+  "theory-heading",
+  "theory-decl",
+  "theory-script",
+  "theory-goal",
+  "qed",
+  "qed-block",
+  "qed-global",
+  "proof-heading",
+  "proof-goal",
+  "proof-block",
+  "proof-open",
+  "proof-close",
+  "proof-chain",
+  "proof-decl",
+  "proof-asm",
+  "proof-asm-goal",
+  "proof-script"
+);
+
+
+## keywords
+
+my %keywords;
+
+sub set_keyword {
+  my ($name, $kind) = @_;
+  if (defined $keywords{$name} and $keywords{$name} ne $kind) {
+    print STDERR "### Inconsistent declaration of keyword \"${name}\": $keywords{$name} vs ${kind}\n";
+  }
+  $keywords{$name} = $kind;
+}
+
+sub collect_keywords {
+  while(<STDIN>) {
+    if (m/^Outer syntax keyword:\s*"(.*)"/) {
+      my $name = $1;
+      &set_keyword($name, "minor");
+    }
+    elsif (m/^Outer syntax command:\s*"(.*)"\s*\((.*)\)/) {
+      my $name = $1;
+      my $kind = $2;
+      &set_keyword($name, $kind);
+    }
+  }
+}
+
+
+## Emacs output
+
+sub emacs_output {
+  my $file = $keywords_name eq "" ? "isar-keywords.el" : "isar-keywords-${keywords_name}.el";
+  open (OUTPUT, "> ${file}") || die "$!";
+  select OUTPUT;
+
+  print ";;\n";
+  print ";; Keyword classification tables for Isabelle/Isar.\n";
+  print ";; This file was generated from ${sessions} -- DO NOT EDIT!\n";
+  print ";;\n";
+  print ";; \$", "Id\$\n";
+  print ";;\n";
+
+  for my $kind (@kinds) {
+    my @names;
+    for my $name (keys(%keywords)) {
+      if ($kind eq "major" ? $keywords{$name} ne "minor" : $keywords{$name} eq $kind) {
+        if ($kind ne "minor" or $name =~ m/^[A-Za-z0-9_]+$/) {
+          push @names, $name;
+        }
+      }
+    }
+    @names = sort(@names);
+
+    print "\n(defconst isar-keywords-${kind}";
+    print "\n  '(";
+    my $first = 1;
+    for my $name (@names) {
+      $name =~ s/([\.\*\+\?\[\]\^\$])/\\\\$1/g;
+      if ($first) {
+        print "\"${name}\"";
+        $first = 0;
+      }
+      else {
+        print "\n    \"${name}\"";
+      }
+    }
+    print "))\n";
+  }
+  print "\n(provide 'isar-keywords)\n";
+
+  close OUTPUT;
+  select;
+  print STDERR "${file}\n";
+}
+
+
+## main
+
+&collect_keywords();
+&emacs_output();
+