1.1 --- a/src/Pure/General/buffer.ML	Wed Aug 27 20:36:25 2008 +0200
     1.2 +++ b/src/Pure/General/buffer.ML	Wed Aug 27 20:36:26 2008 +0200
     1.3 @@ -14,7 +14,6 @@
     1.4    val markup: Markup.T -> (T -> T) -> T -> T
     1.5    val content: T -> string
     1.6    val output: T -> TextIO.outstream -> unit
     1.7 -  val write: Path.T -> T -> unit
     1.8  end;
     1.9  
    1.10  structure Buffer: BUFFER =
    1.11 @@ -62,6 +61,4 @@
    1.12        | rev_output (Substring (s, buf)) = (TextIO.outputSubstr (stream, s); rev_output buf);
    1.13    in rev_output (rev_buffer buffer empty) end;
    1.14  
    1.15 -fun write path buf = File.open_output (output buf) path;
    1.16 -
    1.17  end;

     2.1 --- a/src/Pure/Thy/present.ML	Wed Aug 27 20:36:25 2008 +0200
     2.2 +++ b/src/Pure/Thy/present.ML	Wed Aug 27 20:36:26 2008 +0200
     2.3 @@ -359,7 +359,7 @@
     2.4  fun index_buffer index = Buffer.add (implode (sorted_index index)) Buffer.empty;
     2.5  
     2.6  fun write_tex src name path =
     2.7 -  Buffer.write (Path.append path (tex_path name)) src;
     2.8 +  File.write_buffer (Path.append path (tex_path name)) src;
     2.9  
    2.10  fun write_tex_index tex_index path =
    2.11    write_tex (index_buffer tex_index |> Buffer.add Latex.tex_trailer) doc_indexN path;
    2.12 @@ -375,7 +375,7 @@
    2.13  
    2.14      fun finish_tex path (a, {tex_source, ...}: theory_info) = write_tex tex_source a path;
    2.15      fun finish_html (a, {html, ...}: theory_info) =
    2.16 -      Buffer.write (Path.append html_prefix (html_path a)) (Buffer.add HTML.end_document html);
    2.17 +      File.write_buffer (Path.append html_prefix (html_path a)) (Buffer.add HTML.end_document html);
    2.18  
    2.19      val sorted_graph = sorted_index graph;
    2.20      val opt_graphs =
    2.21 @@ -395,7 +395,7 @@
    2.22    in
    2.23      if info then
    2.24       (File.mkdir (Path.append html_prefix session_path);
    2.25 -      Buffer.write (Path.append html_prefix pre_index_path) (index_buffer html_index);
    2.26 +      File.write_buffer (Path.append html_prefix pre_index_path) (index_buffer html_index);
    2.27        File.write (Path.append html_prefix session_entries_path) "";
    2.28        create_index html_prefix;
    2.29        if length path > 1 then update_index parent_html_prefix name else ();