Add output function

--- a/src/Pure/General/buffer.ML	Sun Dec 03 21:46:54 2006 +0100
+++ b/src/Pure/General/buffer.ML	Sun Dec 03 23:21:55 2006 +0100
@@ -12,6 +12,7 @@
   val add: string -> T -> T
   val content: T -> string
   val write: Path.T -> T -> unit
+  val output: (string -> unit) -> T -> unit
 end;
 
 structure Buffer: BUFFER =
@@ -28,4 +29,6 @@
 
 fun write path (Buffer xs) = File.write_list path (rev xs);
 
+fun output f (Buffer xs) = Library.seq f (rev xs);
+
 end;