1.1 --- a/src/Pure/Thy/present.ML	Fri Feb 15 20:42:00 2002 +0100
     1.2 +++ b/src/Pure/Thy/present.ML	Fri Feb 15 20:43:09 2002 +0100
     1.3 @@ -264,14 +264,18 @@
     1.4  
     1.5  (* init session *)
     1.6  
     1.7 +fun copy_files path1 path2 =
     1.8 + (File.mkdir path2;
     1.9 +  system ("cp " ^ File.sysify_path path1 ^ " " ^ File.sysify_path path2));  (*FIXME: quote!?*)
    1.10 +
    1.11 +fun copy_all path1 path2 =
    1.12 + (File.mkdir path2;
    1.13 +  system ("cp -r " ^ File.quote_sysify_path path1 ^ " " ^
    1.14 +    File.quote_sysify_path (Path.append path2 Path.parent)));
    1.15 +
    1.16 +
    1.17  fun name_of_session elems = space_implode "/" ("Isabelle" :: elems);
    1.18  
    1.19 -fun copy_files path1 path2 =
    1.20 -  (File.mkdir path2;
    1.21 -   File.system_command  (*FIXME: quote paths!?*)
    1.22 -     ("cp " ^ File.sysify_path path1 ^ " " ^ File.sysify_path path2));
    1.23 -
    1.24 -
    1.25  fun init build info doc doc_graph path name doc_prefix2 (remote_path, first_time) verbose =
    1.26    if not build andalso not info andalso doc = "" andalso is_none doc_prefix2 then
    1.27      (browser_info := empty_browser_info; session_info := None)
    1.28 @@ -354,8 +358,9 @@
    1.29          Some (isatool_browser graph)
    1.30        else None;
    1.31  
    1.32 -    fun doc_common path =
    1.33 -      (copy_files (Path.unpack "~~/lib/texinputs/*.sty") path;
    1.34 +    fun prepare_sources path =
    1.35 +     (copy_all doc_path path;
    1.36 +      copy_files (Path.unpack "~~/lib/texinputs/*.sty") path;
    1.37        (case opt_graphs of None => () | Some (pdf, eps) =>
    1.38          (File.write (Path.append path graph_pdf_path) pdf;
    1.39            File.write (Path.append path graph_eps_path) eps));
    1.40 @@ -381,19 +386,16 @@
    1.41        conditional verbose (fn () =>
    1.42          std_error ("Browser info at " ^ show_path html_prefix ^ "\n"))));
    1.43  
    1.44 +    (case doc_prefix2 of None => () | Some path =>
    1.45 +     (prepare_sources path;
    1.46 +      conditional verbose (fn () => std_error ("Document sources at " ^ show_path path ^ "\n"))));
    1.47 +
    1.48      (case doc_prefix1 of None => () | Some path =>
    1.49 -     (File.mkdir html_prefix;
    1.50 -      File.copy_all doc_path html_prefix;
    1.51 -      doc_common path;
    1.52 +     (prepare_sources path;
    1.53        isatool_document doc_format path;
    1.54        conditional verbose (fn () =>
    1.55          std_error ("Document at " ^ show_path (Path.ext doc_format path) ^ "\n"))));
    1.56  
    1.57 -    (case doc_prefix2 of None => () | Some path =>
    1.58 -     (File.mkdir path;
    1.59 -      doc_common path;
    1.60 -      conditional verbose (fn () => std_error ("Document sources at " ^ show_path path ^ "\n"))));
    1.61 -
    1.62      browser_info := empty_browser_info;
    1.63      session_info := None
    1.64    end);