# HG changeset patch # User wenzelm # Date 1230932528 -3600 # Node ID 868634981a32a8888aba9a72b35728be0697e265 # Parent ae6f2b1559fa71560e08f8388bda2e56753ee07a removed unused add_substring; back to simple list implementation; diff -r ae6f2b1559fa -r 868634981a32 src/Pure/General/buffer.ML --- 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;