# 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