src/Pure/General/url.ML
changeset 23784 75e6b9dd5336
parent 21858 05f57309170c
child 29606 fedb8be05f24
     1.1 --- a/src/Pure/General/url.ML	Wed Jul 11 12:23:34 2007 +0200
     1.2 +++ b/src/Pure/General/url.ML	Wed Jul 11 17:47:45 2007 +0200
     1.3 @@ -53,11 +53,11 @@
     1.4  local
     1.5  
     1.6  val scan_host =
     1.7 -  (Scan.many1 (fn s => s <> "/" andalso Symbol.not_eof s) >> implode) --|
     1.8 +  (Scan.many1 (fn s => s <> "/" andalso Symbol.is_regular s) >> implode) --|
     1.9    Scan.ahead ($$ "/" || Scan.one Symbol.is_eof);
    1.10  
    1.11 -val scan_path = Scan.many Symbol.not_eof >> (Path.explode o implode);
    1.12 -val scan_path_root = Scan.many Symbol.not_eof >> (Path.explode o implode o cons "/");
    1.13 +val scan_path = Scan.many Symbol.is_regular >> (Path.explode o implode);
    1.14 +val scan_path_root = Scan.many Symbol.is_regular >> (Path.explode o implode o cons "/");
    1.15  
    1.16  val scan_url =
    1.17    Scan.unless (Scan.this_string "file:" ||