--- a/lib/scripts/keywords Fri Mar 16 18:21:22 2012 +0100
+++ b/lib/scripts/keywords Fri Mar 16 20:33:33 2012 +0100
@@ -30,18 +30,67 @@
}
}
+my %convert_kinds = (
+ "thy_begin" => "theory-begin",
+ "thy_end" => "theory-end",
+ "thy_heading" => "theory-heading",
+ "thy_decl" => "theory-decl",
+ "thy_script" => "theory-script",
+ "thy_goal" => "theory-goal",
+ "thy_schematic_goal" => "theory-goal",
+ "qed_block" => "qed-block",
+ "qed_global" => "qed-global",
+ "prf_heading" => "proof-heading",
+ "prf_goal" => "proof-goal",
+ "prf_block" => "proof-block",
+ "prf_open" => "proof-open",
+ "prf_close" => "proof-close",
+ "prf_chain" => "proof-chain",
+ "prf_decl" => "proof-decl",
+ "prf_asm" => "proof-asm",
+ "prf_asm_goal" => "proof-asm-goal",
+ "prf_script" => "proof-script"
+);
+
+my @emacs_kinds = (
+ "major",
+ "minor",
+ "control",
+ "diag",
+ "theory-begin",
+ "theory-switch",
+ "theory-end",
+ "theory-heading",
+ "theory-decl",
+ "theory-script",
+ "theory-goal",
+ "qed",
+ "qed-block",
+ "qed-global",
+ "proof-heading",
+ "proof-goal",
+ "proof-block",
+ "proof-open",
+ "proof-close",
+ "proof-chain",
+ "proof-decl",
+ "proof-asm",
+ "proof-asm-goal",
+ "proof-script"
+);
+
sub collect_keywords {
while(<STDIN>) {
- if (m/^Outer syntax keyword:\s*"(.*)"/) {
+ if (m/^Outer syntax keyword "([^"]*)" :: (\S*)/) {
+ my $name = $1;
+ my $kind = $2;
+ if (defined $convert_kinds{$kind}) { $kind = $convert_kinds{$kind} }
+ &set_keyword($name, $kind);
+ }
+ elsif (m/^Outer syntax keyword "([^"]*)"/) {
my $name = $1;
&set_keyword($name, "minor");
}
- elsif (m/^Outer syntax command:\s*"(.*)"\s*\((.*)\)/) {
- my $name = $1;
- my $kind = $2;
- if ($kind eq "theory-schematic-goal") { $kind = "theory-goal"; }
- &set_keyword($name, $kind);
- }
}
}
@@ -49,32 +98,6 @@
## Emacs output
sub emacs_output {
- my @kinds = (
- "major",
- "minor",
- "control",
- "diag",
- "theory-begin",
- "theory-switch",
- "theory-end",
- "theory-heading",
- "theory-decl",
- "theory-script",
- "theory-goal",
- "qed",
- "qed-block",
- "qed-global",
- "proof-heading",
- "proof-goal",
- "proof-block",
- "proof-open",
- "proof-close",
- "proof-chain",
- "proof-decl",
- "proof-asm",
- "proof-asm-goal",
- "proof-script"
- );
my $file = $keywords_name eq "" ? "isar-keywords.el" : "isar-keywords-${keywords_name}.el";
open (OUTPUT, "> ${file}") || die "$!";
select OUTPUT;
@@ -85,7 +108,7 @@
print ";; *** DO NOT EDIT *** DO NOT EDIT *** DO NOT EDIT ***\n";
print ";;\n";
- for my $kind (@kinds) {
+ for my $kind (@emacs_kinds) {
my @names;
for my $name (keys(%keywords)) {
if ($kind eq "major" ? $keywords{$name} ne "minor" : $keywords{$name} eq $kind) {