1.1 --- a/src/Pure/Thy/thy_output.ML Sun Mar 08 20:31:54 2009 +0100
1.2 +++ b/src/Pure/Thy/thy_output.ML Sun Mar 08 21:12:37 2009 +0100
1.3 @@ -18,6 +18,10 @@
1.4 val print_antiquotations: unit -> unit
1.5 val boolean: string -> bool
1.6 val integer: string -> int
1.7 + val raw_antiquotation: string -> (Args.src -> Toplevel.state ->
1.8 + Context.generic * Args.T list -> string * (Context.generic * Args.T list)) -> unit
1.9 + val antiquotation: string -> (Args.src -> Proof.context ->
1.10 + Context.generic * Args.T list -> string * (Context.generic * Args.T list)) -> unit
1.11 val args: (Context.generic * Args.T list -> 'a * (Context.generic * Args.T list)) ->
1.12 (Args.src -> Proof.context -> 'a -> string) -> Args.src -> Toplevel.state -> string
1.13 datatype markup = Markup | MarkupEnv | Verbatim
1.14 @@ -127,6 +131,14 @@
1.15
1.16 fun syntax scan = Args.context_syntax "document antiquotation" scan;
1.17
1.18 +fun raw_antiquotation name scan =
1.19 + add_commands [(name, fn src => fn state =>
1.20 + #1 (syntax (scan src state) src (Toplevel.presentation_context_of state NONE)))];
1.21 +
1.22 +fun antiquotation name scan =
1.23 + raw_antiquotation name (fn src => fn state =>
1.24 + scan src (Toplevel.presentation_context_of state NONE));
1.25 +
1.26 fun args scan f src state : string =
1.27 let
1.28 val loc = if ! locale = "" then NONE else SOME (! locale);