# HG changeset patch
# User wenzelm
# Date 1236610195 -3600
# Node ID 85c7ffbfac17bdb484a958998959a877e1806812
# Parent  72ac3d101a68b4054f2b274f6ac56262aceb4515# Parent  ee2c7592e59f55c17553d9f359c65a69fa992cbc
merged

diff -r 72ac3d101a68 -r 85c7ffbfac17 CONTRIBUTORS
--- a/CONTRIBUTORS	Mon Mar 09 14:44:04 2009 +0100
+++ b/CONTRIBUTORS	Mon Mar 09 15:49:55 2009 +0100
@@ -7,6 +7,10 @@
 Contributions to this Isabelle version
 --------------------------------------
 
+* March 2009: Robert Himmelmann, TUM and Amine Chaieb, University of
+  Cambridge
+  Elementary topology in Euclidean space.
+
 * February 2009: Filip Maric, Univ. of Belgrade
   A Serbian theory.
 
diff -r 72ac3d101a68 -r 85c7ffbfac17 doc-src/antiquote_setup.ML
--- a/doc-src/antiquote_setup.ML	Mon Mar 09 14:44:04 2009 +0100
+++ b/doc-src/antiquote_setup.ML	Mon Mar 09 15:49:55 2009 +0100
@@ -35,8 +35,8 @@
 
 val verbatim = space_implode "\\verb,|," o map (enclose "\\verb|" "|") o space_explode "|";
 
-val _ = ThyOutput.antiquotation "verbatim" (fn _ => fn _ =>
-  Scan.lift Args.name >> (split_lines #> map verbatim #> space_implode "\\isasep\\isanewline%\n"));
+val _ = ThyOutput.antiquotation "verbatim" (Scan.lift Args.name)
+  (K (split_lines #> map verbatim #> space_implode "\\isasep\\isanewline%\n"));
 
 
 (* ML text *)
diff -r 72ac3d101a68 -r 85c7ffbfac17 src/Pure/Thy/thy_output.ML
--- a/src/Pure/Thy/thy_output.ML	Mon Mar 09 14:44:04 2009 +0100
+++ b/src/Pure/Thy/thy_output.ML	Mon Mar 09 15:49:55 2009 +0100
@@ -18,10 +18,9 @@
   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 antiquotation: string ->
+    (Context.generic * Args.T list -> 'a * (Context.generic * Args.T list)) ->
+    ({state: Toplevel.state, source: Args.src, context: Proof.context} -> 'a -> string) -> 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
@@ -131,13 +130,10 @@
 
 fun syntax scan = Args.context_syntax "document antiquotation" scan;
 
-fun raw_antiquotation name scan =
+fun antiquotation name scan output =
   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));
+    let val (x, ctxt) = syntax scan src (Toplevel.presentation_context_of state NONE);
+    in output {source = src, state = state, context = ctxt} x end)];
 
 fun args scan f src state : string =
   let