added write_nonempty;

--- 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;