--- 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*)