# HG changeset patch
# User wenzelm
# Date 1013802189 -3600
# Node ID d9dd528ecea6a2aa68bbe8eb150baa0e1a581aaa
# Parent  61f485eb0dc2521608e72e414364966c1fe83a9d
clarified copy_all;
generated second copy of document sources first (more robust);

diff -r 61f485eb0dc2 -r d9dd528ecea6 src/Pure/Thy/present.ML
--- a/src/Pure/Thy/present.ML	Fri Feb 15 20:42:00 2002 +0100
+++ b/src/Pure/Thy/present.ML	Fri Feb 15 20:43:09 2002 +0100
@@ -264,14 +264,18 @@
 
 (* init session *)
 
-fun name_of_session elems = space_implode "/" ("Isabelle" :: elems);
+fun copy_files path1 path2 =
+ (File.mkdir path2;
+  system ("cp " ^ File.sysify_path path1 ^ " " ^ File.sysify_path path2));  (*FIXME: quote!?*)
 
-fun copy_files path1 path2 =
-  (File.mkdir path2;
-   File.system_command  (*FIXME: quote paths!?*)
-     ("cp " ^ File.sysify_path path1 ^ " " ^ File.sysify_path path2));
+fun copy_all path1 path2 =
+ (File.mkdir path2;
+  system ("cp -r " ^ File.quote_sysify_path path1 ^ " " ^
+    File.quote_sysify_path (Path.append path2 Path.parent)));
 
 
+fun name_of_session elems = space_implode "/" ("Isabelle" :: elems);
+
 fun init build info doc doc_graph path name doc_prefix2 (remote_path, first_time) verbose =
   if not build andalso not info andalso doc = "" andalso is_none doc_prefix2 then
     (browser_info := empty_browser_info; session_info := None)
@@ -354,8 +358,9 @@
         Some (isatool_browser graph)
       else None;
 
-    fun doc_common path =
-      (copy_files (Path.unpack "~~/lib/texinputs/*.sty") path;
+    fun prepare_sources path =
+     (copy_all doc_path path;
+      copy_files (Path.unpack "~~/lib/texinputs/*.sty") path;
       (case opt_graphs of None => () | Some (pdf, eps) =>
         (File.write (Path.append path graph_pdf_path) pdf;
           File.write (Path.append path graph_eps_path) eps));
@@ -381,19 +386,16 @@
       conditional verbose (fn () =>
         std_error ("Browser info at " ^ show_path html_prefix ^ "\n"))));
 
+    (case doc_prefix2 of None => () | Some path =>
+     (prepare_sources path;
+      conditional verbose (fn () => std_error ("Document sources at " ^ show_path path ^ "\n"))));
+
     (case doc_prefix1 of None => () | Some path =>
-     (File.mkdir html_prefix;
-      File.copy_all doc_path html_prefix;
-      doc_common path;
+     (prepare_sources path;
       isatool_document doc_format path;
       conditional verbose (fn () =>
         std_error ("Document at " ^ show_path (Path.ext doc_format path) ^ "\n"))));
 
-    (case doc_prefix2 of None => () | Some path =>
-     (File.mkdir path;
-      doc_common path;
-      conditional verbose (fn () => std_error ("Document sources at " ^ show_path path ^ "\n"))));
-
     browser_info := empty_browser_info;
     session_info := None
   end);