src/Pure/General/buffer.ML
author paulson
Tue, 05 Sep 2000 10:16:03 +0200
changeset 9841 ca3173f87b5c
parent 8806 a202293db3f6
child 14981 e73f8140af78
permissions -rw-r--r--
safe_meson_tac -> meson_tac

(*  Title:      Pure/General/buffer.ML
    ID:         $Id$
    Author:     Markus Wenzel, TU Muenchen
    License:    GPL (GNU GENERAL PUBLIC LICENSE)

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 x (Buffer xs) = Buffer (x :: xs);
fun content (Buffer xs) = implode (rev xs);
fun write path buffer = File.write path (content buffer);

end;