1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/lib/Tools/keywords	Sat Oct 06 21:25:58 2007 +0200
     1.3 @@ -0,0 +1,80 @@
     1.4 +#!/usr/bin/env bash
     1.5 +#
     1.6 +# $Id$
     1.7 +# Author: Makarius
     1.8 +#
     1.9 +# DESCRIPTION: generate outer syntax keyword files from session logs
    1.10 +
    1.11 +
    1.12 +## diagnostics
    1.13 +
    1.14 +PRG="$(basename "$0")"
    1.15 +
    1.16 +function usage()
    1.17 +{
    1.18 +  echo
    1.19 +  echo "Usage: $PRG [OPTIONS] [LOGS ...]"
    1.20 +  echo
    1.21 +  echo "  Options are:"
    1.22 +  echo "    -k NAME      specific name of keywords collection (default: empty)"
    1.23 +  echo
    1.24 +  echo "  Generate outer syntax keyword files from (compressed) session LOGS."
    1.25 +  echo "  Targets Emacs Proof General."
    1.26 +  echo
    1.27 +  exit 1
    1.28 +}
    1.29 +
    1.30 +
    1.31 +## process command line
    1.32 +
    1.33 +# options
    1.34 +
    1.35 +KEYWORDS_NAME=""
    1.36 +
    1.37 +while getopts "k:" OPT
    1.38 +do
    1.39 +  case "$OPT" in
    1.40 +    k)
    1.41 +      KEYWORDS_NAME="$OPTARG"
    1.42 +      ;;
    1.43 +    \?)
    1.44 +      usage
    1.45 +      ;;
    1.46 +  esac
    1.47 +done
    1.48 +
    1.49 +shift $(($OPTIND - 1))
    1.50 +
    1.51 +
    1.52 +# args
    1.53 +
    1.54 +LOGS="$@"; shift "$#"
    1.55 +
    1.56 +
    1.57 +## main
    1.58 +
    1.59 +#set by configure
    1.60 +AUTO_PERL=perl
    1.61 +
    1.62 +SESSIONS=""
    1.63 +for LOG in $LOGS
    1.64 +do
    1.65 +  NAME="$(basename "$LOG" .gz)"
    1.66 +  if [ "$NAME" != PG -a "$NAME" != Pure ]; then
    1.67 +    if [ -z "$SESSIONS" ]; then
    1.68 +      SESSIONS="$NAME"
    1.69 +    else
    1.70 +      SESSIONS="$SESSIONS + $NAME"
    1.71 +    fi
    1.72 +  fi
    1.73 +done
    1.74 +
    1.75 +for LOG in $LOGS
    1.76 +do
    1.77 +  if [ "${LOG%.gz}" = "$LOG" ]; then
    1.78 +    cat "$LOG"
    1.79 +  else
    1.80 +    gzip -dc "$LOG"
    1.81 +  fi
    1.82 +  echo
    1.83 +done | "$AUTO_PERL" -w "$ISABELLE_HOME/lib/scripts/keywords.pl" "$KEYWORDS_NAME" "$SESSIONS"

     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/lib/scripts/keywords.pl	Sat Oct 06 21:25:58 2007 +0200
     2.3 @@ -0,0 +1,119 @@
     2.4 +#
     2.5 +# $Id$
     2.6 +# Author: Makarius
     2.7 +#
     2.8 +# keywords.pl - generate outer syntax keyword files from session logs
     2.9 +#
    2.10 +
    2.11 +## global parameters
    2.12 +
    2.13 +my ($keywords_name, $sessions) = @ARGV;
    2.14 +
    2.15 +my @kinds = (
    2.16 +  "major",
    2.17 +  "minor",
    2.18 +  "control",
    2.19 +  "diag",
    2.20 +  "theory-begin",
    2.21 +  "theory-switch",
    2.22 +  "theory-end",
    2.23 +  "theory-heading",
    2.24 +  "theory-decl",
    2.25 +  "theory-script",
    2.26 +  "theory-goal",
    2.27 +  "qed",
    2.28 +  "qed-block",
    2.29 +  "qed-global",
    2.30 +  "proof-heading",
    2.31 +  "proof-goal",
    2.32 +  "proof-block",
    2.33 +  "proof-open",
    2.34 +  "proof-close",
    2.35 +  "proof-chain",
    2.36 +  "proof-decl",
    2.37 +  "proof-asm",
    2.38 +  "proof-asm-goal",
    2.39 +  "proof-script"
    2.40 +);
    2.41 +
    2.42 +
    2.43 +## keywords
    2.44 +
    2.45 +my %keywords;
    2.46 +
    2.47 +sub set_keyword {
    2.48 +  my ($name, $kind) = @_;
    2.49 +  if (defined $keywords{$name} and $keywords{$name} ne $kind) {
    2.50 +    print STDERR "### Inconsistent declaration of keyword \"${name}\": $keywords{$name} vs ${kind}\n";
    2.51 +  }
    2.52 +  $keywords{$name} = $kind;
    2.53 +}
    2.54 +
    2.55 +sub collect_keywords {
    2.56 +  while(<STDIN>) {
    2.57 +    if (m/^Outer syntax keyword:\s*"(.*)"/) {
    2.58 +      my $name = $1;
    2.59 +      &set_keyword($name, "minor");
    2.60 +    }
    2.61 +    elsif (m/^Outer syntax command:\s*"(.*)"\s*\((.*)\)/) {
    2.62 +      my $name = $1;
    2.63 +      my $kind = $2;
    2.64 +      &set_keyword($name, $kind);
    2.65 +    }
    2.66 +  }
    2.67 +}
    2.68 +
    2.69 +
    2.70 +## Emacs output
    2.71 +
    2.72 +sub emacs_output {
    2.73 +  my $file = $keywords_name eq "" ? "isar-keywords.el" : "isar-keywords-${keywords_name}.el";
    2.74 +  open (OUTPUT, "> ${file}") || die "$!";
    2.75 +  select OUTPUT;
    2.76 +
    2.77 +  print ";;\n";
    2.78 +  print ";; Keyword classification tables for Isabelle/Isar.\n";
    2.79 +  print ";; This file was generated from ${sessions} -- DO NOT EDIT!\n";
    2.80 +  print ";;\n";
    2.81 +  print ";; \$", "Id\$\n";
    2.82 +  print ";;\n";
    2.83 +
    2.84 +  for my $kind (@kinds) {
    2.85 +    my @names;
    2.86 +    for my $name (keys(%keywords)) {
    2.87 +      if ($kind eq "major" ? $keywords{$name} ne "minor" : $keywords{$name} eq $kind) {
    2.88 +        if ($kind ne "minor" or $name =~ m/^[A-Za-z0-9_]+$/) {
    2.89 +          push @names, $name;
    2.90 +        }
    2.91 +      }
    2.92 +    }
    2.93 +    @names = sort(@names);
    2.94 +
    2.95 +    print "\n(defconst isar-keywords-${kind}";
    2.96 +    print "\n  '(";
    2.97 +    my $first = 1;
    2.98 +    for my $name (@names) {
    2.99 +      $name =~ s/([\.\*\+\?\[\]\^\$])/\\\\$1/g;
   2.100 +      if ($first) {
   2.101 +        print "\"${name}\"";
   2.102 +        $first = 0;
   2.103 +      }
   2.104 +      else {
   2.105 +        print "\n    \"${name}\"";
   2.106 +      }
   2.107 +    }
   2.108 +    print "))\n";
   2.109 +  }
   2.110 +  print "\n(provide 'isar-keywords)\n";
   2.111 +
   2.112 +  close OUTPUT;
   2.113 +  select;
   2.114 +  print STDERR "${file}\n";
   2.115 +}
   2.116 +
   2.117 +
   2.118 +## main
   2.119 +
   2.120 +&collect_keywords();
   2.121 +&emacs_output();
   2.122 +