src/Pure/General/buffer.ML
author wenzelm
Fri Dec 14 11:52:54 2001 +0100 (2001-12-14)
changeset 12498 3b0091bf06e8
parent 8806 a202293db3f6
child 14981 e73f8140af78
permissions -rw-r--r--
changed Thm.varifyT';
wenzelm@6316
     1
(*  Title:      Pure/General/buffer.ML
wenzelm@6316
     2
    ID:         $Id$
wenzelm@6316
     3
    Author:     Markus Wenzel, TU Muenchen
wenzelm@8806
     4
    License:    GPL (GNU GENERAL PUBLIC LICENSE)
wenzelm@6316
     5
wenzelm@6316
     6
Simple string buffers.
wenzelm@6316
     7
*)
wenzelm@6316
     8
wenzelm@6316
     9
signature BUFFER =
wenzelm@6316
    10
sig
wenzelm@6316
    11
  type T
wenzelm@6316
    12
  val empty: T
wenzelm@6316
    13
  val add: string -> T -> T
wenzelm@6316
    14
  val content: T -> string
wenzelm@6316
    15
  val write: Path.T -> T -> unit
wenzelm@6316
    16
end;
wenzelm@6316
    17
wenzelm@6316
    18
structure Buffer: BUFFER =
wenzelm@6316
    19
struct
wenzelm@6316
    20
wenzelm@6316
    21
datatype T = Buffer of string list;
wenzelm@6316
    22
wenzelm@6316
    23
val empty = Buffer [];
wenzelm@6316
    24
fun add x (Buffer xs) = Buffer (x :: xs);
wenzelm@6316
    25
fun content (Buffer xs) = implode (rev xs);
wenzelm@6316
    26
fun write path buffer = File.write path (content buffer);
wenzelm@6316
    27
wenzelm@6316
    28
end;