# HG changeset patch # User wenzelm # Date 1236543157 -3600 # Node ID 1a2a54f910c98bfbcaa226b8638652025975baaf # Parent ee8841b1b981f729545d8223f05c7d1d2fea2c66 added (raw_)antiquotation -- simplified wrapper for defining output commands; diff -r ee8841b1b981 -r 1a2a54f910c9 src/Pure/Thy/thy_output.ML --- a/src/Pure/Thy/thy_output.ML Sun Mar 08 20:31:54 2009 +0100 +++ b/src/Pure/Thy/thy_output.ML Sun Mar 08 21:12:37 2009 +0100 @@ -18,6 +18,10 @@ val print_antiquotations: unit -> unit val boolean: string -> bool val integer: string -> int + val raw_antiquotation: string -> (Args.src -> Toplevel.state -> + Context.generic * Args.T list -> string * (Context.generic * Args.T list)) -> unit + val antiquotation: string -> (Args.src -> Proof.context -> + Context.generic * Args.T list -> string * (Context.generic * Args.T list)) -> unit val args: (Context.generic * Args.T list -> 'a * (Context.generic * Args.T list)) -> (Args.src -> Proof.context -> 'a -> string) -> Args.src -> Toplevel.state -> string datatype markup = Markup | MarkupEnv | Verbatim @@ -127,6 +131,14 @@ fun syntax scan = Args.context_syntax "document antiquotation" scan; +fun raw_antiquotation name scan = + add_commands [(name, fn src => fn state => + #1 (syntax (scan src state) src (Toplevel.presentation_context_of state NONE)))]; + +fun antiquotation name scan = + raw_antiquotation name (fn src => fn state => + scan src (Toplevel.presentation_context_of state NONE)); + fun args scan f src state : string = let val loc = if ! locale = "" then NONE else SOME (! locale);