# HG changeset patch
# User wenzelm
# Date 870869549 -7200
# Node ID 41a49c67190186386a781d976a1fdbe71aa1c57b
# Parent  3d0d5f2a2e334f5902e3be13a3db06cce1a9bf6f
tuned copy_file;

diff -r 3d0d5f2a2e33 -r 41a49c671901 src/Pure/Thy/browser_info.ML
--- a/src/Pure/Thy/browser_info.ML	Wed Aug 06 14:12:03 1997 +0200
+++ b/src/Pure/Thy/browser_info.ML	Wed Aug 06 14:12:29 1997 +0200
@@ -53,7 +53,7 @@
 
 (*create directory
   FIXME: move to library?*)
-fun mkdir path = (execute ("mkdir -p " ^ path) ; ());
+fun mkdir path = (execute ("mkdir -p " ^ path); ());
 
 
 (*Path of Isabelle's main (source) directory
@@ -62,6 +62,14 @@
   "/" ^ space_implode "/" (rev (tl (tl (rev (space_explode "/" (OS.FileSys.getDir ())))))));
 
 
+(* copy contents of file *)  (* FIXME: move to library?*)
+
+fun copy_file infile outfile =
+  if not (file_exists infile) then ()
+  else write_file outfile (read_file infile);
+
+
+
 (******************** HTML generation functions *************************)
 
 (*Set location of graphics for HTML files*)
@@ -437,17 +445,6 @@
            pure_subchart := Some (html_path cwd)
         end;
 
-      (*Copy files
-        FIXME: move to library?*)
-      fun copy_file infile outfile = if not (file_exists infile) then () else
-        let val is = TextIO.openIn infile;
-            val inp = TextIO.inputAll is;
-            val _ = TextIO.closeIn is;
-            val os = TextIO.openOut outfile;
-            val _ = TextIO.output (os, inp);
-            val _ = TextIO.closeOut os
-        in () end
-
   in make_html := true;
      (*Make sure that base_path contains the physical path and no
        symbolic links*)