# HG changeset patch
# User wenzelm
# Date 1483539654 -3600
# Node ID 3f20c63f71be95010462a5080a1cdf434380a274
# Parent  dd3797f1e0d61e44c9c00df1f29865bc8049ba81
Windows UNC path is plain file;

diff -r dd3797f1e0d6 -r 3f20c63f71be src/Pure/General/url.ML
--- a/src/Pure/General/url.ML	Wed Jan 04 12:03:45 2017 +0100
+++ b/src/Pure/General/url.ML	Wed Jan 04 15:20:54 2017 +0100
@@ -8,7 +8,6 @@
 sig
   datatype T =
     File of Path.T |
-    RemoteFile of string * Path.T |
     Http of string * Path.T |
     Ftp of string * Path.T
   val append: T -> T -> T
@@ -25,17 +24,15 @@
 
 datatype T =
   File of Path.T |
-  RemoteFile of string * Path.T |
   Http of string * Path.T |
   Ftp of string * Path.T;
 
 
 (* append *)
 
-fun append (File p)            (File p') = File (Path.append p p')
-  | append (RemoteFile (h, p)) (File p') = RemoteFile (h, Path.append p p')
-  | append (Http (h, p))       (File p') = Http (h, Path.append p p')
-  | append (Ftp (h, p))        (File p') = Ftp (h, Path.append p p')
+fun append (File p) (File p') = File (Path.append p p')
+  | append (Http (h, p)) (File p') = Http (h, Path.append p p')
+  | append (Ftp (h, p)) (File p') = Ftp (h, Path.append p p')
   | append _ url = url;
 
 
@@ -44,7 +41,6 @@
 fun implode_path p = if Path.is_current p then "" else Path.implode p;
 
 fun implode_url (File p) = implode_path p
-  | implode_url (RemoteFile (h, p)) = "file://" ^ h ^ implode_path p
   | implode_url (Http (h, p)) = "http://" ^ h ^ implode_path p
   | implode_url (Ftp (h, p)) = "ftp://" ^ h ^ implode_path p;
 
@@ -65,7 +61,8 @@
     Scan.this_string "http:" || Scan.this_string "ftp:") 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_host -- scan_path >> RemoteFile ||
+  Scan.this_string "file://" |-- scan_host -- scan_path
+    >> (fn (h, p) => File (Path.append (Path.named_root h) p)) ||
   Scan.this_string "file:/" |-- scan_path_root >> File ||
   Scan.this_string "http://" |-- scan_host -- scan_path >> Http ||
   Scan.this_string "ftp://" |-- scan_host -- scan_path >> Ftp;