equal
deleted
inserted
replaced
46 val command_tags: string -> string list |
46 val command_tags: string -> string list |
47 val keyword_statusN: string |
47 val keyword_statusN: string |
48 val status: unit -> unit |
48 val status: unit -> unit |
49 val keyword: string -> unit |
49 val keyword: string -> unit |
50 val command: string -> T -> unit |
50 val command: string -> T -> unit |
|
51 val declare: string * (string * string list) option -> unit |
51 val is_diag: string -> bool |
52 val is_diag: string -> bool |
52 val is_control: string -> bool |
53 val is_control: string -> bool |
53 val is_regular: string -> bool |
54 val is_regular: string -> bool |
54 val is_heading: string -> bool |
55 val is_heading: string -> bool |
55 val is_theory_begin: string -> bool |
56 val is_theory_begin: string -> bool |
212 fun command name kind = |
213 fun command name kind = |
213 (change_lexicons (apsnd (Scan.extend_lexicon (Symbol.explode name))); |
214 (change_lexicons (apsnd (Scan.extend_lexicon (Symbol.explode name))); |
214 change_commands (Symtab.update (name, kind)); |
215 change_commands (Symtab.update (name, kind)); |
215 command_status (name, kind)); |
216 command_status (name, kind)); |
216 |
217 |
|
218 fun declare (name, NONE) = keyword name |
|
219 | declare (name, SOME kind) = command name (make kind); |
|
220 |
217 |
221 |
218 (* command categories *) |
222 (* command categories *) |
219 |
223 |
220 fun command_category ks name = |
224 fun command_category ks name = |
221 (case command_keyword name of |
225 (case command_keyword name of |