src/Pure/Thy/thy_output.ML
changeset 29491 4f864f851f4d
parent 28644 e2ae4a6cf166
child 29606 fedb8be05f24
equal deleted inserted replaced
29490:8f0a481199e7 29491:4f864f851f4d
     9 sig
     9 sig
    10   val display: bool ref
    10   val display: bool ref
    11   val quotes: bool ref
    11   val quotes: bool ref
    12   val indent: int ref
    12   val indent: int ref
    13   val source: bool ref
    13   val source: bool ref
       
    14   val break: bool ref
    14   val add_commands: (string * (Args.src -> Toplevel.node option -> string)) list -> unit
    15   val add_commands: (string * (Args.src -> Toplevel.node option -> string)) list -> unit
    15   val add_options: (string * (string -> (unit -> string) -> unit -> string)) list -> unit
    16   val add_options: (string * (string -> (unit -> string) -> unit -> string)) list -> unit
    16   val defined_command: string -> bool
    17   val defined_command: string -> bool
    17   val defined_option: string -> bool
    18   val defined_option: string -> bool
    18   val print_antiquotations: unit -> unit
    19   val print_antiquotations: unit -> unit