# HG changeset patch
# User wenzelm
# Date 1086800190 -7200
# Node ID 988b4342ed1f4e3edfc747b704cdd65bafd8ef1f
# Parent  944087c009328c8766d0183c8b4e68cafded0c89
tuned representation; added RemoteFile;

diff -r 944087c00932 -r 988b4342ed1f src/Pure/General/url.ML
--- a/src/Pure/General/url.ML	Wed Jun 09 18:56:21 2004 +0200
+++ b/src/Pure/General/url.ML	Wed Jun 09 18:56:30 2004 +0200
@@ -8,10 +8,11 @@
 
 signature URL =
 sig
-  type T
-  val file: Path.T -> T
-  val http: string * Path.T -> T
-  val ftp: string * Path.T -> T
+  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
   val pack: T -> string
   val unpack: string -> T
@@ -20,49 +21,46 @@
 structure Url: URL =
 struct
 
-
 (* type url *)
 
-datatype scheme = File | Http of string | Ftp of string;
-
-datatype T = Url of scheme * Path.T;
-
-fun file p = Url (File, p);
-fun http (h, p) = Url (Http h, p);
-fun ftp (h, p) = Url (Ftp h, p);
+datatype T =
+  File of Path.T |
+  RemoteFile of string * Path.T |
+  Http of string * Path.T |
+  Ftp of string * Path.T;
 
 
 (* append *)
 
-fun append (Url (s, p)) (Url (File, p')) = Url (s, Path.append p p')
+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')
   | append _ url = url;
 
 
 (* pack *)
 
-fun pack_scheme File = ""
-  | pack_scheme (Http host) = "http://" ^ host
-  | pack_scheme (Ftp host) = "ftp://" ^ host;
+fun pack_path p = if Path.is_current p then "" else Path.pack p;
 
-fun pack (Url (s, p)) = pack_scheme s ^ (if Path.is_current p then "" else Path.pack p);
+fun pack (File p) = pack_path p
+  | pack (RemoteFile (h, p)) = "file://" ^ h ^ pack_path p
+  | pack (Http (h, p)) = "http://" ^ h ^ pack_path p
+  | pack (Ftp (h, p)) = "ftp://" ^ h ^ pack_path p;
 
 
 (* unpack *)
 
-fun scan_lits [] x = ("", x)
-  | scan_lits (c :: cs) x = (($$ c -- scan_lits cs) >> op ^) x;
-
-val scan_literal = scan_lits o Symbol.explode;
-
 val scan_path = Scan.any Symbol.not_eof >> (Path.unpack o implode);
 val scan_host = Scan.any1 (not_equal "/" andf Symbol.not_eof) >> implode;
 
 val scan_url =
-  scan_literal "http://" |-- scan_host -- scan_path >> http ||
-  scan_literal "ftp://" |-- scan_host -- scan_path >> ftp ||
-  Scan.unless (scan_literal "http:" || scan_literal "ftp:") scan_path >> file;
+  Scan.unless (Scan.this_string "file:" ||
+    Scan.this_string "http:" || Scan.this_string "ftp:") scan_path >> File ||
+  Scan.this_string "file://" |-- scan_host -- scan_path >> RemoteFile ||
+  Scan.this_string "http://" |-- scan_host -- scan_path >> Http ||
+  Scan.this_string "ftp://" |-- scan_host -- scan_path >> Ftp;
 
 fun unpack s = Symbol.scanner "Malformed URL" scan_url (Symbol.explode s);
 
-
 end;