src/Pure/Thy/present.ML

--- a/src/Pure/Thy/present.ML	Thu Dec 14 22:19:39 2006 +0100
+++ b/src/Pure/Thy/present.ML	Fri Dec 15 00:08:06 2006 +0100
@@ -60,15 +60,15 @@
 val graph_eps_path = Path.basic "session_graph.eps";
 
 val session_path = Path.basic ".session";
-val session_entries_path = Path.unpack ".session/entries";
-val pre_index_path = Path.unpack ".session/pre-index";
+val session_entries_path = Path.explode ".session/entries";
+val pre_index_path = Path.explode ".session/pre-index";
 
 fun mk_rel_path [] ys = Path.make ys
   | mk_rel_path xs [] = Path.appends (replicate (length xs) Path.parent)
   | mk_rel_path (ps as x :: xs) (qs as y :: ys) = if x = y then mk_rel_path xs ys else
       Path.appends (replicate (length ps) Path.parent @ [Path.make qs]);
 
-fun show_path path = Path.pack (Path.append (File.pwd ()) path);
+fun show_path path = Path.implode (Path.append (File.pwd ()) path);
 
 
 
@@ -108,7 +108,7 @@
 fun display_graph gr =
   let
     val _ = writeln "Generating graph ...";
-    val path = File.tmp_path (Path.unpack "tmp.graph");
+    val path = File.tmp_path (Path.explode "tmp.graph");
     val _ = write_graph gr path;
     val _ = File.isatool ("browser -c " ^ File.shell_path path ^ " &");
   in () end;
@@ -126,9 +126,9 @@
     path =
       if null session then "" else
       if is_some remote_path andalso not is_local then
-        Url.pack (Url.append (the remote_path) (Url.File
+        Url.implode (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)),
+      else Path.implode (Path.append (mk_rel_path curr_sess session) (html_path name)),
     unfold = false,
     parents =
       map (fn s => ID_of (#session (get_info (ThyInfo.theory s))) s) (ThyInfo.get_preds name)}
@@ -271,7 +271,7 @@
 
 fun update_index dir name =
   (case try get_entries dir of
-    NONE => warning ("Browser info: cannot access session index of " ^ quote (Path.pack dir))
+    NONE => warning ("Browser info: cannot access session index of " ^ quote (Path.implode dir))
   | SOME es => (put_entries ((remove (op =) name es) @ [name]) dir; create_index dir));
 
 
@@ -323,7 +323,7 @@
         (case readme of NONE => [] | SOME p => [(Url.File p, "README")]) @
         map (fn (name, _) => (Url.File (Path.ext doc (Path.basic name)), name)) documents;
       val index_text = HTML.begin_index (index_up_lnk, parent_name)
-        (Url.File index_path, session_name) docs (Url.unpack "medium.html");
+        (Url.File index_path, session_name) docs (Url.explode "medium.html");
     in
       session_info := SOME (make_session_info (name, parent_name, session_name, path, html_prefix,
       info, doc, doc_graph, documents, doc_prefix1, doc_prefix2, remote_path, verbose, readme));
@@ -407,10 +407,10 @@
       if length path > 1 then update_index parent_html_prefix name else ();
       (case readme of NONE => () | SOME path => File.copy path html_prefix);
       write_graph graph (Path.append html_prefix graph_path);
-      File.copy (Path.unpack "~~/lib/browser/GraphBrowser.jar") html_prefix;
+      File.copy (Path.explode "~~/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));
-      File.copy (Path.unpack "~~/lib/html/isabelle.css") html_prefix;
+      File.copy (Path.explode "~~/lib/html/isabelle.css") html_prefix;
       List.app finish_html thys;
       List.app (uncurry File.write) files;
       conditional verbose (fn () =>
@@ -474,7 +474,7 @@
               HTML.ml_file (Url.File base) (File.read path));
             (SOME (Url.File base_html), Url.File raw_path, loadit)
           end
-      | NONE => (warning ("Browser info: expected to find ML file" ^ quote (Path.pack raw_path));
+      | NONE => (warning ("Browser info: expected to find ML file" ^ quote (Path.implode raw_path));
           (NONE, Url.File raw_path, loadit)));
 
     val files_html = map prep_file files;
@@ -487,7 +487,7 @@
 
     val entry =
      {name = name, ID = ID_of path name, dir = sess_name, unfold = true,
-      path = Path.pack (html_path name),
+      path = Path.implode (html_path name),
       parents = map (fn s => ID_of (#session (get_info (ThyInfo.theory s))) s) raw_parents};
 
   in
@@ -523,11 +523,11 @@
       let
         val base = Path.base path;
         val name =
-          (case Path.pack (#1 (Path.split_ext base)) of "" => gensym "DUMMY" | s => s);
+          (case Path.implode (#1 (Path.split_ext base)) of "" => gensym "DUMMY" | s => s);
       in
         if File.exists path then
           (Buffer.add (Latex.theory_entry name) tex_index, (name, base, File.read path))
-        else error ("Bad file: " ^ quote (Path.pack path))
+        else error ("Bad file: " ^ quote (Path.implode path))
       end;
     val (tex_index, srcs) = foldl_map prep_draft (Buffer.empty, src_paths);
 
@@ -535,7 +535,7 @@
     val result_path = Path.append doc_path Path.parent;
     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.copy (Path.explode "~~/lib/texinputs/draft.tex") root_path;
     val _ = File.isatool ("latex -o sty " ^ File.shell_path root_path);
     val _ = File.isatool ("latex -o syms " ^ File.shell_path root_path);
 
@@ -547,7 +547,7 @@
 
     val _ = srcs |> List.app (fn (name, base, txt) =>
       Symbol.explode txt
-      |> Latex.symbol_source (known_syms, known_ctrls) (Path.pack base)
+      |> Latex.symbol_source (known_syms, known_ctrls) (Path.implode base)
       |> File.write (Path.append doc_path (tex_path name)));
     val _ = write_tex_index tex_index doc_path;
   in isatool_document false doc_format documentN "" doc_path result_path end;