1.1 --- a/src/Pure/Thy/thy_output.ML	Mon Mar 09 10:10:34 2009 +0100
     1.2 +++ b/src/Pure/Thy/thy_output.ML	Mon Mar 09 11:56:34 2009 +0100
     1.3 @@ -18,10 +18,9 @@
     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 antiquotation: string ->
    1.12 +    (Context.generic * Args.T list -> 'a * (Context.generic * Args.T list)) ->
    1.13 +    ({state: Toplevel.state, source: Args.src, context: Proof.context} -> 'a -> string) -> unit
    1.14    val args: (Context.generic * Args.T list -> 'a * (Context.generic * Args.T list)) ->
    1.15      (Args.src -> Proof.context -> 'a -> string) -> Args.src -> Toplevel.state -> string
    1.16    datatype markup = Markup | MarkupEnv | Verbatim
    1.17 @@ -131,13 +130,10 @@
    1.18  
    1.19  fun syntax scan = Args.context_syntax "document antiquotation" scan;
    1.20  
    1.21 -fun raw_antiquotation name scan =
    1.22 +fun antiquotation name scan output =
    1.23    add_commands [(name, fn src => fn state =>
    1.24 -    #1 (syntax (scan src state) src (Toplevel.presentation_context_of state NONE)))];
    1.25 -
    1.26 -fun antiquotation name scan =
    1.27 -  raw_antiquotation name (fn src => fn state =>
    1.28 -    scan src (Toplevel.presentation_context_of state NONE));
    1.29 +    let val (x, ctxt) = syntax scan src (Toplevel.presentation_context_of state NONE);
    1.30 +    in output {source = src, state = state, context = ctxt} x end)];
    1.31  
    1.32  fun args scan f src state : string =
    1.33    let