4 # keywords.pl - generate outer syntax keyword files from session logs
9 my ($keywords_name, $target_tool, $sessions) = @ARGV;
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;
24 $keywords{$name} = $kind;
28 sub collect_keywords {
30 if (m/^Outer syntax keyword:\s*"(.*)"/) {
32 &set_keyword($name, "minor");
34 elsif (m/^Outer syntax command:\s*"(.*)"\s*\((.*)\)/) {
37 &set_keyword($name, $kind);
72 my $file = $keywords_name eq "" ? "isar-keywords.el" : "isar-keywords-${keywords_name}.el";
73 open (OUTPUT, "> ${file}") || die "$!";
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";
82 for my $kind (@kinds) {
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_]+$/) {
91 @names = sort(@names);
93 print "\n(defconst isar-keywords-${kind}";
96 for my $name (@names) {
97 $name =~ s/([\.\*\+\?\[\]\^\$])/\\\\$1/g;
103 print "\n \"${name}\"";
108 print "\n(provide 'isar-keywords)\n";
112 print STDERR "${target_tool}: ${file}\n";
119 my %keyword_types = (
120 "minor" => "KEYWORD4",
121 "control" => "INVALID",
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",
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"
144 my $file = "isabelle.xml";
145 open (OUTPUT, "> ${file}") || die "$!";
149 <?xml version="1.0"?>
150 <!DOCTYPE MODE SYSTEM "xmode.dtd">
152 print "<!-- Generated from ${sessions}. -->\n";
153 print "<!-- *** DO NOT EDIT *** DO NOT EDIT *** DO NOT EDIT *** -->\n";
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" />
167 <RULES IGNORE_CASE="FALSE" HIGHLIGHT_DIGITS="FALSE" ESCAPE="\">
168 <SPAN TYPE="COMMENT1" NO_ESCAPE="TRUE">
172 <SPAN TYPE="COMMENT3" NO_ESCAPE="TRUE">
176 <SPAN TYPE="LITERAL1">
180 <SPAN TYPE="LITERAL3">
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/&/&/g;
194 print " <${type}>${name}</${type}>\n";
206 print STDERR "${target_tool}: ${file}\n";
213 eval "${target_tool}_output()";