# HG changeset patch
# User wenzelm
# Date 1219862186 -7200
# Node ID 051d5ccbafc5bb73e93d3fb7bc6fc5a3d764283f
# Parent  dad9a2f178acf260fde45d556d63d5a61009e0f9
renamed Buffer.write to File.write_buffer;

diff -r dad9a2f178ac -r 051d5ccbafc5 src/Pure/General/buffer.ML
--- a/src/Pure/General/buffer.ML	Wed Aug 27 20:36:25 2008 +0200
+++ b/src/Pure/General/buffer.ML	Wed Aug 27 20:36:26 2008 +0200
@@ -14,7 +14,6 @@
   val markup: Markup.T -> (T -> T) -> T -> T
   val content: T -> string
   val output: T -> TextIO.outstream -> unit
-  val write: Path.T -> T -> unit
 end;
 
 structure Buffer: BUFFER =
@@ -62,6 +61,4 @@
       | rev_output (Substring (s, buf)) = (TextIO.outputSubstr (stream, s); rev_output buf);
   in rev_output (rev_buffer buffer empty) end;
 
-fun write path buf = File.open_output (output buf) path;
-
 end;
diff -r dad9a2f178ac -r 051d5ccbafc5 src/Pure/Thy/present.ML
--- a/src/Pure/Thy/present.ML	Wed Aug 27 20:36:25 2008 +0200
+++ b/src/Pure/Thy/present.ML	Wed Aug 27 20:36:26 2008 +0200
@@ -359,7 +359,7 @@
 fun index_buffer index = Buffer.add (implode (sorted_index index)) Buffer.empty;
 
 fun write_tex src name path =
-  Buffer.write (Path.append path (tex_path name)) src;
+  File.write_buffer (Path.append path (tex_path name)) src;
 
 fun write_tex_index tex_index path =
   write_tex (index_buffer tex_index |> Buffer.add Latex.tex_trailer) doc_indexN path;
@@ -375,7 +375,7 @@
 
     fun finish_tex path (a, {tex_source, ...}: theory_info) = write_tex tex_source a path;
     fun finish_html (a, {html, ...}: theory_info) =
-      Buffer.write (Path.append html_prefix (html_path a)) (Buffer.add HTML.end_document html);
+      File.write_buffer (Path.append html_prefix (html_path a)) (Buffer.add HTML.end_document html);
 
     val sorted_graph = sorted_index graph;
     val opt_graphs =
@@ -395,7 +395,7 @@
   in
     if info then
      (File.mkdir (Path.append html_prefix session_path);
-      Buffer.write (Path.append html_prefix pre_index_path) (index_buffer html_index);
+      File.write_buffer (Path.append html_prefix pre_index_path) (index_buffer html_index);
       File.write (Path.append html_prefix session_entries_path) "";
       create_index html_prefix;
       if length path > 1 then update_index parent_html_prefix name else ();