removed unused add_substring;
back to simple list implementation;

--- a/src/Pure/General/buffer.ML	Fri Jan 02 22:41:42 2009 +0100
+++ b/src/Pure/General/buffer.ML	Fri Jan 02 22:42:08 2009 +0100
@@ -1,5 +1,4 @@
 (*  Title:      Pure/General/buffer.ML
-    ID:         $Id$
     Author:     Markus Wenzel, TU Muenchen
 
 Efficient text buffers.
@@ -10,7 +9,6 @@
   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: T -> TextIO.outstream -> unit
@@ -19,46 +17,18 @@
 structure Buffer: BUFFER =
 struct
 
-(* datatype *)
-
-datatype T =
-    EmptyBuffer
-  | String of string * T
-  | Substring of substring * T;
+datatype T = Buffer of string list;
 
-val empty = EmptyBuffer;
-
+val empty = Buffer [];
 
-(* 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 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;
 
-
-(* 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 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 buffer stream =
-  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 content (Buffer xs) = implode (rev xs);
+fun output (Buffer xs) stream = List.app (fn s => TextIO.output (stream, s)) (rev xs);
 
 end;