src/Pure/proof_general.ML

 end;
 
 
 (* prepare theory context *)
 
-val thy_name = Path.pack o #1 o Path.split_ext o Path.base o Path.unpack;
+val thy_name = Path.implode o #1 o Path.split_ext o Path.base o Path.explode;
 
 (* FIXME general treatment of tracing*)
 val update_thy_only = setmp MetaSimplifier.trace_simp false ThyInfo.update_thy_only;
 
 fun dynamic_context () =
   (case Context.get_context () of
     SOME thy => "  Using current (dynamic!) one: " ^ quote (Context.theory_name thy)
   | NONE => "");
 
 fun try_update_thy_only file =
-  ThyLoad.cond_add_path (Path.dir (Path.unpack file)) (fn () =>
+  ThyLoad.cond_add_path (Path.dir (Path.explode file)) (fn () =>
     let val name = thy_name file in
       if is_some (ThyLoad.check_file NONE (ThyLoad.thy_path name))
       then update_thy_only name
       else warning ("Unkown theory context of ML file." ^ dynamic_context ())
     end) ();

   let val name = thy_name file in
     if Toplevel.is_toplevel state andalso ThyInfo.known_thy name then
      (ThyInfo.touch_child_thys name;
       ThyInfo.pretend_use_thy_only name handle ERROR msg =>
        (warning msg; warning ("Failed to register theory: " ^ quote name);
-        tell_file_retracted (Path.base (Path.unpack file))))
+        tell_file_retracted (Path.base (Path.explode file))))
     else raise Toplevel.UNDEF
   end;
 
 fun vacuous_inform_file_processed file state =
  (warning ("No theory " ^ quote (thy_name file));
-  tell_file_retracted (Path.base (Path.unpack file)));
+  tell_file_retracted (Path.base (Path.explode file)));
 
 
 (* restart top-level loop (keeps most state information) *)
 
 local

     fun config_file()  = orenv "ISABELLE_PGIPCONFIG" "~~/lib/ProofGeneral/pgip_isar.xml"
     fun isabelle_www() = orenv "ISABELLE_HOMEPAGE" "http://isabelle.in.tum.de/"
 in
 fun send_pgip_config () =
     let
-        val path = Path.unpack (config_file())
+        val path = Path.explode (config_file())
         val exists = File.exists path
         val proverinfo =
             XML.element "proverinfo"
               [("name",     	 "Isabelle"), 
 	       ("version",  	 version),

 
 (* Reveal some information about prover state *)
 fun send_informguise (openfile, opentheory, openproofpos) =
     let val guisefile =
             case openfile of SOME f => [XML.element "guisefile"
-                                                    [("url",Url.pack (Url.File (Path.unpack f)))] []]
+                                                    [("url",Url.implode (Url.File (Path.explode f)))] []]
                            | _ => []
         val guisetheory =
             case opentheory of SOME t => [XML.element "guisetheory" [("thyname", t)] []]
                              | _ => []
         val guiseproof =

 
 (* load an arbitrary file (must be .thy or .ML) *)
 
 fun use_thy_or_ml_file file =
     let
-        val (path,extn) = Path.split_ext (Path.unpack file)
+        val (path,extn) = Path.split_ext (Path.explode file)
     in
         case extn of
-            "" => isarcmd ("use_thy " ^ (quote (Path.pack path)))
-          | "thy" => isarcmd ("use_thy " ^ (quote (Path.pack path)))
+            "" => isarcmd ("use_thy " ^ (quote (Path.implode path)))
+          | "thy" => isarcmd ("use_thy " ^ (quote (Path.implode path)))
           | "ML" => isarcmd ("use " ^ quote file)
           | other => error ("Don't know how to read a file with extension " ^ other)
     end
 
 

   val objtype_attro = xmlattro "objtype"
   val objtype_attr = xmlattr "objtype"
   val name_attr = xmlattr "name"
 
   fun localfile_of_url url = (* only handle file:/// or file://localhost/ *)
-      case Url.unpack url of
+      case Url.explode url of
           (Url.File path) => File.platform_path path
         | _ => error ("Cannot access non-local URL " ^ url)
 
   val fileurl_of = localfile_of_url o (xmlattr "url")
 

 
 in
 
 fun write_keywords s =
  (init_outer_syntax ();
-  File.write (Path.unpack ("isar-keywords" ^ (if s = "" then "" else "-" ^ s) ^".el"))
+  File.write (Path.explode ("isar-keywords" ^ (if s = "" then "" else "-" ^ s) ^".el"))
     (make_elisp_syntax (OuterSyntax.dest_keywords (), OuterSyntax.dest_parsers ())));
 
 end;