src/Pure/General/buffer.ML
author haftmann
Wed, 21 Sep 2005 10:32:24 +0200
changeset 17540 f662416aa5f2
parent 17062 7272b45099c7
child 18132 0e9c9a18f454
permissions -rw-r--r--
removed assoc, overwrite

(*  Title:      Pure/General/buffer.ML
    ID:         $Id$
    Author:     Markus Wenzel, TU Muenchen

Simple string buffers.
*)

signature BUFFER =
sig
  type T
  val empty: T
  val add: string -> T -> T
  val content: T -> string
  val write: Path.T -> T -> unit
end;

structure Buffer: BUFFER =
struct

datatype T = Buffer of string list;

val empty = Buffer [];

fun add "" buf = buf
  | add x (Buffer xs) = Buffer (x :: xs);

fun content (Buffer xs) = implode (rev xs);

fun write path (Buffer xs) = File.write_list path (rev xs);

end;