# HG changeset patch
# User wenzelm
# Date 1206997733 -7200
# Node ID 7f64d8cf6707db3edaf1e831cd3dcf19c98795ee
# Parent  494f418cc51c65206aab0728b36125a13400b886
added add_substring;
output: operate directly on stream;
tuned;

diff -r 494f418cc51c -r 7f64d8cf6707 src/Pure/General/buffer.ML
--- a/src/Pure/General/buffer.ML	Mon Mar 31 23:08:51 2008 +0200
+++ b/src/Pure/General/buffer.ML	Mon Mar 31 23:08:53 2008 +0200
@@ -2,7 +2,7 @@
     ID:         $Id$
     Author:     Markus Wenzel, TU Muenchen
 
-Efficient string buffers.
+Efficient text buffers.
 *)
 
 signature BUFFER =
@@ -10,30 +10,58 @@
   type T
   val empty: T
   val add: string -> T -> T
+  val add_substring: substring -> T -> T
   val markup: Markup.T -> (T -> T) -> T -> T
   val content: T -> string
+  val output: TextIO.outstream -> T -> unit
   val write: Path.T -> T -> unit
-  val output: (string -> unit) -> T -> unit
 end;
 
 structure Buffer: BUFFER =
 struct
 
-datatype T = Buffer of string list;
+(* datatype *)
+
+datatype T =
+    EmptyBuffer
+  | String of string * T
+  | Substring of substring * T;
 
-val empty = Buffer [];
+val empty = EmptyBuffer;
+
 
-fun add "" buf = buf
-  | add x (Buffer xs) = Buffer (x :: xs);
+(* add content *)
+
+fun add s buf = if s = "" then buf else String (s, buf);
+fun add_substring s buf = if Substring.isEmpty s then buf else Substring (s, buf);
 
 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);
+
+(* cumulative content *)
+
+fun rev_content EmptyBuffer acc = acc
+  | rev_content (String (s, buf)) acc = rev_content buf (s :: acc)
+  | rev_content (Substring (s, buf)) acc = rev_content buf (Substring.string s :: acc);
+
+fun content buf = implode (rev_content buf []);
+
+
+(* file output *)
 
-fun write path (Buffer xs) = File.write_list path (rev xs);
+fun rev_buffer EmptyBuffer acc = acc
+  | rev_buffer (String (s, buf)) acc = rev_buffer buf (String (s, acc))
+  | rev_buffer (Substring (s, buf)) acc = rev_buffer buf (Substring (s, acc));
 
-fun output f (Buffer xs) = List.app f (rev xs);
+fun output stream buffer =
+  let
+    fun rev_output EmptyBuffer = ()
+      | rev_output (String (s, buf)) = (TextIO.output (stream, s); rev_output buf)
+      | rev_output (Substring (s, buf)) = (TextIO.outputSubstr (stream, s); rev_output buf);
+  in rev_output (rev_buffer buffer empty) end;
+
+fun write path buf = File.open_output (fn stream => output stream buf) path;
 
 end;