# HG changeset patch # User aspinall # Date 1094164538 -7200 # Node ID b62f7b493360f674cf5f96ccb87b5f91a097e848 # Parent fff9c761f89ebcd941734641a92223b602be65b1 Fix file:/// and file://localhost/ to give absolute paths diff -r fff9c761f89e -r b62f7b493360 src/Pure/General/url.ML --- a/src/Pure/General/url.ML Fri Sep 03 00:28:44 2004 +0200 +++ b/src/Pure/General/url.ML Fri Sep 03 00:35:38 2004 +0200 @@ -57,12 +57,13 @@ 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_url = Scan.unless (Scan.this_string "file:" || Scan.this_string "http:" || Scan.this_string "ftp:") scan_path >> File || - Scan.this_string "file:///" |-- scan_path >> File || - Scan.this_string "file://localhost/" |-- 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;