equal
deleted
inserted
replaced
70 open (OUTPUT, "> ${file}") || die "$!"; |
70 open (OUTPUT, "> ${file}") || die "$!"; |
71 select OUTPUT; |
71 select OUTPUT; |
72 |
72 |
73 print ";;\n"; |
73 print ";;\n"; |
74 print ";; Keyword classification tables for Isabelle/Isar.\n"; |
74 print ";; Keyword classification tables for Isabelle/Isar.\n"; |
75 print ";; This file was generated from ${sessions} -- DO NOT EDIT!\n"; |
75 print ";; Generated from ${sessions}\n"; |
|
76 print ";; *** DO NOT EDIT *** DO NOT EDIT *** DO NOT EDIT ***\n"; |
76 print ";;\n"; |
77 print ";;\n"; |
77 print ";; \$", "Id\$\n"; |
78 print ";; \$", "Id\$\n"; |
78 print ";;\n"; |
79 print ";;\n"; |
79 |
80 |
80 for my $kind (@kinds) { |
81 for my $kind (@kinds) { |
145 |
146 |
146 print <<'EOF'; |
147 print <<'EOF'; |
147 <?xml version="1.0"?> |
148 <?xml version="1.0"?> |
148 <!DOCTYPE MODE SYSTEM "xmode.dtd"> |
149 <!DOCTYPE MODE SYSTEM "xmode.dtd"> |
149 EOF |
150 EOF |
150 print "<!-- This file was generated from ${sessions} -->\n"; |
151 print "<!-- Generated from ${sessions} -->\n"; |
|
152 print "<!-- *** DO NOT EDIT *** DO NOT EDIT *** DO NOT EDIT *** -->\n"; |
151 print <<'EOF'; |
153 print <<'EOF'; |
152 <MODE> |
154 <MODE> |
153 <PROPS> |
155 <PROPS> |
154 <PROPERTY NAME="commentStart" VALUE="(*"/> |
156 <PROPERTY NAME="commentStart" VALUE="(*"/> |
155 <PROPERTY NAME="commentEnd" VALUE="*)"/> |
157 <PROPERTY NAME="commentEnd" VALUE="*)"/> |