lib/scripts/keywords.pl
author wenzelm
Sat Oct 06 21:25:58 2007 +0200 (2007-10-06)
changeset 24875 8e6ca75bf5aa
child 24886 ce449d6aef3f
permissions -rw-r--r--
generate outer syntax keyword files from session logs;
wenzelm@24875
     1
#
wenzelm@24875
     2
# $Id$
wenzelm@24875
     3
# Author: Makarius
wenzelm@24875
     4
#
wenzelm@24875
     5
# keywords.pl - generate outer syntax keyword files from session logs
wenzelm@24875
     6
#
wenzelm@24875
     7
wenzelm@24875
     8
## global parameters
wenzelm@24875
     9
wenzelm@24875
    10
my ($keywords_name, $sessions) = @ARGV;
wenzelm@24875
    11
wenzelm@24875
    12
my @kinds = (
wenzelm@24875
    13
  "major",
wenzelm@24875
    14
  "minor",
wenzelm@24875
    15
  "control",
wenzelm@24875
    16
  "diag",
wenzelm@24875
    17
  "theory-begin",
wenzelm@24875
    18
  "theory-switch",
wenzelm@24875
    19
  "theory-end",
wenzelm@24875
    20
  "theory-heading",
wenzelm@24875
    21
  "theory-decl",
wenzelm@24875
    22
  "theory-script",
wenzelm@24875
    23
  "theory-goal",
wenzelm@24875
    24
  "qed",
wenzelm@24875
    25
  "qed-block",
wenzelm@24875
    26
  "qed-global",
wenzelm@24875
    27
  "proof-heading",
wenzelm@24875
    28
  "proof-goal",
wenzelm@24875
    29
  "proof-block",
wenzelm@24875
    30
  "proof-open",
wenzelm@24875
    31
  "proof-close",
wenzelm@24875
    32
  "proof-chain",
wenzelm@24875
    33
  "proof-decl",
wenzelm@24875
    34
  "proof-asm",
wenzelm@24875
    35
  "proof-asm-goal",
wenzelm@24875
    36
  "proof-script"
wenzelm@24875
    37
);
wenzelm@24875
    38
wenzelm@24875
    39
wenzelm@24875
    40
## keywords
wenzelm@24875
    41
wenzelm@24875
    42
my %keywords;
wenzelm@24875
    43
wenzelm@24875
    44
sub set_keyword {
wenzelm@24875
    45
  my ($name, $kind) = @_;
wenzelm@24875
    46
  if (defined $keywords{$name} and $keywords{$name} ne $kind) {
wenzelm@24875
    47
    print STDERR "### Inconsistent declaration of keyword \"${name}\": $keywords{$name} vs ${kind}\n";
wenzelm@24875
    48
  }
wenzelm@24875
    49
  $keywords{$name} = $kind;
wenzelm@24875
    50
}
wenzelm@24875
    51
wenzelm@24875
    52
sub collect_keywords {
wenzelm@24875
    53
  while(<STDIN>) {
wenzelm@24875
    54
    if (m/^Outer syntax keyword:\s*"(.*)"/) {
wenzelm@24875
    55
      my $name = $1;
wenzelm@24875
    56
      &set_keyword($name, "minor");
wenzelm@24875
    57
    }
wenzelm@24875
    58
    elsif (m/^Outer syntax command:\s*"(.*)"\s*\((.*)\)/) {
wenzelm@24875
    59
      my $name = $1;
wenzelm@24875
    60
      my $kind = $2;
wenzelm@24875
    61
      &set_keyword($name, $kind);
wenzelm@24875
    62
    }
wenzelm@24875
    63
  }
wenzelm@24875
    64
}
wenzelm@24875
    65
wenzelm@24875
    66
wenzelm@24875
    67
## Emacs output
wenzelm@24875
    68
wenzelm@24875
    69
sub emacs_output {
wenzelm@24875
    70
  my $file = $keywords_name eq "" ? "isar-keywords.el" : "isar-keywords-${keywords_name}.el";
wenzelm@24875
    71
  open (OUTPUT, "> ${file}") || die "$!";
wenzelm@24875
    72
  select OUTPUT;
wenzelm@24875
    73
wenzelm@24875
    74
  print ";;\n";
wenzelm@24875
    75
  print ";; Keyword classification tables for Isabelle/Isar.\n";
wenzelm@24875
    76
  print ";; This file was generated from ${sessions} -- DO NOT EDIT!\n";
wenzelm@24875
    77
  print ";;\n";
wenzelm@24875
    78
  print ";; \$", "Id\$\n";
wenzelm@24875
    79
  print ";;\n";
wenzelm@24875
    80
wenzelm@24875
    81
  for my $kind (@kinds) {
wenzelm@24875
    82
    my @names;
wenzelm@24875
    83
    for my $name (keys(%keywords)) {
wenzelm@24875
    84
      if ($kind eq "major" ? $keywords{$name} ne "minor" : $keywords{$name} eq $kind) {
wenzelm@24875
    85
        if ($kind ne "minor" or $name =~ m/^[A-Za-z0-9_]+$/) {
wenzelm@24875
    86
          push @names, $name;
wenzelm@24875
    87
        }
wenzelm@24875
    88
      }
wenzelm@24875
    89
    }
wenzelm@24875
    90
    @names = sort(@names);
wenzelm@24875
    91
wenzelm@24875
    92
    print "\n(defconst isar-keywords-${kind}";
wenzelm@24875
    93
    print "\n  '(";
wenzelm@24875
    94
    my $first = 1;
wenzelm@24875
    95
    for my $name (@names) {
wenzelm@24875
    96
      $name =~ s/([\.\*\+\?\[\]\^\$])/\\\\$1/g;
wenzelm@24875
    97
      if ($first) {
wenzelm@24875
    98
        print "\"${name}\"";
wenzelm@24875
    99
        $first = 0;
wenzelm@24875
   100
      }
wenzelm@24875
   101
      else {
wenzelm@24875
   102
        print "\n    \"${name}\"";
wenzelm@24875
   103
      }
wenzelm@24875
   104
    }
wenzelm@24875
   105
    print "))\n";
wenzelm@24875
   106
  }
wenzelm@24875
   107
  print "\n(provide 'isar-keywords)\n";
wenzelm@24875
   108
wenzelm@24875
   109
  close OUTPUT;
wenzelm@24875
   110
  select;
wenzelm@24875
   111
  print STDERR "${file}\n";
wenzelm@24875
   112
}
wenzelm@24875
   113
wenzelm@24875
   114
wenzelm@24875
   115
## main
wenzelm@24875
   116
wenzelm@24875
   117
&collect_keywords();
wenzelm@24875
   118
&emacs_output();
wenzelm@24875
   119