src/Pure/Thy/present.ML

 
 fun sorted_index index = map snd (sort (int_ord o pairself fst) (rev index));
 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;
 
 

     val thys = Symtab.dest theories;
     val parent_html_prefix = Path.append html_prefix Path.parent;
 
     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 =
       if doc_graph andalso (is_some doc_prefix1 orelse is_some doc_prefix2) then
         SOME (isatool_browser sorted_graph)

       write_tex_index tex_index path;
       List.app (finish_tex path) thys);
   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 ();
       (case readme of NONE => () | SOME path => File.copy path html_prefix);
       write_graph sorted_graph (Path.append html_prefix graph_path);