# HG changeset patch
# User aspinall
# Date 1165184515 -3600
# Node ID d1ca26a2b91821975e510e0d9bbd57c6a8146266
# Parent  c762bdc2b504db2b0d69008af46aa79427b2f4f0
Add output function

diff -r c762bdc2b504 -r d1ca26a2b918 src/Pure/General/buffer.ML
--- 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;