diff -r f9d085c2625c -r 05f57309170c src/Pure/General/url.ML
--- a/src/Pure/General/url.ML	Thu Dec 14 22:19:39 2006 +0100
+++ b/src/Pure/General/url.ML	Fri Dec 15 00:08:06 2006 +0100
@@ -13,8 +13,8 @@
     Http of string * Path.T |
     Ftp of string * Path.T
   val append: T -> T -> T
-  val pack: T -> string
-  val unpack: string -> T
+  val implode: T -> string
+  val explode: string -> T
 end;
 
 structure Url: URL =
@@ -38,26 +38,26 @@
   | append _ url = url;
 
 
-(* pack *)
+(* implode *)
 
-fun pack_path p = if Path.is_current p then "" else Path.pack p;
+fun implode_path p = if Path.is_current p then "" else Path.implode p;
 
-fun pack (File p) = pack_path p
-  | pack (RemoteFile (h, p)) = "file://" ^ h ^ pack_path p
-  | pack (Http (h, p)) = "http://" ^ h ^ pack_path p
-  | pack (Ftp (h, p)) = "ftp://" ^ h ^ pack_path p;
+fun implode_url (File p) = implode_path p
+  | implode_url (RemoteFile (h, p)) = "file://" ^ h ^ implode_path p
+  | implode_url (Http (h, p)) = "http://" ^ h ^ implode_path p
+  | implode_url (Ftp (h, p)) = "ftp://" ^ h ^ implode_path p;
 
 
-(* unpack *)
+(* explode *)
 
 local
 
 val scan_host =
-  (Scan.any1 (fn s => s <> "/" andalso Symbol.not_eof s) >> implode) --|
+  (Scan.many1 (fn s => s <> "/" andalso Symbol.not_eof s) >> implode) --|
   Scan.ahead ($$ "/" || Scan.one Symbol.is_eof);
 
-val scan_path = Scan.any Symbol.not_eof >> (Path.unpack o implode);
-val scan_path_root = Scan.any Symbol.not_eof >> (Path.unpack o implode o cons "/");
+val scan_path = Scan.many Symbol.not_eof >> (Path.explode o implode);
+val scan_path_root = Scan.many Symbol.not_eof >> (Path.explode o implode o cons "/");
 
 val scan_url =
   Scan.unless (Scan.this_string "file:" ||
@@ -71,8 +71,13 @@
 
 in
 
-fun unpack s = Symbol.scanner "Malformed URL" scan_url (Symbol.explode s);
+fun explode_url s = Symbol.scanner "Malformed URL" scan_url (Symbol.explode s);
 
 end;
 
+
+(*final declarations of this structure!*)
+val implode = implode_url;
+val explode = explode_url;
+
 end;