--- 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);