--- a/src/Pure/General/buffer.ML Thu Oct 07 11:39:47 1999 +0200
+++ b/src/Pure/General/buffer.ML Thu Oct 07 12:19:21 1999 +0200
@@ -12,7 +12,6 @@
val add: string -> T -> T
val content: T -> string
val write: Path.T -> T -> unit
- val write_nonempty: Path.T -> T -> unit
end;
structure Buffer: BUFFER =
@@ -21,13 +20,8 @@
datatype T = Buffer of string list;
val empty = Buffer [];
-
fun add x (Buffer xs) = Buffer (x :: xs);
fun content (Buffer xs) = implode (rev xs);
-
fun write path buffer = File.write path (content buffer);
-fun write_nonempty _ (Buffer []) = ()
- | write_nonempty path buffer = write path buffer;
-
end;