# HG changeset patch
# User wenzelm
# Date 1120639307 -7200
# Node ID be576390178834a05f8d0ad33872b627c651175c
# Parent  c7d1c79d921cfc001331e2bb7a9f38e6f833519f
added write_list, append_list;

diff -r c7d1c79d921c -r be5763901788 src/Pure/General/file.ML
--- a/src/Pure/General/file.ML	Wed Jul 06 10:41:46 2005 +0200
+++ b/src/Pure/General/file.ML	Wed Jul 06 10:41:47 2005 +0200
@@ -22,6 +22,8 @@
   val read: Path.T -> string
   val write: Path.T -> string -> unit
   val append: Path.T -> string -> unit
+  val write_list: Path.T -> string list -> unit
+  val append_list: Path.T -> string list -> unit
   val eq: Path.T * Path.T -> bool
   val copy: Path.T -> Path.T -> unit
   val copy_dir: Path.T -> Path.T -> unit
@@ -107,18 +109,21 @@
   let val y = f x handle exn => (g x; raise exn)
   in g x; y end;
 
-fun output txt stream = TextIO.output (stream, txt);
+fun output txts stream = List.app (fn txt => TextIO.output (stream, txt)) txts;
 
 in
 
 fun read path =
   fail_safe TextIO.inputAll TextIO.closeIn (TextIO.openIn (platform_path path));
 
-fun write path txt =
-  fail_safe (output txt) TextIO.closeOut (TextIO.openOut (platform_path path));
+fun write_list path txts =
+  fail_safe (output txts) TextIO.closeOut (TextIO.openOut (platform_path path));
 
-fun append path txt =
-  fail_safe (output txt) TextIO.closeOut (TextIO.openAppend (platform_path path));
+fun append_list path txts =
+  fail_safe (output txts) TextIO.closeOut (TextIO.openAppend (platform_path path));
+
+fun write path txt = write_list path [txt];
+fun append path txt = append_list path [txt];
 
 end;