31 val prf_asm_goal: string |
31 val prf_asm_goal: string |
32 val prf_script: string |
32 val prf_script: string |
33 val prf_script_goal: string |
33 val prf_script_goal: string |
34 val prf_script_asm_goal: string |
34 val prf_script_asm_goal: string |
35 type spec = (string * string list) * string list |
35 type spec = (string * string list) * string list |
|
36 val no_spec: spec |
36 type keywords |
37 type keywords |
37 val minor_keywords: keywords -> Scan.lexicon |
38 val minor_keywords: keywords -> Scan.lexicon |
38 val major_keywords: keywords -> Scan.lexicon |
39 val major_keywords: keywords -> Scan.lexicon |
39 val no_command_keywords: keywords -> keywords |
40 val no_command_keywords: keywords -> keywords |
40 val empty_keywords: keywords |
41 val empty_keywords: keywords |
41 val merge_keywords: keywords * keywords -> keywords |
42 val merge_keywords: keywords * keywords -> keywords |
42 val add_keywords: ((string * Position.T) * spec option) list -> keywords -> keywords |
43 val add_keywords: ((string * Position.T) * spec) list -> keywords -> keywords |
43 val is_keyword: keywords -> string -> bool |
44 val is_keyword: keywords -> string -> bool |
44 val is_command: keywords -> string -> bool |
45 val is_command: keywords -> string -> bool |
45 val is_literal: keywords -> string -> bool |
46 val is_literal: keywords -> string -> bool |
46 val dest_commands: keywords -> string list |
47 val dest_commands: keywords -> string list |
47 val command_markup: keywords -> string -> Markup.T option |
48 val command_markup: keywords -> string -> Markup.T option |
127 if not (member (op =) kinds kind) then |
130 if not (member (op =) kinds kind) then |
128 error ("Unknown outer syntax keyword kind " ^ quote kind) |
131 error ("Unknown outer syntax keyword kind " ^ quote kind) |
129 else if not (null files) andalso kind <> thy_load then |
132 else if not (null files) andalso kind <> thy_load then |
130 error ("Illegal specification of files for " ^ quote kind) |
133 error ("Illegal specification of files for " ^ quote kind) |
131 else {pos = pos, id = serial (), kind = kind, files = files, tags = tags}; |
134 else {pos = pos, id = serial (), kind = kind, files = files, tags = tags}; |
132 |
|
133 |
135 |
134 |
136 |
135 (** keyword tables **) |
137 (** keyword tables **) |
136 |
138 |
137 (* type keywords *) |
139 (* type keywords *) |
166 (Scan.merge_lexicons (minor1, minor2), |
168 (Scan.merge_lexicons (minor1, minor2), |
167 Scan.merge_lexicons (major1, major2), |
169 Scan.merge_lexicons (major1, major2), |
168 Symtab.merge (K true) (commands1, commands2)); |
170 Symtab.merge (K true) (commands1, commands2)); |
169 |
171 |
170 val add_keywords = |
172 val add_keywords = |
171 fold (fn ((name, pos), opt_spec) => map_keywords (fn (minor, major, commands) => |
173 fold (fn ((name, pos), spec as ((kind, _), _)) => map_keywords (fn (minor, major, commands) => |
172 (case opt_spec of |
174 if kind = "" then |
173 NONE => |
175 let |
174 let |
176 val minor' = Scan.extend_lexicon (Symbol.explode name) minor; |
175 val minor' = Scan.extend_lexicon (Symbol.explode name) minor; |
177 in (minor', major, commands) end |
176 in (minor', major, commands) end |
178 else |
177 | SOME spec => |
179 let |
178 let |
180 val entry = check_spec pos spec; |
179 val entry = check_spec pos spec; |
181 val major' = Scan.extend_lexicon (Symbol.explode name) major; |
180 val major' = Scan.extend_lexicon (Symbol.explode name) major; |
182 val commands' = Symtab.update (name, entry) commands; |
181 val commands' = Symtab.update (name, entry) commands; |
183 in (minor, major', commands') end)); |
182 in (minor, major', commands') end))); |
|
183 |
184 |
184 |
185 |
185 (* keyword status *) |
186 (* keyword status *) |
186 |
187 |
187 fun is_keyword keywords s = Scan.is_literal (minor_keywords keywords) (Symbol.explode s); |
188 fun is_keyword keywords s = Scan.is_literal (minor_keywords keywords) (Symbol.explode s); |