removed copy, copy_all (superceded by File.copy, File.copy_dir);
File.shell_path, File.isatool;
tuned;
--- 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)))