lib/scripts/keywords.pl
author wenzelm
Sat Dec 20 11:55:34 2008 +0100 (2008-12-20)
changeset 29145 b1c6f4563df7
parent 27386 d10ec4969b9f
child 33684 29d8aaeb56e5
permissions -rw-r--r--
removed Ids;
     1 #
     2 # Author: Makarius
     3 #
     4 # keywords.pl - generate outer syntax keyword files from session logs
     5 #
     6 
     7 ## arguments
     8 
     9 my ($keywords_name, $target_tool, $sessions) = @ARGV;
    10 
    11 
    12 ## keywords
    13 
    14 my %keywords;
    15 
    16 sub set_keyword {
    17   my ($name, $kind) = @_;
    18   if (defined $keywords{$name} and $keywords{$name} ne $kind and $keywords{$name} ne "minor") {
    19     if ($kind ne "minor") {
    20       print STDERR "### Inconsistent declaration of keyword \"${name}\": $keywords{$name} vs ${kind}\n";
    21       $keywords{$name} = $kind;
    22     }
    23   } else {
    24     $keywords{$name} = $kind;
    25   }
    26 }
    27 
    28 sub collect_keywords {
    29   while(<STDIN>) {
    30     if (m/^Outer syntax keyword:\s*"(.*)"/) {
    31       my $name = $1;
    32       &set_keyword($name, "minor");
    33     }
    34     elsif (m/^Outer syntax command:\s*"(.*)"\s*\((.*)\)/) {
    35       my $name = $1;
    36       my $kind = $2;
    37       &set_keyword($name, $kind);
    38     }
    39   }
    40 }
    41 
    42 
    43 ## Emacs output
    44 
    45 sub emacs_output {
    46   my @kinds = (
    47     "major",
    48     "minor",
    49     "control",
    50     "diag",
    51     "theory-begin",
    52     "theory-switch",
    53     "theory-end",
    54     "theory-heading",
    55     "theory-decl",
    56     "theory-script",
    57     "theory-goal",
    58     "qed",
    59     "qed-block",
    60     "qed-global",
    61     "proof-heading",
    62     "proof-goal",
    63     "proof-block",
    64     "proof-open",
    65     "proof-close",
    66     "proof-chain",
    67     "proof-decl",
    68     "proof-asm",
    69     "proof-asm-goal",
    70     "proof-script"
    71   );
    72   my $file = $keywords_name eq "" ? "isar-keywords.el" : "isar-keywords-${keywords_name}.el";
    73   open (OUTPUT, "> ${file}") || die "$!";
    74   select OUTPUT;
    75 
    76   print ";;\n";
    77   print ";; Keyword classification tables for Isabelle/Isar.\n";
    78   print ";; Generated from ${sessions}.\n";
    79   print ";; *** DO NOT EDIT *** DO NOT EDIT *** DO NOT EDIT ***\n";
    80   print ";;\n";
    81 
    82   for my $kind (@kinds) {
    83     my @names;
    84     for my $name (keys(%keywords)) {
    85       if ($kind eq "major" ? $keywords{$name} ne "minor" : $keywords{$name} eq $kind) {
    86         if ($kind ne "minor" or $name =~ m/^[A-Za-z0-9_]+$/) {
    87           push @names, $name;
    88         }
    89       }
    90     }
    91     @names = sort(@names);
    92 
    93     print "\n(defconst isar-keywords-${kind}";
    94     print "\n  '(";
    95     my $first = 1;
    96     for my $name (@names) {
    97       $name =~ s/([\.\*\+\?\[\]\^\$])/\\\\$1/g;
    98       if ($first) {
    99         print "\"${name}\"";
   100         $first = 0;
   101       }
   102       else {
   103         print "\n    \"${name}\"";
   104       }
   105     }
   106     print "))\n";
   107   }
   108   print "\n(provide 'isar-keywords)\n";
   109 
   110   close OUTPUT;
   111   select;
   112   print STDERR "${target_tool}: ${file}\n";
   113 }
   114 
   115 
   116 ## jEdit output
   117 
   118 sub jedit_output {
   119   my %keyword_types = (
   120     "minor"           => "KEYWORD4",
   121     "control"         => "INVALID",
   122     "diag"            => "LABEL",
   123     "theory-begin"    => "KEYWORD3",
   124     "theory-switch"   => "KEYWORD3",
   125     "theory-end"      => "KEYWORD3",
   126     "theory-heading"  => "OPERATOR",
   127     "theory-decl"     => "OPERATOR",
   128     "theory-script"   => "KEYWORD1",
   129     "theory-goal"     => "OPERATOR",
   130     "qed"             => "OPERATOR",
   131     "qed-block"       => "OPERATOR",
   132     "qed-global"      => "OPERATOR",
   133     "proof-heading"   => "OPERATOR",
   134     "proof-goal"      => "OPERATOR",
   135     "proof-block"     => "OPERATOR",
   136     "proof-open"      => "OPERATOR",
   137     "proof-close"     => "OPERATOR",
   138     "proof-chain"     => "OPERATOR",
   139     "proof-decl"      => "OPERATOR",
   140     "proof-asm"       => "KEYWORD2",
   141     "proof-asm-goal"  => "KEYWORD2",
   142     "proof-script"    => "KEYWORD1"
   143   );
   144   my $file = "isabelle.xml";
   145   open (OUTPUT, "> ${file}") || die "$!";
   146   select OUTPUT;
   147 
   148   print <<'EOF';
   149 <?xml version="1.0"?>
   150 <!DOCTYPE MODE SYSTEM "xmode.dtd">
   151 EOF
   152   print "<!-- Generated from ${sessions}. -->\n";
   153   print "<!-- *** DO NOT EDIT *** DO NOT EDIT *** DO NOT EDIT *** -->\n";
   154   print <<'EOF';
   155 <MODE>
   156   <PROPS>
   157     <PROPERTY NAME="commentStart" VALUE="(*"/>
   158     <PROPERTY NAME="commentEnd" VALUE="*)"/>
   159     <PROPERTY NAME="noWordSep" VALUE="_'.?"/>
   160     <PROPERTY NAME="indentOpenBrackets" VALUE="{"/>
   161     <PROPERTY NAME="indentCloseBrackets" VALUE="}"/>
   162     <PROPERTY NAME="unalignedOpenBrackets" VALUE="(" />
   163     <PROPERTY NAME="unalignedCloseBrackets" VALUE=")" />
   164     <PROPERTY NAME="tabSize" VALUE="2" />
   165     <PROPERTY NAME="indentSize" VALUE="2" />
   166   </PROPS>
   167   <RULES IGNORE_CASE="FALSE" HIGHLIGHT_DIGITS="FALSE" ESCAPE="\">
   168     <SPAN TYPE="COMMENT1" NO_ESCAPE="TRUE">
   169       <BEGIN>(*</BEGIN>
   170       <END>*)</END>
   171     </SPAN>
   172     <SPAN TYPE="COMMENT3" NO_ESCAPE="TRUE">
   173       <BEGIN>{*</BEGIN>
   174       <END>*}</END>
   175     </SPAN>
   176     <SPAN TYPE="LITERAL1">
   177       <BEGIN>`</BEGIN>
   178       <END>`</END>
   179     </SPAN>
   180     <SPAN TYPE="LITERAL3">
   181       <BEGIN>"</BEGIN>
   182       <END>"</END>
   183     </SPAN>
   184     <KEYWORDS>
   185 EOF
   186 
   187   for my $name (sort(keys(%keywords))) {
   188     my $kind = $keywords{$name};
   189     my $type = $keyword_types{$kind};
   190     if ($kind ne "minor" or $name =~ m/^[A-Za-z0-9_]+$/) {
   191       $name =~ s/&/&amp;/g;
   192       $name =~ s/</&lt;/g;
   193       $name =~ s/>/&lt;/g;
   194       print "      <${type}>${name}</${type}>\n";
   195     }
   196   }
   197 
   198   print <<'EOF';
   199     </KEYWORDS>
   200   </RULES>
   201 </MODE>
   202 EOF
   203 
   204   close OUTPUT;
   205   select;
   206   print STDERR "${target_tool}: ${file}\n";
   207 }
   208 
   209 
   210 ## main
   211 
   212 &collect_keywords();
   213 eval "${target_tool}_output()";
   214