src/Pure/General/buffer.ML
author wenzelm
Tue, 09 Mar 1999 12:08:50 +0100
changeset 6316 4a786a8a1a97
child 7754 4b1bc1266c8c
permissions -rw-r--r--
simple string buffers;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
6316
4a786a8a1a97 simple string buffers;
wenzelm
parents:
diff changeset
     1
(*  Title:      Pure/General/buffer.ML
4a786a8a1a97 simple string buffers;
wenzelm
parents:
diff changeset
     2
    ID:         $Id$
4a786a8a1a97 simple string buffers;
wenzelm
parents:
diff changeset
     3
    Author:     Markus Wenzel, TU Muenchen
4a786a8a1a97 simple string buffers;
wenzelm
parents:
diff changeset
     4
4a786a8a1a97 simple string buffers;
wenzelm
parents:
diff changeset
     5
Simple string buffers.
4a786a8a1a97 simple string buffers;
wenzelm
parents:
diff changeset
     6
*)
4a786a8a1a97 simple string buffers;
wenzelm
parents:
diff changeset
     7
4a786a8a1a97 simple string buffers;
wenzelm
parents:
diff changeset
     8
signature BUFFER =
4a786a8a1a97 simple string buffers;
wenzelm
parents:
diff changeset
     9
sig
4a786a8a1a97 simple string buffers;
wenzelm
parents:
diff changeset
    10
  type T
4a786a8a1a97 simple string buffers;
wenzelm
parents:
diff changeset
    11
  val empty: T
4a786a8a1a97 simple string buffers;
wenzelm
parents:
diff changeset
    12
  val add: string -> T -> T
4a786a8a1a97 simple string buffers;
wenzelm
parents:
diff changeset
    13
  val content: T -> string
4a786a8a1a97 simple string buffers;
wenzelm
parents:
diff changeset
    14
  val write: Path.T -> T -> unit
4a786a8a1a97 simple string buffers;
wenzelm
parents:
diff changeset
    15
end;
4a786a8a1a97 simple string buffers;
wenzelm
parents:
diff changeset
    16
4a786a8a1a97 simple string buffers;
wenzelm
parents:
diff changeset
    17
structure Buffer: BUFFER =
4a786a8a1a97 simple string buffers;
wenzelm
parents:
diff changeset
    18
struct
4a786a8a1a97 simple string buffers;
wenzelm
parents:
diff changeset
    19
4a786a8a1a97 simple string buffers;
wenzelm
parents:
diff changeset
    20
datatype T = Buffer of string list;
4a786a8a1a97 simple string buffers;
wenzelm
parents:
diff changeset
    21
4a786a8a1a97 simple string buffers;
wenzelm
parents:
diff changeset
    22
val empty = Buffer [];
4a786a8a1a97 simple string buffers;
wenzelm
parents:
diff changeset
    23
fun add x (Buffer xs) = Buffer (x :: xs);
4a786a8a1a97 simple string buffers;
wenzelm
parents:
diff changeset
    24
fun content (Buffer xs) = implode (rev xs);
4a786a8a1a97 simple string buffers;
wenzelm
parents:
diff changeset
    25
fun write path buffer = File.write path (content buffer);
4a786a8a1a97 simple string buffers;
wenzelm
parents:
diff changeset
    26
4a786a8a1a97 simple string buffers;
wenzelm
parents:
diff changeset
    27
end;