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