45 val tag_proof: T -> T |
45 val tag_proof: T -> T |
46 val tag_ml: T -> T |
46 val tag_ml: T -> T |
47 type spec = (string * string list) * string list |
47 type spec = (string * string list) * string list |
48 val spec: spec -> T |
48 val spec: spec -> T |
49 val command_spec: (string * spec) * Position.T -> (string * T) * Position.T |
49 val command_spec: (string * spec) * Position.T -> (string * T) * Position.T |
50 type keywords |
|
51 val lexicons_of: keywords -> Scan.lexicon * Scan.lexicon |
|
52 val get_keywords: unit -> keywords |
|
53 val get_lexicons: unit -> Scan.lexicon * Scan.lexicon |
50 val get_lexicons: unit -> Scan.lexicon * Scan.lexicon |
54 val is_keyword: string -> bool |
51 val is_keyword: string -> bool |
55 val command_keyword: string -> T option |
52 val command_keyword: string -> T option |
56 val command_files: string -> string list |
53 val command_files: string -> string list |
57 val command_tags: string -> string list |
54 val command_tags: string -> string list |
58 val dest: unit -> string list * string list |
55 val dest: unit -> string list * string list |
59 val status: unit -> unit |
56 val status: unit -> unit |
60 val define_keywords: string * T option -> keywords -> keywords |
|
61 val define: string * T option -> unit |
57 val define: string * T option -> unit |
62 val is_diag: string -> bool |
58 val is_diag: string -> bool |
63 val is_control: string -> bool |
59 val is_control: string -> bool |
64 val is_regular: string -> bool |
60 val is_regular: string -> bool |
65 val is_heading: string -> bool |
61 val is_heading: string -> bool |
169 commands: T Symtab.table}; (*command classification*) |
165 commands: T Symtab.table}; (*command classification*) |
170 |
166 |
171 fun make_keywords (lexicons, commands) = |
167 fun make_keywords (lexicons, commands) = |
172 Keywords {lexicons = lexicons, commands = commands}; |
168 Keywords {lexicons = lexicons, commands = commands}; |
173 |
169 |
174 fun map_keywords f (Keywords {lexicons, commands}) = |
|
175 make_keywords (f (lexicons, commands)); |
|
176 |
|
177 fun lexicons_of (Keywords {lexicons, ...}) = lexicons; |
|
178 |
|
179 local |
170 local |
180 |
171 |
181 val global_keywords = |
172 val global_keywords = |
182 Unsynchronized.ref (make_keywords ((Scan.empty_lexicon, Scan.empty_lexicon), Symtab.empty)); |
173 Unsynchronized.ref (make_keywords ((Scan.empty_lexicon, Scan.empty_lexicon), Symtab.empty)); |
183 |
174 |
184 in |
175 in |
185 |
176 |
186 fun get_keywords () = ! global_keywords; |
177 fun get_keywords () = ! global_keywords; |
187 |
178 |
188 fun change_keywords f = CRITICAL (fn () => Unsynchronized.change global_keywords f); |
179 fun change_keywords f = CRITICAL (fn () => |
|
180 Unsynchronized.change global_keywords |
|
181 (fn Keywords {lexicons, commands} => make_keywords (f (lexicons, commands)))); |
189 |
182 |
190 end; |
183 end; |
191 |
184 |
192 fun get_lexicons () = lexicons_of (get_keywords ()); |
185 fun get_lexicons () = get_keywords () |> (fn Keywords {lexicons, ...} => lexicons); |
193 fun get_commands () = get_keywords () |> (fn Keywords {commands, ...} => commands); |
186 fun get_commands () = get_keywords () |> (fn Keywords {commands, ...} => commands); |
194 |
187 |
195 |
188 |
196 (* lookup *) |
189 (* lookup *) |
197 |
190 |
220 in () end; |
213 in () end; |
221 |
214 |
222 |
215 |
223 (* define *) |
216 (* define *) |
224 |
217 |
225 fun define_keywords (name, opt_kind) = map_keywords (fn ((minor, major), commands) => |
218 fun define (name, opt_kind) = change_keywords (fn ((minor, major), commands) => |
226 (case opt_kind of |
219 (case opt_kind of |
227 NONE => |
220 NONE => |
228 let |
221 let |
229 val minor' = Scan.extend_lexicon (Symbol.explode name) minor; |
222 val minor' = Scan.extend_lexicon (Symbol.explode name) minor; |
230 in ((minor', major), commands) end |
223 in ((minor', major), commands) end |
232 let |
225 let |
233 val major' = Scan.extend_lexicon (Symbol.explode name) major; |
226 val major' = Scan.extend_lexicon (Symbol.explode name) major; |
234 val commands' = Symtab.update (name, kind) commands; |
227 val commands' = Symtab.update (name, kind) commands; |
235 in ((minor, major'), commands') end)); |
228 in ((minor, major'), commands') end)); |
236 |
229 |
237 val define = change_keywords o define_keywords; |
|
238 |
|
239 |
230 |
240 (* command categories *) |
231 (* command categories *) |
241 |
232 |
242 fun command_category ks name = |
233 fun command_category ks name = |
243 (case command_keyword name of |
234 (case command_keyword name of |