src/Pure/General/buffer.ML
author wenzelm
Wed, 09 Nov 2005 16:26:47 +0100
changeset 18132 0e9c9a18f454
parent 17062 7272b45099c7
child 21630 d1ca26a2b918
permissions -rw-r--r--
tuned comments;
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
18132
0e9c9a18f454 tuned comments;
wenzelm
parents: 17062
diff changeset
     5
Efficient string buffers.
6316
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 [];
17062
7272b45099c7 tuned Buffer.add;
wenzelm
parents: 16712
diff changeset
    23
7272b45099c7 tuned Buffer.add;
wenzelm
parents: 16712
diff changeset
    24
fun add "" buf = buf
7272b45099c7 tuned Buffer.add;
wenzelm
parents: 16712
diff changeset
    25
  | add x (Buffer xs) = Buffer (x :: xs);
7272b45099c7 tuned Buffer.add;
wenzelm
parents: 16712
diff changeset
    26
6316
4a786a8a1a97 simple string buffers;
wenzelm
parents:
diff changeset
    27
fun content (Buffer xs) = implode (rev xs);
17062
7272b45099c7 tuned Buffer.add;
wenzelm
parents: 16712
diff changeset
    28
16712
c7d1c79d921c tuned write: use File.write_list;
wenzelm
parents: 14981
diff changeset
    29
fun write path (Buffer xs) = File.write_list path (rev xs);
6316
4a786a8a1a97 simple string buffers;
wenzelm
parents:
diff changeset
    30
4a786a8a1a97 simple string buffers;
wenzelm
parents:
diff changeset
    31
end;