Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Fix file:/// and file://localhost/ to return local file result
authoraspinall
Fri, 03 Sep 2004 00:28:44 +0200
changeset 15174 fff9c761f89e
parent 15173 e1582a0d29b5
child 15175 b62f7b493360
Fix file:/// and file://localhost/ to return local file result
src/Pure/General/url.ML file | annotate | diff | comparison | revisions 
--- a/src/Pure/General/url.ML	Fri Sep 03 00:26:18 2004 +0200
+++ b/src/Pure/General/url.ML	Fri Sep 03 00:28:44 2004 +0200
@@ -55,15 +55,15 @@
 fun gen_host quant = (quant (not_equal "/" andf Symbol.not_eof) >> implode) --|
   Scan.ahead ($$ "/" || Scan.one Symbol.is_eof);
 
-val scan_host = gen_host Scan.any;
 val scan_host1 = gen_host Scan.any1;
 val scan_path = Scan.any Symbol.not_eof >> (Path.unpack o implode);
 
 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_host >> (fn "localhost" => "" | h => h)) -- scan_path >> RemoteFile ||
+  Scan.this_string "file:///" |-- scan_path >> File ||
+  Scan.this_string "file://localhost/" |-- scan_path >> 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;
isabelle