src/Pure/General/buffer.ML
author wenzelm
Tue, 19 Jul 2005 20:47:01 +0200
changeset 16894 40f80823b451
parent 16712 c7d1c79d921c
child 17062 7272b45099c7
permissions -rw-r--r--
Inttab.defined;
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);
16712
c7d1c79d921c tuned write: use File.write_list;
wenzelm
parents: 14981
diff changeset
    25
fun write path (Buffer xs) = File.write_list path (rev xs);
6316
4a786a8a1a97 simple string buffers;
wenzelm
parents:
diff changeset
    26
4a786a8a1a97 simple string buffers;
wenzelm
parents:
diff changeset
    27
end;