# HG changeset patch
# User wenzelm
# Date 1184168867 -7200
# Node ID ea7c2ee8a47ad87e3b3fb9057604244b42c76387
# Parent  75e6b9dd53367f62f792523d06cc3fe6cda1f021
added markup operation;

diff -r 75e6b9dd5336 -r ea7c2ee8a47a src/Pure/General/buffer.ML
--- 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);