src/Pure/General/url.ML
changeset 21858 05f57309170c
parent 21515 43d55165b282
child 23784 75e6b9dd5336
     1.1 --- a/src/Pure/General/url.ML	Thu Dec 14 22:19:39 2006 +0100
     1.2 +++ b/src/Pure/General/url.ML	Fri Dec 15 00:08:06 2006 +0100
     1.3 @@ -13,8 +13,8 @@
     1.4      Http of string * Path.T |
     1.5      Ftp of string * Path.T
     1.6    val append: T -> T -> T
     1.7 -  val pack: T -> string
     1.8 -  val unpack: string -> T
     1.9 +  val implode: T -> string
    1.10 +  val explode: string -> T
    1.11  end;
    1.12  
    1.13  structure Url: URL =
    1.14 @@ -38,26 +38,26 @@
    1.15    | append _ url = url;
    1.16  
    1.17  
    1.18 -(* pack *)
    1.19 +(* implode *)
    1.20  
    1.21 -fun pack_path p = if Path.is_current p then "" else Path.pack p;
    1.22 +fun implode_path p = if Path.is_current p then "" else Path.implode p;
    1.23  
    1.24 -fun pack (File p) = pack_path p
    1.25 -  | pack (RemoteFile (h, p)) = "file://" ^ h ^ pack_path p
    1.26 -  | pack (Http (h, p)) = "http://" ^ h ^ pack_path p
    1.27 -  | pack (Ftp (h, p)) = "ftp://" ^ h ^ pack_path p;
    1.28 +fun implode_url (File p) = implode_path p
    1.29 +  | implode_url (RemoteFile (h, p)) = "file://" ^ h ^ implode_path p
    1.30 +  | implode_url (Http (h, p)) = "http://" ^ h ^ implode_path p
    1.31 +  | implode_url (Ftp (h, p)) = "ftp://" ^ h ^ implode_path p;
    1.32  
    1.33  
    1.34 -(* unpack *)
    1.35 +(* explode *)
    1.36  
    1.37  local
    1.38  
    1.39  val scan_host =
    1.40 -  (Scan.any1 (fn s => s <> "/" andalso Symbol.not_eof s) >> implode) --|
    1.41 +  (Scan.many1 (fn s => s <> "/" andalso Symbol.not_eof s) >> implode) --|
    1.42    Scan.ahead ($$ "/" || Scan.one Symbol.is_eof);
    1.43  
    1.44 -val scan_path = Scan.any Symbol.not_eof >> (Path.unpack o implode);
    1.45 -val scan_path_root = Scan.any Symbol.not_eof >> (Path.unpack o implode o cons "/");
    1.46 +val scan_path = Scan.many Symbol.not_eof >> (Path.explode o implode);
    1.47 +val scan_path_root = Scan.many Symbol.not_eof >> (Path.explode o implode o cons "/");
    1.48  
    1.49  val scan_url =
    1.50    Scan.unless (Scan.this_string "file:" ||
    1.51 @@ -71,8 +71,13 @@
    1.52  
    1.53  in
    1.54  
    1.55 -fun unpack s = Symbol.scanner "Malformed URL" scan_url (Symbol.explode s);
    1.56 +fun explode_url s = Symbol.scanner "Malformed URL" scan_url (Symbol.explode s);
    1.57  
    1.58  end;
    1.59  
    1.60 +
    1.61 +(*final declarations of this structure!*)
    1.62 +val implode = implode_url;
    1.63 +val explode = explode_url;
    1.64 +
    1.65  end;