author | wenzelm |
Fri, 16 Mar 2012 20:33:33 +0100 | |
changeset 46967 | 499d9bbd8de9 |
parent 36316 | f9b45eac4c60 |
child 46969 | 481b7d9ad6fe |
permissions | -rwxr-xr-x |
35022
c844b93dd147
modernized perl scripts: prefer standalone executables;
wenzelm
parents:
33684
diff
changeset
|
1 |
#!/usr/bin/env perl |
24875 | 2 |
# |
3 |
# Author: Makarius |
|
4 |
# |
|
5 |
# keywords.pl - generate outer syntax keyword files from session logs |
|
6 |
# |
|
7 |
||
35022
c844b93dd147
modernized perl scripts: prefer standalone executables;
wenzelm
parents:
33684
diff
changeset
|
8 |
use warnings; |
c844b93dd147
modernized perl scripts: prefer standalone executables;
wenzelm
parents:
33684
diff
changeset
|
9 |
use strict; |
c844b93dd147
modernized perl scripts: prefer standalone executables;
wenzelm
parents:
33684
diff
changeset
|
10 |
|
c844b93dd147
modernized perl scripts: prefer standalone executables;
wenzelm
parents:
33684
diff
changeset
|
11 |
|
24886 | 12 |
## arguments |
24875 | 13 |
|
33684 | 14 |
my ($keywords_name, $sessions) = @ARGV; |
24875 | 15 |
|
16 |
||
17 |
## keywords |
|
18 |
||
19 |
my %keywords; |
|
20 |
||
21 |
sub set_keyword { |
|
22 |
my ($name, $kind) = @_; |
|
27386 | 23 |
if (defined $keywords{$name} and $keywords{$name} ne $kind and $keywords{$name} ne "minor") { |
24 |
if ($kind ne "minor") { |
|
25 |
print STDERR "### Inconsistent declaration of keyword \"${name}\": $keywords{$name} vs ${kind}\n"; |
|
26 |
$keywords{$name} = $kind; |
|
27 |
} |
|
28 |
} else { |
|
29 |
$keywords{$name} = $kind; |
|
24875 | 30 |
} |
31 |
} |
|
32 |
||
46967
499d9bbd8de9
uniform keyword names within ML/Scala -- produce elisp names via external conversion;
wenzelm
parents:
36316
diff
changeset
|
33 |
my %convert_kinds = ( |
499d9bbd8de9
uniform keyword names within ML/Scala -- produce elisp names via external conversion;
wenzelm
parents:
36316
diff
changeset
|
34 |
"thy_begin" => "theory-begin", |
499d9bbd8de9
uniform keyword names within ML/Scala -- produce elisp names via external conversion;
wenzelm
parents:
36316
diff
changeset
|
35 |
"thy_end" => "theory-end", |
499d9bbd8de9
uniform keyword names within ML/Scala -- produce elisp names via external conversion;
wenzelm
parents:
36316
diff
changeset
|
36 |
"thy_heading" => "theory-heading", |
499d9bbd8de9
uniform keyword names within ML/Scala -- produce elisp names via external conversion;
wenzelm
parents:
36316
diff
changeset
|
37 |
"thy_decl" => "theory-decl", |
499d9bbd8de9
uniform keyword names within ML/Scala -- produce elisp names via external conversion;
wenzelm
parents:
36316
diff
changeset
|
38 |
"thy_script" => "theory-script", |
499d9bbd8de9
uniform keyword names within ML/Scala -- produce elisp names via external conversion;
wenzelm
parents:
36316
diff
changeset
|
39 |
"thy_goal" => "theory-goal", |
499d9bbd8de9
uniform keyword names within ML/Scala -- produce elisp names via external conversion;
wenzelm
parents:
36316
diff
changeset
|
40 |
"thy_schematic_goal" => "theory-goal", |
499d9bbd8de9
uniform keyword names within ML/Scala -- produce elisp names via external conversion;
wenzelm
parents:
36316
diff
changeset
|
41 |
"qed_block" => "qed-block", |
499d9bbd8de9
uniform keyword names within ML/Scala -- produce elisp names via external conversion;
wenzelm
parents:
36316
diff
changeset
|
42 |
"qed_global" => "qed-global", |
499d9bbd8de9
uniform keyword names within ML/Scala -- produce elisp names via external conversion;
wenzelm
parents:
36316
diff
changeset
|
43 |
"prf_heading" => "proof-heading", |
499d9bbd8de9
uniform keyword names within ML/Scala -- produce elisp names via external conversion;
wenzelm
parents:
36316
diff
changeset
|
44 |
"prf_goal" => "proof-goal", |
499d9bbd8de9
uniform keyword names within ML/Scala -- produce elisp names via external conversion;
wenzelm
parents:
36316
diff
changeset
|
45 |
"prf_block" => "proof-block", |
499d9bbd8de9
uniform keyword names within ML/Scala -- produce elisp names via external conversion;
wenzelm
parents:
36316
diff
changeset
|
46 |
"prf_open" => "proof-open", |
499d9bbd8de9
uniform keyword names within ML/Scala -- produce elisp names via external conversion;
wenzelm
parents:
36316
diff
changeset
|
47 |
"prf_close" => "proof-close", |
499d9bbd8de9
uniform keyword names within ML/Scala -- produce elisp names via external conversion;
wenzelm
parents:
36316
diff
changeset
|
48 |
"prf_chain" => "proof-chain", |
499d9bbd8de9
uniform keyword names within ML/Scala -- produce elisp names via external conversion;
wenzelm
parents:
36316
diff
changeset
|
49 |
"prf_decl" => "proof-decl", |
499d9bbd8de9
uniform keyword names within ML/Scala -- produce elisp names via external conversion;
wenzelm
parents:
36316
diff
changeset
|
50 |
"prf_asm" => "proof-asm", |
499d9bbd8de9
uniform keyword names within ML/Scala -- produce elisp names via external conversion;
wenzelm
parents:
36316
diff
changeset
|
51 |
"prf_asm_goal" => "proof-asm-goal", |
499d9bbd8de9
uniform keyword names within ML/Scala -- produce elisp names via external conversion;
wenzelm
parents:
36316
diff
changeset
|
52 |
"prf_script" => "proof-script" |
499d9bbd8de9
uniform keyword names within ML/Scala -- produce elisp names via external conversion;
wenzelm
parents:
36316
diff
changeset
|
53 |
); |
499d9bbd8de9
uniform keyword names within ML/Scala -- produce elisp names via external conversion;
wenzelm
parents:
36316
diff
changeset
|
54 |
|
499d9bbd8de9
uniform keyword names within ML/Scala -- produce elisp names via external conversion;
wenzelm
parents:
36316
diff
changeset
|
55 |
my @emacs_kinds = ( |
499d9bbd8de9
uniform keyword names within ML/Scala -- produce elisp names via external conversion;
wenzelm
parents:
36316
diff
changeset
|
56 |
"major", |
499d9bbd8de9
uniform keyword names within ML/Scala -- produce elisp names via external conversion;
wenzelm
parents:
36316
diff
changeset
|
57 |
"minor", |
499d9bbd8de9
uniform keyword names within ML/Scala -- produce elisp names via external conversion;
wenzelm
parents:
36316
diff
changeset
|
58 |
"control", |
499d9bbd8de9
uniform keyword names within ML/Scala -- produce elisp names via external conversion;
wenzelm
parents:
36316
diff
changeset
|
59 |
"diag", |
499d9bbd8de9
uniform keyword names within ML/Scala -- produce elisp names via external conversion;
wenzelm
parents:
36316
diff
changeset
|
60 |
"theory-begin", |
499d9bbd8de9
uniform keyword names within ML/Scala -- produce elisp names via external conversion;
wenzelm
parents:
36316
diff
changeset
|
61 |
"theory-switch", |
499d9bbd8de9
uniform keyword names within ML/Scala -- produce elisp names via external conversion;
wenzelm
parents:
36316
diff
changeset
|
62 |
"theory-end", |
499d9bbd8de9
uniform keyword names within ML/Scala -- produce elisp names via external conversion;
wenzelm
parents:
36316
diff
changeset
|
63 |
"theory-heading", |
499d9bbd8de9
uniform keyword names within ML/Scala -- produce elisp names via external conversion;
wenzelm
parents:
36316
diff
changeset
|
64 |
"theory-decl", |
499d9bbd8de9
uniform keyword names within ML/Scala -- produce elisp names via external conversion;
wenzelm
parents:
36316
diff
changeset
|
65 |
"theory-script", |
499d9bbd8de9
uniform keyword names within ML/Scala -- produce elisp names via external conversion;
wenzelm
parents:
36316
diff
changeset
|
66 |
"theory-goal", |
499d9bbd8de9
uniform keyword names within ML/Scala -- produce elisp names via external conversion;
wenzelm
parents:
36316
diff
changeset
|
67 |
"qed", |
499d9bbd8de9
uniform keyword names within ML/Scala -- produce elisp names via external conversion;
wenzelm
parents:
36316
diff
changeset
|
68 |
"qed-block", |
499d9bbd8de9
uniform keyword names within ML/Scala -- produce elisp names via external conversion;
wenzelm
parents:
36316
diff
changeset
|
69 |
"qed-global", |
499d9bbd8de9
uniform keyword names within ML/Scala -- produce elisp names via external conversion;
wenzelm
parents:
36316
diff
changeset
|
70 |
"proof-heading", |
499d9bbd8de9
uniform keyword names within ML/Scala -- produce elisp names via external conversion;
wenzelm
parents:
36316
diff
changeset
|
71 |
"proof-goal", |
499d9bbd8de9
uniform keyword names within ML/Scala -- produce elisp names via external conversion;
wenzelm
parents:
36316
diff
changeset
|
72 |
"proof-block", |
499d9bbd8de9
uniform keyword names within ML/Scala -- produce elisp names via external conversion;
wenzelm
parents:
36316
diff
changeset
|
73 |
"proof-open", |
499d9bbd8de9
uniform keyword names within ML/Scala -- produce elisp names via external conversion;
wenzelm
parents:
36316
diff
changeset
|
74 |
"proof-close", |
499d9bbd8de9
uniform keyword names within ML/Scala -- produce elisp names via external conversion;
wenzelm
parents:
36316
diff
changeset
|
75 |
"proof-chain", |
499d9bbd8de9
uniform keyword names within ML/Scala -- produce elisp names via external conversion;
wenzelm
parents:
36316
diff
changeset
|
76 |
"proof-decl", |
499d9bbd8de9
uniform keyword names within ML/Scala -- produce elisp names via external conversion;
wenzelm
parents:
36316
diff
changeset
|
77 |
"proof-asm", |
499d9bbd8de9
uniform keyword names within ML/Scala -- produce elisp names via external conversion;
wenzelm
parents:
36316
diff
changeset
|
78 |
"proof-asm-goal", |
499d9bbd8de9
uniform keyword names within ML/Scala -- produce elisp names via external conversion;
wenzelm
parents:
36316
diff
changeset
|
79 |
"proof-script" |
499d9bbd8de9
uniform keyword names within ML/Scala -- produce elisp names via external conversion;
wenzelm
parents:
36316
diff
changeset
|
80 |
); |
499d9bbd8de9
uniform keyword names within ML/Scala -- produce elisp names via external conversion;
wenzelm
parents:
36316
diff
changeset
|
81 |
|
24875 | 82 |
sub collect_keywords { |
83 |
while(<STDIN>) { |
|
46967
499d9bbd8de9
uniform keyword names within ML/Scala -- produce elisp names via external conversion;
wenzelm
parents:
36316
diff
changeset
|
84 |
if (m/^Outer syntax keyword "([^"]*)" :: (\S*)/) { |
499d9bbd8de9
uniform keyword names within ML/Scala -- produce elisp names via external conversion;
wenzelm
parents:
36316
diff
changeset
|
85 |
my $name = $1; |
499d9bbd8de9
uniform keyword names within ML/Scala -- produce elisp names via external conversion;
wenzelm
parents:
36316
diff
changeset
|
86 |
my $kind = $2; |
499d9bbd8de9
uniform keyword names within ML/Scala -- produce elisp names via external conversion;
wenzelm
parents:
36316
diff
changeset
|
87 |
if (defined $convert_kinds{$kind}) { $kind = $convert_kinds{$kind} } |
499d9bbd8de9
uniform keyword names within ML/Scala -- produce elisp names via external conversion;
wenzelm
parents:
36316
diff
changeset
|
88 |
&set_keyword($name, $kind); |
499d9bbd8de9
uniform keyword names within ML/Scala -- produce elisp names via external conversion;
wenzelm
parents:
36316
diff
changeset
|
89 |
} |
499d9bbd8de9
uniform keyword names within ML/Scala -- produce elisp names via external conversion;
wenzelm
parents:
36316
diff
changeset
|
90 |
elsif (m/^Outer syntax keyword "([^"]*)"/) { |
24875 | 91 |
my $name = $1; |
92 |
&set_keyword($name, "minor"); |
|
93 |
} |
|
94 |
} |
|
95 |
} |
|
96 |
||
97 |
||
98 |
## Emacs output |
|
99 |
||
100 |
sub emacs_output { |
|
101 |
my $file = $keywords_name eq "" ? "isar-keywords.el" : "isar-keywords-${keywords_name}.el"; |
|
102 |
open (OUTPUT, "> ${file}") || die "$!"; |
|
103 |
select OUTPUT; |
|
104 |
||
105 |
print ";;\n"; |
|
106 |
print ";; Keyword classification tables for Isabelle/Isar.\n"; |
|
24912 | 107 |
print ";; Generated from ${sessions}.\n"; |
24905 | 108 |
print ";; *** DO NOT EDIT *** DO NOT EDIT *** DO NOT EDIT ***\n"; |
24875 | 109 |
print ";;\n"; |
110 |
||
46967
499d9bbd8de9
uniform keyword names within ML/Scala -- produce elisp names via external conversion;
wenzelm
parents:
36316
diff
changeset
|
111 |
for my $kind (@emacs_kinds) { |
24875 | 112 |
my @names; |
113 |
for my $name (keys(%keywords)) { |
|
114 |
if ($kind eq "major" ? $keywords{$name} ne "minor" : $keywords{$name} eq $kind) { |
|
115 |
if ($kind ne "minor" or $name =~ m/^[A-Za-z0-9_]+$/) { |
|
116 |
push @names, $name; |
|
117 |
} |
|
118 |
} |
|
119 |
} |
|
120 |
@names = sort(@names); |
|
121 |
||
122 |
print "\n(defconst isar-keywords-${kind}"; |
|
123 |
print "\n '("; |
|
124 |
my $first = 1; |
|
125 |
for my $name (@names) { |
|
126 |
$name =~ s/([\.\*\+\?\[\]\^\$])/\\\\$1/g; |
|
127 |
if ($first) { |
|
128 |
print "\"${name}\""; |
|
129 |
$first = 0; |
|
130 |
} |
|
131 |
else { |
|
132 |
print "\n \"${name}\""; |
|
133 |
} |
|
134 |
} |
|
135 |
print "))\n"; |
|
136 |
} |
|
137 |
print "\n(provide 'isar-keywords)\n"; |
|
138 |
||
139 |
close OUTPUT; |
|
140 |
select; |
|
33684 | 141 |
print STDERR "${file}\n"; |
24875 | 142 |
} |
143 |
||
144 |
||
145 |
## main |
|
146 |
||
147 |
&collect_keywords(); |
|
33684 | 148 |
&emacs_output(); |