# HG changeset patch # User wenzelm # Date 1210789853 -7200 # Node ID 44d9960d358756b6e6d3b709a1cf1dfd53506156 # Parent 9454a8bd1114d8dd1059c893d979c528a383020f added defined_command, defined_option; diff -r 9454a8bd1114 -r 44d9960d3587 src/Pure/Thy/thy_output.ML --- a/src/Pure/Thy/thy_output.ML Wed May 14 20:30:29 2008 +0200 +++ b/src/Pure/Thy/thy_output.ML Wed May 14 20:30:53 2008 +0200 @@ -13,6 +13,8 @@ val source: bool ref val add_commands: (string * (Args.src -> Toplevel.node option -> string)) list -> unit val add_options: (string * (string -> (unit -> string) -> unit -> string)) list -> unit + val defined_command: string -> bool + val defined_option: string -> bool val print_antiquotations: unit -> unit val boolean: string -> bool val integer: string -> int @@ -66,6 +68,9 @@ fun add_commands xs = CRITICAL (fn () => change global_commands (fold (add_item "command") xs)); fun add_options xs = CRITICAL (fn () => change global_options (fold (add_item "option") xs)); +fun defined_command name = Symtab.defined (! global_commands) name; +fun defined_option name = Symtab.defined (! global_options) name; + fun command src = let val ((name, _), pos) = Args.dest_src src in (case Symtab.lookup (! global_commands) name of