added markup operation;

--- a/src/Pure/General/buffer.ML	Wed Jul 11 17:47:45 2007 +0200
+++ b/src/Pure/General/buffer.ML	Wed Jul 11 17:47:47 2007 +0200
@@ -10,6 +10,7 @@
   type T
   val empty: T
   val add: string -> T -> T
+  val markup: Markup.T -> (T -> T) -> T -> T
   val content: T -> string
   val write: Path.T -> T -> unit
   val output: (string -> unit) -> T -> unit
@@ -25,6 +26,10 @@
 fun add "" buf = buf
   | add x (Buffer xs) = Buffer (x :: xs);
 
+fun markup m body =
+  let val (bg, en) = Markup.output m
+  in add bg #> body #> add en end;
+
 fun content (Buffer xs) = implode (rev xs);
 
 fun write path (Buffer xs) = File.write_list path (rev xs);