# HG changeset patch
# User aspinall
# Date 1111752227 -3600
# Node ID 43f1669cbae32912f0959cc115b6bb3497bf9a4c
# Parent  484178635bd8022b907065c03da26e65bf31f680
Support non-standard file: URL syntax, temporarily.

diff -r 484178635bd8 -r 43f1669cbae3 src/Pure/General/url.ML
--- a/src/Pure/General/url.ML	Thu Mar 24 17:03:37 2005 +0100
+++ b/src/Pure/General/url.ML	Fri Mar 25 13:03:47 2005 +0100
@@ -2,7 +2,7 @@
     ID:         $Id$
     Author:     Markus Wenzel, TU Muenchen
 
-Basic URLs.
+Basic URLs.  See RFC 1738.
 *)
 
 signature URL =
@@ -66,7 +66,10 @@
   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 "ftp://" |-- scan_host1 -- scan_path >> Ftp ||
+  Scan.this_string "file://" |-- scan_host1 -- scan_path >> Ftp (* or other proto *) ||
+  (* NB: this next one is not in RFC 1738, but produced by some Haskell libraries *)
+  Scan.this_string "file:" |-- scan_path >> File 
 
 in