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