# HG changeset patch # User wenzelm # Date 1117963886 -7200 # Node ID 0609fb8df4a7304995394955774bd91d5ecc12d1 # Parent bd1b38f57fc774a7d1980007ae34a3387c33f973 removed copy, copy_all (superceded by File.copy, File.copy_dir); File.shell_path, File.isatool; tuned; diff -r bd1b38f57fc7 -r 0609fb8df4a7 src/Pure/Thy/present.ML --- a/src/Pure/Thy/present.ML Sun Jun 05 11:31:25 2005 +0200 +++ b/src/Pure/Thy/present.ML Sun Jun 05 11:31:26 2005 +0200 @@ -115,8 +115,8 @@ {name = name, ID = ID_of session name, dir = sess_name, path = if null session then "" else - if isSome remote_path andalso not is_local then - Url.pack (Url.append (valOf remote_path) (Url.File + if is_some remote_path andalso not is_local then + Url.pack (Url.append (the remote_path) (Url.File (Path.append (Path.make session) (html_path name)))) else Path.pack (Path.append (mk_rel_path curr_sess session) (html_path name)), unfold = false, @@ -266,16 +266,6 @@ (* init session *) -fun copy_files path1 path2 = - (File.mkdir path2; - system ("cp " ^ File.sysify_path path1 ^ " " ^ File.sysify_path path2)); (*FIXME: quote!?*) - -fun copy_all path1 path2 = - (File.mkdir path2; - system ("cp -r " ^ File.quote_sysify_path path1 ^ "/. " ^ - File.quote_sysify_path path2)); - - 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 = @@ -296,7 +286,7 @@ val parent_index_path = Path.append Path.parent index_path; val index_up_lnk = if first_time then - Url.append (valOf remote_path) (Url.File (Path.append sess_prefix parent_index_path)) + Url.append (the remote_path) (Url.File (Path.append sess_prefix parent_index_path)) else Url.File parent_index_path; val readme = if File.exists readme_html_path then SOME readme_html_path @@ -326,7 +316,7 @@ fun isatool_document verbose doc_format path = let val s = "\"$ISATOOL\" document -c -o '" ^ doc_format ^ "' " ^ - File.quote_sysify_path path ^ " 2>&1" ^ (if verbose then "" else " >/dev/null"); + File.shell_path path ^ " 2>&1" ^ (if verbose then "" else " >/dev/null"); val doc_path = Path.ext doc_format path; in if verbose then writeln s else (); @@ -340,11 +330,10 @@ val pdfpath = File.tmp_path graph_pdf_path; val epspath = File.tmp_path graph_eps_path; val gpath = File.tmp_path graph_path; - val s = "\"$ISATOOL\" browser -o " ^ File.quote_sysify_path pdfpath ^ " " ^ - File.quote_sysify_path gpath; + val s = "browser -o " ^ File.shell_path pdfpath ^ " " ^ File.shell_path gpath; in write_graph graph gpath; - if system s <> 0 orelse not (File.exists epspath) orelse not (File.exists pdfpath) + if File.isatool s <> 0 orelse not (File.exists epspath) orelse not (File.exists pdfpath) then error "Failed to prepare dependency graph" else let val pdf = File.read pdfpath and eps = File.read epspath @@ -363,13 +352,16 @@ Buffer.write (Path.append html_prefix (html_path a)) (Buffer.add HTML.end_theory html); val opt_graphs = - if doc_graph andalso (isSome doc_prefix1 orelse isSome doc_prefix2) then + if doc_graph andalso (is_some doc_prefix1 orelse is_some doc_prefix2) then SOME (isatool_browser graph) else NONE; fun prepare_sources path = - (copy_all doc_path path; - copy_files (Path.unpack "~~/lib/texinputs/*.sty") path; + (File.mkdir path; + File.copy_dir doc_path path; + File.copy (Path.unpack "~~/lib/texinputs/isabelle.sty") path; + File.copy (Path.unpack "~~/lib/texinputs/isabellesym.sty") path; + File.copy (Path.unpack "~~/lib/texinputs/pdfsetup.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)); @@ -382,12 +374,12 @@ 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 (Path.append html_prefix path)); + (case readme of NONE => () | SOME path => File.copy path html_prefix); write_graph graph (Path.append html_prefix graph_path); - copy_files (Path.unpack "~~/lib/browser/GraphBrowser.jar") html_prefix; + File.copy (Path.unpack "~~/lib/browser/GraphBrowser.jar") html_prefix; List.app (fn (a, txt) => File.write (Path.append html_prefix (Path.basic a)) txt) (HTML.applet_pages name (Url.File index_path, name)); - copy_files (Path.unpack "~~/lib/html/isabelle.css") html_prefix; + File.copy (Path.unpack "~~/lib/html/isabelle.css") html_prefix; List.app finish_html thys; List.app (uncurry File.write) files; conditional verbose (fn () => @@ -426,8 +418,8 @@ fun parent_link remote_path curr_session name = let val {name = _, session, is_local} = get_info (ThyInfo.theory name) in (if null session then NONE else - SOME (if isSome remote_path andalso not is_local then - Url.append (valOf remote_path) (Url.File + SOME (if is_some remote_path andalso not is_local then + Url.append (the remote_path) (Url.File (Path.append (Path.make session) (html_path name))) else Url.File (Path.append (mk_rel_path curr_session session) (html_path name))), name) @@ -439,7 +431,7 @@ val parents = map (parent_link remote_path path) raw_parents; val ml_path = ThyLoad.ml_path name; val files = map (apsnd SOME) orig_files @ - (if isSome (ThyLoad.check_file optpath ml_path) then [(ml_path, NONE)] else []); + (if is_some (ThyLoad.check_file optpath ml_path) then [(ml_path, NONE)] else []); fun prep_file (raw_path, loadit) = (case ThyLoad.check_file optpath raw_path of @@ -473,7 +465,7 @@ add_graph_entry entry; add_html_index (HTML.theory_entry (Url.File (html_path name), name)); add_tex_index (Latex.theory_entry name); - BrowserInfoData.put {name = sess_name, session = path, is_local = isSome remote_path} thy + BrowserInfoData.put {name = sess_name, session = path, is_local = is_some remote_path} thy end); @@ -513,10 +505,8 @@ val _ = File.mkdir doc_path; val root_path = Path.append doc_path (Path.basic "root.tex"); val _ = File.copy (Path.unpack "~~/lib/texinputs/draft.tex") root_path; - val _ = File.system_command - ("\"$ISATOOL\" latex -o sty " ^ File.quote_sysify_path root_path); - val _ = File.system_command - ("\"$ISATOOL\" latex -o syms " ^ File.quote_sysify_path root_path); + val _ = File.isatool ("latex -o sty " ^ File.shell_path root_path); + val _ = File.isatool ("latex -o syms " ^ File.shell_path root_path); fun known name = let val ss = split_lines (File.read (Path.append doc_path (Path.basic name)))