1.1 --- a/src/Pure/Thy/present.ML Sun Jun 05 11:31:25 2005 +0200
1.2 +++ b/src/Pure/Thy/present.ML Sun Jun 05 11:31:26 2005 +0200
1.3 @@ -115,8 +115,8 @@
1.4 {name = name, ID = ID_of session name, dir = sess_name,
1.5 path =
1.6 if null session then "" else
1.7 - if isSome remote_path andalso not is_local then
1.8 - Url.pack (Url.append (valOf remote_path) (Url.File
1.9 + if is_some remote_path andalso not is_local then
1.10 + Url.pack (Url.append (the remote_path) (Url.File
1.11 (Path.append (Path.make session) (html_path name))))
1.12 else Path.pack (Path.append (mk_rel_path curr_sess session) (html_path name)),
1.13 unfold = false,
1.14 @@ -266,16 +266,6 @@
1.15
1.16 (* init session *)
1.17
1.18 -fun copy_files path1 path2 =
1.19 - (File.mkdir path2;
1.20 - system ("cp " ^ File.sysify_path path1 ^ " " ^ File.sysify_path path2)); (*FIXME: quote!?*)
1.21 -
1.22 -fun copy_all path1 path2 =
1.23 - (File.mkdir path2;
1.24 - system ("cp -r " ^ File.quote_sysify_path path1 ^ "/. " ^
1.25 - File.quote_sysify_path path2));
1.26 -
1.27 -
1.28 fun name_of_session elems = space_implode "/" ("Isabelle" :: elems);
1.29
1.30 fun init build info doc doc_graph path name doc_prefix2 (remote_path, first_time) verbose =
1.31 @@ -296,7 +286,7 @@
1.32
1.33 val parent_index_path = Path.append Path.parent index_path;
1.34 val index_up_lnk = if first_time then
1.35 - Url.append (valOf remote_path) (Url.File (Path.append sess_prefix parent_index_path))
1.36 + Url.append (the remote_path) (Url.File (Path.append sess_prefix parent_index_path))
1.37 else Url.File parent_index_path;
1.38 val readme =
1.39 if File.exists readme_html_path then SOME readme_html_path
1.40 @@ -326,7 +316,7 @@
1.41 fun isatool_document verbose doc_format path =
1.42 let
1.43 val s = "\"$ISATOOL\" document -c -o '" ^ doc_format ^ "' " ^
1.44 - File.quote_sysify_path path ^ " 2>&1" ^ (if verbose then "" else " >/dev/null");
1.45 + File.shell_path path ^ " 2>&1" ^ (if verbose then "" else " >/dev/null");
1.46 val doc_path = Path.ext doc_format path;
1.47 in
1.48 if verbose then writeln s else ();
1.49 @@ -340,11 +330,10 @@
1.50 val pdfpath = File.tmp_path graph_pdf_path;
1.51 val epspath = File.tmp_path graph_eps_path;
1.52 val gpath = File.tmp_path graph_path;
1.53 - val s = "\"$ISATOOL\" browser -o " ^ File.quote_sysify_path pdfpath ^ " " ^
1.54 - File.quote_sysify_path gpath;
1.55 + val s = "browser -o " ^ File.shell_path pdfpath ^ " " ^ File.shell_path gpath;
1.56 in
1.57 write_graph graph gpath;
1.58 - if system s <> 0 orelse not (File.exists epspath) orelse not (File.exists pdfpath)
1.59 + if File.isatool s <> 0 orelse not (File.exists epspath) orelse not (File.exists pdfpath)
1.60 then error "Failed to prepare dependency graph"
1.61 else
1.62 let val pdf = File.read pdfpath and eps = File.read epspath
1.63 @@ -363,13 +352,16 @@
1.64 Buffer.write (Path.append html_prefix (html_path a)) (Buffer.add HTML.end_theory html);
1.65
1.66 val opt_graphs =
1.67 - if doc_graph andalso (isSome doc_prefix1 orelse isSome doc_prefix2) then
1.68 + if doc_graph andalso (is_some doc_prefix1 orelse is_some doc_prefix2) then
1.69 SOME (isatool_browser graph)
1.70 else NONE;
1.71
1.72 fun prepare_sources path =
1.73 - (copy_all doc_path path;
1.74 - copy_files (Path.unpack "~~/lib/texinputs/*.sty") path;
1.75 + (File.mkdir path;
1.76 + File.copy_dir doc_path path;
1.77 + File.copy (Path.unpack "~~/lib/texinputs/isabelle.sty") path;
1.78 + File.copy (Path.unpack "~~/lib/texinputs/isabellesym.sty") path;
1.79 + File.copy (Path.unpack "~~/lib/texinputs/pdfsetup.sty") path;
1.80 (case opt_graphs of NONE => () | SOME (pdf, eps) =>
1.81 (File.write (Path.append path graph_pdf_path) pdf;
1.82 File.write (Path.append path graph_eps_path) eps));
1.83 @@ -382,12 +374,12 @@
1.84 File.write (Path.append html_prefix session_entries_path) "";
1.85 create_index html_prefix;
1.86 if length path > 1 then update_index parent_html_prefix name else ();
1.87 - (case readme of NONE => () | SOME path => File.copy path (Path.append html_prefix path));
1.88 + (case readme of NONE => () | SOME path => File.copy path html_prefix);
1.89 write_graph graph (Path.append html_prefix graph_path);
1.90 - copy_files (Path.unpack "~~/lib/browser/GraphBrowser.jar") html_prefix;
1.91 + File.copy (Path.unpack "~~/lib/browser/GraphBrowser.jar") html_prefix;
1.92 List.app (fn (a, txt) => File.write (Path.append html_prefix (Path.basic a)) txt)
1.93 (HTML.applet_pages name (Url.File index_path, name));
1.94 - copy_files (Path.unpack "~~/lib/html/isabelle.css") html_prefix;
1.95 + File.copy (Path.unpack "~~/lib/html/isabelle.css") html_prefix;
1.96 List.app finish_html thys;
1.97 List.app (uncurry File.write) files;
1.98 conditional verbose (fn () =>
1.99 @@ -426,8 +418,8 @@
1.100 fun parent_link remote_path curr_session name =
1.101 let val {name = _, session, is_local} = get_info (ThyInfo.theory name)
1.102 in (if null session then NONE else
1.103 - SOME (if isSome remote_path andalso not is_local then
1.104 - Url.append (valOf remote_path) (Url.File
1.105 + SOME (if is_some remote_path andalso not is_local then
1.106 + Url.append (the remote_path) (Url.File
1.107 (Path.append (Path.make session) (html_path name)))
1.108 else Url.File (Path.append (mk_rel_path curr_session session)
1.109 (html_path name))), name)
1.110 @@ -439,7 +431,7 @@
1.111 val parents = map (parent_link remote_path path) raw_parents;
1.112 val ml_path = ThyLoad.ml_path name;
1.113 val files = map (apsnd SOME) orig_files @
1.114 - (if isSome (ThyLoad.check_file optpath ml_path) then [(ml_path, NONE)] else []);
1.115 + (if is_some (ThyLoad.check_file optpath ml_path) then [(ml_path, NONE)] else []);
1.116
1.117 fun prep_file (raw_path, loadit) =
1.118 (case ThyLoad.check_file optpath raw_path of
1.119 @@ -473,7 +465,7 @@
1.120 add_graph_entry entry;
1.121 add_html_index (HTML.theory_entry (Url.File (html_path name), name));
1.122 add_tex_index (Latex.theory_entry name);
1.123 - BrowserInfoData.put {name = sess_name, session = path, is_local = isSome remote_path} thy
1.124 + BrowserInfoData.put {name = sess_name, session = path, is_local = is_some remote_path} thy
1.125 end);
1.126
1.127
1.128 @@ -513,10 +505,8 @@
1.129 val _ = File.mkdir doc_path;
1.130 val root_path = Path.append doc_path (Path.basic "root.tex");
1.131 val _ = File.copy (Path.unpack "~~/lib/texinputs/draft.tex") root_path;
1.132 - val _ = File.system_command
1.133 - ("\"$ISATOOL\" latex -o sty " ^ File.quote_sysify_path root_path);
1.134 - val _ = File.system_command
1.135 - ("\"$ISATOOL\" latex -o syms " ^ File.quote_sysify_path root_path);
1.136 + val _ = File.isatool ("latex -o sty " ^ File.shell_path root_path);
1.137 + val _ = File.isatool ("latex -o syms " ^ File.shell_path root_path);
1.138
1.139 fun known name =
1.140 let val ss = split_lines (File.read (Path.append doc_path (Path.basic name)))