--- 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.
--- 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 *)
--- 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