equal
deleted
inserted
replaced
1 # |
1 # |
2 # $Id$ |
|
3 # Author: Makarius |
2 # Author: Makarius |
4 # |
3 # |
5 # keywords.pl - generate outer syntax keyword files from session logs |
4 # keywords.pl - generate outer syntax keyword files from session logs |
6 # |
5 # |
7 |
6 |
77 print ";;\n"; |
76 print ";;\n"; |
78 print ";; Keyword classification tables for Isabelle/Isar.\n"; |
77 print ";; Keyword classification tables for Isabelle/Isar.\n"; |
79 print ";; Generated from ${sessions}.\n"; |
78 print ";; Generated from ${sessions}.\n"; |
80 print ";; *** DO NOT EDIT *** DO NOT EDIT *** DO NOT EDIT ***\n"; |
79 print ";; *** DO NOT EDIT *** DO NOT EDIT *** DO NOT EDIT ***\n"; |
81 print ";;\n"; |
80 print ";;\n"; |
82 print ";; \$", "Id\$\n"; |
|
83 print ";;\n"; |
|
84 |
81 |
85 for my $kind (@kinds) { |
82 for my $kind (@kinds) { |
86 my @names; |
83 my @names; |
87 for my $name (keys(%keywords)) { |
84 for my $name (keys(%keywords)) { |
88 if ($kind eq "major" ? $keywords{$name} ne "minor" : $keywords{$name} eq $kind) { |
85 if ($kind eq "major" ? $keywords{$name} ne "minor" : $keywords{$name} eq $kind) { |
152 <?xml version="1.0"?> |
149 <?xml version="1.0"?> |
153 <!DOCTYPE MODE SYSTEM "xmode.dtd"> |
150 <!DOCTYPE MODE SYSTEM "xmode.dtd"> |
154 EOF |
151 EOF |
155 print "<!-- Generated from ${sessions}. -->\n"; |
152 print "<!-- Generated from ${sessions}. -->\n"; |
156 print "<!-- *** DO NOT EDIT *** DO NOT EDIT *** DO NOT EDIT *** -->\n"; |
153 print "<!-- *** DO NOT EDIT *** DO NOT EDIT *** DO NOT EDIT *** -->\n"; |
157 print "<!-- \$", "Id\$ -->\n"; |
|
158 print <<'EOF'; |
154 print <<'EOF'; |
159 <MODE> |
155 <MODE> |
160 <PROPS> |
156 <PROPS> |
161 <PROPERTY NAME="commentStart" VALUE="(*"/> |
157 <PROPERTY NAME="commentStart" VALUE="(*"/> |
162 <PROPERTY NAME="commentEnd" VALUE="*)"/> |
158 <PROPERTY NAME="commentEnd" VALUE="*)"/> |