src/Pure/General/buffer.ML
author wenzelm
Fri, 05 May 2000 22:02:46 +0200
changeset 8806 a202293db3f6
parent 7767 659648e14c3e
child 14981 e73f8140af78
permissions -rw-r--r--
GPLed;
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
8806
wenzelm
parents: 7767
diff changeset
     4
    License:    GPL (GNU GENERAL PUBLIC LICENSE)
6316
4a786a8a1a97 simple string buffers;
wenzelm
parents:
diff changeset
     5
4a786a8a1a97 simple string buffers;
wenzelm
parents:
diff changeset
     6
Simple string buffers.
4a786a8a1a97 simple string buffers;
wenzelm
parents:
diff changeset
     7
*)
4a786a8a1a97 simple string buffers;
wenzelm
parents:
diff changeset
     8
4a786a8a1a97 simple string buffers;
wenzelm
parents:
diff changeset
     9
signature BUFFER =
4a786a8a1a97 simple string buffers;
wenzelm
parents:
diff changeset
    10
sig
4a786a8a1a97 simple string buffers;
wenzelm
parents:
diff changeset
    11
  type T
4a786a8a1a97 simple string buffers;
wenzelm
parents:
diff changeset
    12
  val empty: T
4a786a8a1a97 simple string buffers;
wenzelm
parents:
diff changeset
    13
  val add: string -> T -> T
4a786a8a1a97 simple string buffers;
wenzelm
parents:
diff changeset
    14
  val content: T -> string
4a786a8a1a97 simple string buffers;
wenzelm
parents:
diff changeset
    15
  val write: Path.T -> T -> unit
4a786a8a1a97 simple string buffers;
wenzelm
parents:
diff changeset
    16
end;
4a786a8a1a97 simple string buffers;
wenzelm
parents:
diff changeset
    17
4a786a8a1a97 simple string buffers;
wenzelm
parents:
diff changeset
    18
structure Buffer: BUFFER =
4a786a8a1a97 simple string buffers;
wenzelm
parents:
diff changeset
    19
struct
4a786a8a1a97 simple string buffers;
wenzelm
parents:
diff changeset
    20
4a786a8a1a97 simple string buffers;
wenzelm
parents:
diff changeset
    21
datatype T = Buffer of string list;
4a786a8a1a97 simple string buffers;
wenzelm
parents:
diff changeset
    22
4a786a8a1a97 simple string buffers;
wenzelm
parents:
diff changeset
    23
val empty = Buffer [];
4a786a8a1a97 simple string buffers;
wenzelm
parents:
diff changeset
    24
fun add x (Buffer xs) = Buffer (x :: xs);
4a786a8a1a97 simple string buffers;
wenzelm
parents:
diff changeset
    25
fun content (Buffer xs) = implode (rev xs);
4a786a8a1a97 simple string buffers;
wenzelm
parents:
diff changeset
    26
fun write path buffer = File.write path (content buffer);
4a786a8a1a97 simple string buffers;
wenzelm
parents:
diff changeset
    27
4a786a8a1a97 simple string buffers;
wenzelm
parents:
diff changeset
    28
end;