--- 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;