src/Pure/General/url.ML

 (*  Title:      Pure/General/url.ML
     ID:         $Id$
     Author:     Markus Wenzel, TU Muenchen
 
-Basic URLs.  See RFC 1738.
+Basic URLs, see RFC 1738.
 *)
 
 signature URL =
 sig
   datatype T =

 
 (* unpack *)
 
 local
 
-fun gen_host quant = (quant (not_equal "/" andf Symbol.not_eof) >> implode) --|
+val scan_host =
+  (Scan.any1 (not_equal "/" andf Symbol.not_eof) >> implode) --|
   Scan.ahead ($$ "/" || Scan.one Symbol.is_eof);
 
-val scan_host1 = gen_host Scan.any1;
 val scan_path = Scan.any Symbol.not_eof >> (Path.unpack o implode);
-val scan_path_root = Scan.any Symbol.not_eof >> (Path.unpack o (curry (op^) "/") o implode);
+val scan_path_root = Scan.any Symbol.not_eof >> (Path.unpack o implode o cons "/");
 
 val scan_url =
   Scan.unless (Scan.this_string "file:" ||
     Scan.this_string "http:" || Scan.this_string "ftp:") scan_path >> File ||
   Scan.this_string "file:///" |-- scan_path_root >> File ||
   Scan.this_string "file://localhost/" |-- scan_path_root >> File ||
-  Scan.this_string "file://" |-- scan_host1 -- scan_path >> RemoteFile ||
-  Scan.this_string "http://" |-- scan_host1 -- scan_path >> Http ||
-  Scan.this_string "ftp://" |-- scan_host1 -- scan_path >> Ftp ||
-  Scan.this_string "file://" |-- scan_host1 -- scan_path >> Ftp (* or other proto *)
+  Scan.this_string "file://" |-- scan_host -- scan_path >> RemoteFile ||
+  Scan.this_string "http://" |-- scan_host -- scan_path >> Http ||
+  Scan.this_string "ftp://" |-- scan_host -- scan_path >> Ftp;
 
 in
 
 fun unpack s = Symbol.scanner "Malformed URL" scan_url (Symbol.explode s);