# HG changeset patch
# User wenzelm
# Date 1120639308 -7200
# Node ID d9e3ef66b38cf7cd0d7fec4b78a66a2a913ec294
# Parent  be576390178834a05f8d0ad33872b627c651175c
added output_buffer;

diff -r be5763901788 -r d9e3ef66b38c src/Pure/General/pretty.ML
--- a/src/Pure/General/pretty.ML	Wed Jul 06 10:41:47 2005 +0200
+++ b/src/Pure/General/pretty.ML	Wed Jul 06 10:41:48 2005 +0200
@@ -45,6 +45,7 @@
   val chunks: T list -> T
   val indent: int -> T -> T
   val string_of: T -> string
+  val output_buffer: T -> Buffer.T
   val output: T -> string
   val writeln: T -> unit
   val writelns: T list -> unit
@@ -240,9 +241,8 @@
 
 fun prune dp e = if dp > 0 then pruning dp e else e;
 
-fun output e =
-  Buffer.content (#tx (format ([prune (! depth) e], (Buffer.empty, 0), 0) empty));
-
+fun output_buffer e = #tx (format ([prune (! depth) e], (Buffer.empty, 0), 0) empty);
+val output = Buffer.content o output_buffer;
 val string_of = Output.raw o output;
 val writeln = writeln o string_of;
 fun writelns [] = () | writelns es = writeln (chunks es);