Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/Pure/General/url.ML
changeset 23784 75e6b9dd5336
parent 21858 05f57309170c
child 29606 fedb8be05f24 
--- a/src/Pure/General/url.ML	Wed Jul 11 12:23:34 2007 +0200
+++ b/src/Pure/General/url.ML	Wed Jul 11 17:47:45 2007 +0200
@@ -53,11 +53,11 @@
 local
 
 val scan_host =
-  (Scan.many1 (fn s => s <> "/" andalso Symbol.not_eof s) >> implode) --|
+  (Scan.many1 (fn s => s <> "/" andalso Symbol.is_regular s) >> implode) --|
   Scan.ahead ($$ "/" || Scan.one Symbol.is_eof);
 
-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_path = Scan.many Symbol.is_regular >> (Path.explode o implode);
+val scan_path_root = Scan.many Symbol.is_regular >> (Path.explode o implode o cons "/");
 
 val scan_url =
   Scan.unless (Scan.this_string "file:" ||
isabelle