1(*  Title:      Pure/Isar/keyword.ML
2    Author:     Makarius
3
4Isar keyword classification.
5*)
6
7signature KEYWORD =
8sig
9  val diag: string
10  val document_heading: string
11  val document_body: string
12  val document_raw: string
13  val thy_begin: string
14  val thy_end: string
15  val thy_decl: string
16  val thy_decl_block: string
17  val thy_load: string
18  val thy_goal: string
19  val qed: string
20  val qed_script: string
21  val qed_block: string
22  val qed_global: string
23  val prf_goal: string
24  val prf_block: string
25  val next_block: string
26  val prf_open: string
27  val prf_close: string
28  val prf_chain: string
29  val prf_decl: string
30  val prf_asm: string
31  val prf_asm_goal: string
32  val prf_script: string
33  val prf_script_goal: string
34  val prf_script_asm_goal: string
35  val before_command: string
36  val quasi_command: string
37  type spec = (string * string list) * string list
38  val no_spec: spec
39  val before_command_spec: spec
40  val quasi_command_spec: spec
41  val document_heading_spec: spec
42  val document_body_spec: spec
43  type keywords
44  val minor_keywords: keywords -> Scan.lexicon
45  val major_keywords: keywords -> Scan.lexicon
46  val no_command_keywords: keywords -> keywords
47  val empty_keywords: keywords
48  val merge_keywords: keywords * keywords -> keywords
49  val add_keywords: ((string * Position.T) * spec) list -> keywords -> keywords
50  val is_keyword: keywords -> string -> bool
51  val is_command: keywords -> string -> bool
52  val is_literal: keywords -> string -> bool
53  val dest_commands: keywords -> string list
54  val command_markup: keywords -> string -> Markup.T option
55  val command_kind: keywords -> string -> string option
56  val command_files: keywords -> string -> Path.T -> Path.T list
57  val command_tags: keywords -> string -> string list
58  val is_vacuous: keywords -> string -> bool
59  val is_diag: keywords -> string -> bool
60  val is_document_heading: keywords -> string -> bool
61  val is_document_body: keywords -> string -> bool
62  val is_document_raw: keywords -> string -> bool
63  val is_document: keywords -> string -> bool
64  val is_theory_end: keywords -> string -> bool
65  val is_theory_load: keywords -> string -> bool
66  val is_theory: keywords -> string -> bool
67  val is_theory_body: keywords -> string -> bool
68  val is_proof: keywords -> string -> bool
69  val is_proof_body: keywords -> string -> bool
70  val is_theory_goal: keywords -> string -> bool
71  val is_proof_goal: keywords -> string -> bool
72  val is_qed: keywords -> string -> bool
73  val is_qed_global: keywords -> string -> bool
74  val is_proof_open: keywords -> string -> bool
75  val is_proof_close: keywords -> string -> bool
76  val is_proof_asm: keywords -> string -> bool
77  val is_improper: keywords -> string -> bool
78  val is_printed: keywords -> string -> bool
79end;
80
81structure Keyword: KEYWORD =
82struct
83
84(** keyword classification **)
85
86(* kinds *)
87
88val diag = "diag";
89val document_heading = "document_heading";
90val document_body = "document_body";
91val document_raw = "document_raw";
92val thy_begin = "thy_begin";
93val thy_end = "thy_end";
94val thy_decl = "thy_decl";
95val thy_decl_block = "thy_decl_block";
96val thy_load = "thy_load";
97val thy_goal = "thy_goal";
98val qed = "qed";
99val qed_script = "qed_script";
100val qed_block = "qed_block";
101val qed_global = "qed_global";
102val prf_goal = "prf_goal";
103val prf_block = "prf_block";
104val next_block = "next_block";
105val prf_open = "prf_open";
106val prf_close = "prf_close";
107val prf_chain = "prf_chain";
108val prf_decl = "prf_decl";
109val prf_asm = "prf_asm";
110val prf_asm_goal = "prf_asm_goal";
111val prf_script = "prf_script";
112val prf_script_goal = "prf_script_goal";
113val prf_script_asm_goal = "prf_script_asm_goal";
114
115val before_command = "before_command";
116val quasi_command = "quasi_command";
117
118val command_kinds =
119  [diag, document_heading, document_body, document_raw, thy_begin, thy_end, thy_load, thy_decl,
120    thy_decl_block, thy_goal, qed, qed_script, qed_block, qed_global, prf_goal, prf_block,
121    next_block, prf_open, prf_close, prf_chain, prf_decl, prf_asm, prf_asm_goal, prf_script,
122    prf_script_goal, prf_script_asm_goal];
123
124
125(* specifications *)
126
127type spec = (string * string list) * string list;
128
129val no_spec: spec = (("", []), []);
130val before_command_spec: spec = ((before_command, []), []);
131val quasi_command_spec: spec = ((quasi_command, []), []);
132val document_heading_spec: spec = (("document_heading", []), ["document"]);
133val document_body_spec: spec = (("document_body", []), ["document"]);
134
135type entry =
136 {pos: Position.T,
137  id: serial,
138  kind: string,
139  files: string list,  (*extensions of embedded files*)
140  tags: string list};
141
142fun check_spec pos ((kind, files), tags) : entry =
143  if not (member (op =) command_kinds kind) then
144    error ("Unknown outer syntax keyword kind " ^ quote kind)
145  else if not (null files) andalso kind <> thy_load then
146    error ("Illegal specification of files for " ^ quote kind)
147  else {pos = pos, id = serial (), kind = kind, files = files, tags = tags};
148
149
150(** keyword tables **)
151
152(* type keywords *)
153
154datatype keywords = Keywords of
155 {minor: Scan.lexicon,
156  major: Scan.lexicon,
157  commands: entry Symtab.table};
158
159fun minor_keywords (Keywords {minor, ...}) = minor;
160fun major_keywords (Keywords {major, ...}) = major;
161
162fun make_keywords (minor, major, commands) =
163  Keywords {minor = minor, major = major, commands = commands};
164
165fun map_keywords f (Keywords {minor, major, commands}) =
166  make_keywords (f (minor, major, commands));
167
168val no_command_keywords =
169  map_keywords (fn (minor, _, _) => (minor, Scan.empty_lexicon, Symtab.empty));
170
171
172(* build keywords *)
173
174val empty_keywords =
175  make_keywords (Scan.empty_lexicon, Scan.empty_lexicon, Symtab.empty);
176
177fun merge_keywords
178  (Keywords {minor = minor1, major = major1, commands = commands1},
179    Keywords {minor = minor2, major = major2, commands = commands2}) =
180  make_keywords
181   (Scan.merge_lexicons (minor1, minor2),
182    Scan.merge_lexicons (major1, major2),
183    Symtab.merge (K true) (commands1, commands2));
184
185val add_keywords =
186  fold (fn ((name, pos), spec as ((kind, _), _)) => map_keywords (fn (minor, major, commands) =>
187    if kind = "" orelse kind = before_command orelse kind = quasi_command then
188      let
189        val minor' = Scan.extend_lexicon (Symbol.explode name) minor;
190      in (minor', major, commands) end
191    else
192      let
193        val entry = check_spec pos spec;
194        val major' = Scan.extend_lexicon (Symbol.explode name) major;
195        val commands' = Symtab.update (name, entry) commands;
196      in (minor, major', commands') end));
197
198
199(* keyword status *)
200
201fun is_keyword keywords s = Scan.is_literal (minor_keywords keywords) (Symbol.explode s);
202fun is_command (Keywords {commands, ...}) = Symtab.defined commands;
203fun is_literal keywords = is_keyword keywords orf is_command keywords;
204
205fun dest_commands (Keywords {commands, ...}) = Symtab.keys commands;
206
207
208(* command keywords *)
209
210fun lookup_command (Keywords {commands, ...}) = Symtab.lookup commands;
211
212fun command_markup keywords name =
213  lookup_command keywords name
214  |> Option.map (fn {pos, id, ...} =>
215      Markup.properties (Position.entity_properties_of false id pos)
216        (Markup.entity Markup.command_keywordN name));
217
218fun command_kind keywords = Option.map #kind o lookup_command keywords;
219
220fun command_files keywords name path =
221  (case lookup_command keywords name of
222    NONE => []
223  | SOME {kind, files, ...} =>
224      if kind <> thy_load then []
225      else if null files then [path]
226      else map (fn ext => Path.ext ext path) files);
227
228fun command_tags keywords name =
229  (case lookup_command keywords name of
230    SOME {tags, ...} => tags
231  | NONE => []);
232
233
234(* command categories *)
235
236fun command_category ks =
237  let
238    val tab = Symtab.make_set ks;
239    fun pred keywords name =
240      (case lookup_command keywords name of
241        NONE => false
242      | SOME {kind, ...} => Symtab.defined tab kind);
243  in pred end;
244
245val is_vacuous = command_category [diag, document_heading, document_body, document_raw];
246
247val is_diag = command_category [diag];
248
249val is_document_heading = command_category [document_heading];
250val is_document_body = command_category [document_body];
251val is_document_raw = command_category [document_raw];
252val is_document = command_category [document_heading, document_body, document_raw];
253
254val is_theory_end = command_category [thy_end];
255
256val is_theory_load = command_category [thy_load];
257
258val is_theory = command_category
259  [thy_begin, thy_end, thy_load, thy_decl, thy_decl_block, thy_goal];
260
261val is_theory_body = command_category
262  [thy_load, thy_decl, thy_decl_block, thy_goal];
263
264val is_proof = command_category
265  [qed, qed_script, qed_block, qed_global, prf_goal, prf_block, next_block, prf_open,
266    prf_close, prf_chain, prf_decl, prf_asm, prf_asm_goal, prf_script, prf_script_goal,
267    prf_script_asm_goal];
268
269val is_proof_body = command_category
270  [diag, document_heading, document_body, document_raw, prf_block, next_block, prf_open,
271    prf_close, prf_chain, prf_decl, prf_asm, prf_asm_goal, prf_script, prf_script_goal,
272    prf_script_asm_goal];
273
274val is_theory_goal = command_category [thy_goal];
275val is_proof_goal = command_category [prf_goal, prf_asm_goal, prf_script_goal, prf_script_asm_goal];
276val is_qed = command_category [qed, qed_script, qed_block];
277val is_qed_global = command_category [qed_global];
278
279val is_proof_open =
280  command_category [prf_goal, prf_asm_goal, prf_script_goal, prf_script_asm_goal, prf_open];
281val is_proof_close = command_category [qed, qed_script, qed_block, prf_close];
282
283val is_proof_asm = command_category [prf_asm, prf_asm_goal];
284val is_improper = command_category [qed_script, prf_script, prf_script_goal, prf_script_asm_goal];
285
286fun is_printed keywords = is_theory_goal keywords orf is_proof keywords;
287
288end;
289