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