src/Pure/Thy/thy_output.ML
changeset 26893 44d9960d3587
parent 26762 78ed28528ca6
child 26996 090a619e7d87
     1.1 --- a/src/Pure/Thy/thy_output.ML	Wed May 14 20:30:29 2008 +0200
     1.2 +++ b/src/Pure/Thy/thy_output.ML	Wed May 14 20:30:53 2008 +0200
     1.3 @@ -13,6 +13,8 @@
     1.4    val source: bool ref
     1.5    val add_commands: (string * (Args.src -> Toplevel.node option -> string)) list -> unit
     1.6    val add_options: (string * (string -> (unit -> string) -> unit -> string)) list -> unit
     1.7 +  val defined_command: string -> bool
     1.8 +  val defined_option: string -> bool
     1.9    val print_antiquotations: unit -> unit
    1.10    val boolean: string -> bool
    1.11    val integer: string -> int
    1.12 @@ -66,6 +68,9 @@
    1.13  fun add_commands xs = CRITICAL (fn () => change global_commands (fold (add_item "command") xs));
    1.14  fun add_options xs = CRITICAL (fn () => change global_options (fold (add_item "option") xs));
    1.15  
    1.16 +fun defined_command name = Symtab.defined (! global_commands) name;
    1.17 +fun defined_option name = Symtab.defined (! global_options) name;
    1.18 +
    1.19  fun command src =
    1.20    let val ((name, _), pos) = Args.dest_src src in
    1.21      (case Symtab.lookup (! global_commands) name of