# HG changeset patch
# User wenzelm
# Date 939226297 -7200
# Node ID 4b1bc1266c8c18e1a2e2879b1a55bb61fa87f6ff
# Parent  c9e7b053694a6848a9e805f12f42ba952b0f2fb6
added write_nonempty;

diff -r c9e7b053694a -r 4b1bc1266c8c src/Pure/General/buffer.ML
--- a/src/Pure/General/buffer.ML	Wed Oct 06 14:03:51 1999 +0200
+++ b/src/Pure/General/buffer.ML	Wed Oct 06 18:11:37 1999 +0200
@@ -12,6 +12,7 @@
   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 =
@@ -20,8 +21,13 @@
 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;