wenzelm@36949
|
1 |
(* Title: Pure/Isar/keyword.ML
|
wenzelm@17059
|
2 |
Author: Makarius
|
wenzelm@17059
|
3 |
|
wenzelm@27357
|
4 |
Isar command keyword classification and global keyword tables.
|
wenzelm@17059
|
5 |
*)
|
wenzelm@17059
|
6 |
|
wenzelm@36949
|
7 |
signature KEYWORD =
|
wenzelm@17059
|
8 |
sig
|
wenzelm@17059
|
9 |
type T
|
wenzelm@17059
|
10 |
val kind_of: T -> string
|
wenzelm@17059
|
11 |
val control: T
|
wenzelm@17059
|
12 |
val diag: T
|
wenzelm@17059
|
13 |
val thy_begin: T
|
wenzelm@17059
|
14 |
val thy_switch: T
|
wenzelm@17059
|
15 |
val thy_end: T
|
wenzelm@17059
|
16 |
val thy_heading: T
|
wenzelm@17059
|
17 |
val thy_decl: T
|
wenzelm@17059
|
18 |
val thy_script: T
|
wenzelm@17059
|
19 |
val thy_goal: T
|
wenzelm@36315
|
20 |
val thy_schematic_goal: T
|
wenzelm@17059
|
21 |
val qed: T
|
wenzelm@17059
|
22 |
val qed_block: T
|
wenzelm@17059
|
23 |
val qed_global: T
|
wenzelm@17059
|
24 |
val prf_heading: T
|
wenzelm@17059
|
25 |
val prf_goal: T
|
wenzelm@17059
|
26 |
val prf_block: T
|
wenzelm@17059
|
27 |
val prf_open: T
|
wenzelm@17059
|
28 |
val prf_close: T
|
wenzelm@17059
|
29 |
val prf_chain: T
|
wenzelm@17059
|
30 |
val prf_decl: T
|
wenzelm@17059
|
31 |
val prf_asm: T
|
wenzelm@17059
|
32 |
val prf_asm_goal: T
|
wenzelm@17059
|
33 |
val prf_script: T
|
wenzelm@17059
|
34 |
val kinds: string list
|
wenzelm@17059
|
35 |
val update_tags: string -> string list -> string list
|
wenzelm@17059
|
36 |
val tag: string -> T -> T
|
wenzelm@17059
|
37 |
val tags_of: T -> string list
|
wenzelm@17059
|
38 |
val tag_theory: T -> T
|
wenzelm@17059
|
39 |
val tag_proof: T -> T
|
wenzelm@17059
|
40 |
val tag_ml: T -> T
|
wenzelm@27357
|
41 |
val get_lexicons: unit -> Scan.lexicon * Scan.lexicon
|
wenzelm@27357
|
42 |
val is_keyword: string -> bool
|
wenzelm@27357
|
43 |
val dest_keywords: unit -> string list
|
wenzelm@27357
|
44 |
val dest_commands: unit -> string list
|
wenzelm@27357
|
45 |
val command_keyword: string -> T option
|
wenzelm@27357
|
46 |
val command_tags: string -> string list
|
wenzelm@34251
|
47 |
val keyword_status_reportN: string
|
wenzelm@27357
|
48 |
val report: unit -> unit
|
wenzelm@27357
|
49 |
val keyword: string -> unit
|
wenzelm@27357
|
50 |
val command: string -> T -> unit
|
wenzelm@29347
|
51 |
val is_diag: string -> bool
|
wenzelm@29347
|
52 |
val is_control: string -> bool
|
wenzelm@29347
|
53 |
val is_regular: string -> bool
|
wenzelm@29347
|
54 |
val is_theory_begin: string -> bool
|
wenzelm@27440
|
55 |
val is_theory: string -> bool
|
wenzelm@27440
|
56 |
val is_proof: string -> bool
|
wenzelm@28431
|
57 |
val is_theory_goal: string -> bool
|
wenzelm@28431
|
58 |
val is_proof_goal: string -> bool
|
wenzelm@36315
|
59 |
val is_schematic_goal: string -> bool
|
wenzelm@28431
|
60 |
val is_qed: string -> bool
|
wenzelm@28431
|
61 |
val is_qed_global: string -> bool
|
wenzelm@17059
|
62 |
end;
|
wenzelm@17059
|
63 |
|
wenzelm@36949
|
64 |
structure Keyword: KEYWORD =
|
wenzelm@17059
|
65 |
struct
|
wenzelm@17059
|
66 |
|
wenzelm@27357
|
67 |
(** keyword classification **)
|
wenzelm@17059
|
68 |
|
wenzelm@17059
|
69 |
datatype T = Keyword of string * string list;
|
wenzelm@17059
|
70 |
|
wenzelm@17059
|
71 |
fun kind s = Keyword (s, []);
|
wenzelm@17059
|
72 |
fun kind_of (Keyword (s, _)) = s;
|
wenzelm@17059
|
73 |
|
wenzelm@17059
|
74 |
|
wenzelm@17059
|
75 |
(* kinds *)
|
wenzelm@17059
|
76 |
|
wenzelm@17059
|
77 |
val control = kind "control";
|
wenzelm@17059
|
78 |
val diag = kind "diag";
|
wenzelm@17059
|
79 |
val thy_begin = kind "theory-begin";
|
wenzelm@17059
|
80 |
val thy_switch = kind "theory-switch";
|
wenzelm@17059
|
81 |
val thy_end = kind "theory-end";
|
wenzelm@17059
|
82 |
val thy_heading = kind "theory-heading";
|
wenzelm@17059
|
83 |
val thy_decl = kind "theory-decl";
|
wenzelm@17059
|
84 |
val thy_script = kind "theory-script";
|
wenzelm@17059
|
85 |
val thy_goal = kind "theory-goal";
|
wenzelm@36315
|
86 |
val thy_schematic_goal = kind "theory-schematic-goal";
|
wenzelm@17059
|
87 |
val qed = kind "qed";
|
wenzelm@17059
|
88 |
val qed_block = kind "qed-block";
|
wenzelm@17059
|
89 |
val qed_global = kind "qed-global";
|
wenzelm@17059
|
90 |
val prf_heading = kind "proof-heading";
|
wenzelm@17059
|
91 |
val prf_goal = kind "proof-goal";
|
wenzelm@17059
|
92 |
val prf_block = kind "proof-block";
|
wenzelm@17059
|
93 |
val prf_open = kind "proof-open";
|
wenzelm@17059
|
94 |
val prf_close = kind "proof-close";
|
wenzelm@17059
|
95 |
val prf_chain = kind "proof-chain";
|
wenzelm@17059
|
96 |
val prf_decl = kind "proof-decl";
|
wenzelm@17059
|
97 |
val prf_asm = kind "proof-asm";
|
wenzelm@17059
|
98 |
val prf_asm_goal = kind "proof-asm-goal";
|
wenzelm@17059
|
99 |
val prf_script = kind "proof-script";
|
wenzelm@17059
|
100 |
|
wenzelm@36315
|
101 |
val kinds =
|
wenzelm@36315
|
102 |
[control, diag, thy_begin, thy_switch, thy_end, thy_heading, thy_decl, thy_script, thy_goal,
|
wenzelm@36315
|
103 |
thy_schematic_goal, qed, qed_block, qed_global, prf_heading, prf_goal, prf_block, prf_open,
|
wenzelm@36315
|
104 |
prf_close, prf_chain, prf_decl, prf_asm, prf_asm_goal, prf_script]
|
wenzelm@36315
|
105 |
|> map kind_of;
|
wenzelm@17059
|
106 |
|
wenzelm@17059
|
107 |
|
wenzelm@17059
|
108 |
(* tags *)
|
wenzelm@17059
|
109 |
|
haftmann@17270
|
110 |
fun update_tags t ts = t :: remove (op = : string * string -> bool) t ts;
|
wenzelm@17059
|
111 |
|
wenzelm@17059
|
112 |
fun tag t (Keyword (s, ts)) = Keyword (s, update_tags t ts);
|
wenzelm@17059
|
113 |
fun tags_of (Keyword (_, ts)) = ts;
|
wenzelm@17059
|
114 |
|
wenzelm@17059
|
115 |
val tag_theory = tag "theory";
|
wenzelm@17059
|
116 |
val tag_proof = tag "proof";
|
wenzelm@17059
|
117 |
val tag_ml = tag "ML";
|
wenzelm@17059
|
118 |
|
wenzelm@27357
|
119 |
|
wenzelm@27357
|
120 |
|
wenzelm@27357
|
121 |
(** global keyword tables **)
|
wenzelm@27357
|
122 |
|
wenzelm@27357
|
123 |
local
|
wenzelm@27357
|
124 |
|
wenzelm@32738
|
125 |
val global_commands = Unsynchronized.ref (Symtab.empty: T Symtab.table);
|
wenzelm@32738
|
126 |
val global_lexicons = Unsynchronized.ref (Scan.empty_lexicon, Scan.empty_lexicon);
|
wenzelm@27357
|
127 |
|
wenzelm@27357
|
128 |
in
|
wenzelm@27357
|
129 |
|
wenzelm@33234
|
130 |
fun get_commands () = ! global_commands;
|
wenzelm@33234
|
131 |
fun get_lexicons () = ! global_lexicons;
|
wenzelm@27357
|
132 |
|
wenzelm@32738
|
133 |
fun change_commands f = CRITICAL (fn () => Unsynchronized.change global_commands f);
|
wenzelm@32738
|
134 |
fun change_lexicons f = CRITICAL (fn () => Unsynchronized.change global_lexicons f);
|
wenzelm@27357
|
135 |
|
wenzelm@17059
|
136 |
end;
|
wenzelm@27357
|
137 |
|
wenzelm@27357
|
138 |
|
wenzelm@27357
|
139 |
(* lookup *)
|
wenzelm@27357
|
140 |
|
wenzelm@27357
|
141 |
fun is_keyword s = Scan.is_literal (#1 (get_lexicons ())) (Symbol.explode s);
|
wenzelm@27805
|
142 |
fun dest_keywords () = sort_strings (Scan.dest_lexicon (#1 (get_lexicons ())));
|
wenzelm@27357
|
143 |
|
wenzelm@27805
|
144 |
fun dest_commands () = sort_strings (Symtab.keys (get_commands ()));
|
wenzelm@27357
|
145 |
fun command_keyword name = Symtab.lookup (get_commands ()) name;
|
wenzelm@27357
|
146 |
fun command_tags name = these (Option.map tags_of (command_keyword name));
|
wenzelm@27357
|
147 |
|
wenzelm@27357
|
148 |
|
wenzelm@36719
|
149 |
(* reports *)
|
wenzelm@27357
|
150 |
|
wenzelm@34251
|
151 |
val keyword_status_reportN = "keyword_status_report";
|
wenzelm@34251
|
152 |
|
wenzelm@34251
|
153 |
fun report_message s =
|
wenzelm@34251
|
154 |
(if print_mode_active keyword_status_reportN then Output.status else writeln) s;
|
wenzelm@34251
|
155 |
|
wenzelm@27357
|
156 |
fun report_keyword name =
|
wenzelm@34251
|
157 |
report_message (Markup.markup (Markup.keyword_decl name)
|
wenzelm@34251
|
158 |
("Outer syntax keyword: " ^ quote name));
|
wenzelm@27357
|
159 |
|
wenzelm@27357
|
160 |
fun report_command (name, kind) =
|
wenzelm@34251
|
161 |
report_message (Markup.markup (Markup.command_decl name (kind_of kind))
|
wenzelm@34251
|
162 |
("Outer syntax command: " ^ quote name ^ " (" ^ kind_of kind ^ ")"));
|
wenzelm@30685
|
163 |
|
wenzelm@27357
|
164 |
fun report () =
|
wenzelm@27357
|
165 |
let val (keywords, commands) = CRITICAL (fn () =>
|
wenzelm@27805
|
166 |
(dest_keywords (), sort_wrt #1 (Symtab.dest (get_commands ()))))
|
wenzelm@34251
|
167 |
in
|
wenzelm@34251
|
168 |
List.app report_keyword keywords;
|
wenzelm@34251
|
169 |
List.app report_command commands
|
wenzelm@34251
|
170 |
end;
|
wenzelm@27357
|
171 |
|
wenzelm@27357
|
172 |
|
wenzelm@27357
|
173 |
(* augment tables *)
|
wenzelm@27357
|
174 |
|
wenzelm@27357
|
175 |
fun keyword name =
|
wenzelm@27768
|
176 |
(change_lexicons (apfst (Scan.extend_lexicon (Symbol.explode name)));
|
wenzelm@34251
|
177 |
report_keyword name);
|
wenzelm@27357
|
178 |
|
wenzelm@27357
|
179 |
fun command name kind =
|
wenzelm@27768
|
180 |
(change_lexicons (apsnd (Scan.extend_lexicon (Symbol.explode name)));
|
wenzelm@27357
|
181 |
change_commands (Symtab.update (name, kind));
|
wenzelm@34251
|
182 |
report_command (name, kind));
|
wenzelm@27357
|
183 |
|
wenzelm@27433
|
184 |
|
wenzelm@28431
|
185 |
(* command categories *)
|
wenzelm@27433
|
186 |
|
wenzelm@27440
|
187 |
fun command_category ks name =
|
wenzelm@27440
|
188 |
(case command_keyword name of
|
wenzelm@27440
|
189 |
NONE => false
|
wenzelm@28431
|
190 |
| SOME k => member (op = o pairself kind_of) ks k);
|
wenzelm@27433
|
191 |
|
wenzelm@29347
|
192 |
val is_diag = command_category [diag];
|
wenzelm@29347
|
193 |
val is_control = command_category [control];
|
wenzelm@29347
|
194 |
fun is_regular name = not (is_diag name orelse is_control name);
|
wenzelm@29347
|
195 |
|
wenzelm@29347
|
196 |
val is_theory_begin = command_category [thy_begin];
|
wenzelm@29347
|
197 |
|
wenzelm@27440
|
198 |
val is_theory = command_category
|
wenzelm@36315
|
199 |
[thy_begin, thy_switch, thy_end, thy_heading, thy_decl, thy_script, thy_goal, thy_schematic_goal];
|
wenzelm@27440
|
200 |
|
wenzelm@27440
|
201 |
val is_proof = command_category
|
wenzelm@28431
|
202 |
[qed, qed_block, qed_global, prf_heading, prf_goal, prf_block, prf_open, prf_close,
|
wenzelm@28431
|
203 |
prf_chain, prf_decl, prf_asm, prf_asm_goal, prf_script];
|
wenzelm@27433
|
204 |
|
wenzelm@36315
|
205 |
val is_theory_goal = command_category [thy_goal, thy_schematic_goal];
|
wenzelm@28431
|
206 |
val is_proof_goal = command_category [prf_goal, prf_asm_goal];
|
wenzelm@36315
|
207 |
val is_schematic_goal = command_category [thy_schematic_goal];
|
wenzelm@28431
|
208 |
val is_qed = command_category [qed, qed_block];
|
wenzelm@28431
|
209 |
val is_qed_global = command_category [qed_global];
|
wenzelm@27520
|
210 |
|
wenzelm@27357
|
211 |
end;
|
wenzelm@36949
|
212 |
|
wenzelm@36949
|
213 |
(*legacy alias*)
|
wenzelm@36949
|
214 |
structure OuterKeyword = Keyword;
|
wenzelm@36949
|
215 |
|
wenzelm@36949
|
216 |
|