1 #!/usr/bin/env perl |
|
2 # |
|
3 # Author: Makarius |
|
4 # |
|
5 # keywords.pl - generate outer syntax keyword files from session logs |
|
6 # |
|
7 |
|
8 use warnings; |
|
9 use strict; |
|
10 |
|
11 |
|
12 ## arguments |
|
13 |
|
14 my ($keywords_name, $sessions) = @ARGV; |
|
15 |
|
16 |
|
17 ## keywords |
|
18 |
|
19 my %keywords; |
|
20 |
|
21 sub set_keyword { |
|
22 my ($name, $kind) = @_; |
|
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; |
|
30 } |
|
31 } |
|
32 |
|
33 my %convert_kinds = ( |
|
34 "thy_begin" => "theory-begin", |
|
35 "thy_end" => "theory-end", |
|
36 "thy_heading1" => "theory-heading", |
|
37 "thy_heading2" => "theory-heading", |
|
38 "thy_heading3" => "theory-heading", |
|
39 "thy_heading4" => "theory-heading", |
|
40 "thy_load" => "theory-decl", |
|
41 "thy_decl" => "theory-decl", |
|
42 "thy_script" => "theory-script", |
|
43 "thy_goal" => "theory-goal", |
|
44 "qed_block" => "qed-block", |
|
45 "qed_global" => "qed-global", |
|
46 "prf_heading2" => "proof-heading", |
|
47 "prf_heading3" => "proof-heading", |
|
48 "prf_heading4" => "proof-heading", |
|
49 "prf_goal" => "proof-goal", |
|
50 "prf_block" => "proof-block", |
|
51 "prf_open" => "proof-open", |
|
52 "prf_close" => "proof-close", |
|
53 "prf_chain" => "proof-chain", |
|
54 "prf_decl" => "proof-decl", |
|
55 "prf_asm" => "proof-asm", |
|
56 "prf_asm_goal" => "proof-asm-goal", |
|
57 "prf_script" => "proof-script" |
|
58 ); |
|
59 |
|
60 my @emacs_kinds = ( |
|
61 "major", |
|
62 "minor", |
|
63 "control", |
|
64 "diag", |
|
65 "theory-begin", |
|
66 "theory-switch", |
|
67 "theory-end", |
|
68 "theory-heading", |
|
69 "theory-decl", |
|
70 "theory-script", |
|
71 "theory-goal", |
|
72 "qed", |
|
73 "qed-block", |
|
74 "qed-global", |
|
75 "proof-heading", |
|
76 "proof-goal", |
|
77 "proof-block", |
|
78 "proof-open", |
|
79 "proof-close", |
|
80 "proof-chain", |
|
81 "proof-decl", |
|
82 "proof-asm", |
|
83 "proof-asm-goal", |
|
84 "proof-script" |
|
85 ); |
|
86 |
|
87 sub collect_keywords { |
|
88 while(<STDIN>) { |
|
89 if (m/^\fOuter syntax keyword "([^"]*)" :: (\S*)/) { |
|
90 my $name = $1; |
|
91 my $kind = $2; |
|
92 if (defined $convert_kinds{$kind}) { $kind = $convert_kinds{$kind} } |
|
93 &set_keyword($name, $kind); |
|
94 } |
|
95 elsif (m/^\fOuter syntax keyword "([^"]*)"/) { |
|
96 my $name = $1; |
|
97 &set_keyword($name, "minor"); |
|
98 } |
|
99 } |
|
100 } |
|
101 |
|
102 |
|
103 ## Emacs output |
|
104 |
|
105 sub emacs_output { |
|
106 my $file = $keywords_name eq "" ? "isar-keywords.el" : "isar-keywords-${keywords_name}.el"; |
|
107 open (OUTPUT, "> ${file}") || die "$!"; |
|
108 select OUTPUT; |
|
109 |
|
110 print ";;\n"; |
|
111 print ";; Keyword classification tables for Isabelle/Isar.\n"; |
|
112 print ";; Generated from ${sessions}.\n"; |
|
113 print ";; *** DO NOT EDIT *** DO NOT EDIT *** DO NOT EDIT ***\n"; |
|
114 print ";;\n"; |
|
115 |
|
116 for my $kind (@emacs_kinds) { |
|
117 my @names; |
|
118 for my $name (keys(%keywords)) { |
|
119 if ($kind eq "major" ? $keywords{$name} ne "minor" : $keywords{$name} eq $kind) { |
|
120 if ($kind ne "minor" or $name =~ m/^[A-Za-z0-9_]+$/) { |
|
121 push @names, $name; |
|
122 } |
|
123 } |
|
124 } |
|
125 @names = sort(@names); |
|
126 |
|
127 print "\n(defconst isar-keywords-${kind}"; |
|
128 print "\n '("; |
|
129 my $first = 1; |
|
130 for my $name (@names) { |
|
131 $name =~ s/([\.\*\+\?\[\]\^\$])/\\\\$1/g; |
|
132 if ($first) { |
|
133 print "\"${name}\""; |
|
134 $first = 0; |
|
135 } |
|
136 else { |
|
137 print "\n \"${name}\""; |
|
138 } |
|
139 } |
|
140 print "))\n"; |
|
141 } |
|
142 print "\n(provide 'isar-keywords)\n"; |
|
143 |
|
144 close OUTPUT; |
|
145 select; |
|
146 print STDERR "${file}\n"; |
|
147 } |
|
148 |
|
149 |
|
150 ## main |
|
151 |
|
152 &collect_keywords(); |
|
153 &emacs_output(); |
|