src/Pure/General/url.ML

 signature URL =
 sig
   datatype T =
     File of Path.T |
     Http of string * Path.T |
+    Https of string * Path.T |
     Ftp of string * Path.T
   val append: T -> T -> T
   val implode: T -> string
   val explode: string -> T
   val pretty: T -> Pretty.T

 (* type url *)
 
 datatype T =
   File of Path.T |
   Http of string * Path.T |
+  Https of string * Path.T |
   Ftp of string * Path.T;
 
 
 (* append *)
 
 fun append (File p) (File p') = File (Path.append p p')
   | append (Http (h, p)) (File p') = Http (h, Path.append p p')
+  | append (Https (h, p)) (File p') = Https (h, Path.append p p')
   | append (Ftp (h, p)) (File p') = Ftp (h, Path.append p p')
   | append _ url = url;
 
 
 (* implode *)
 
 fun implode_path p = if Path.is_current p then "" else Path.implode p;
 
 fun implode_url (File p) = implode_path p
   | implode_url (Http (h, p)) = "http://" ^ h ^ implode_path p
+  | implode_url (Https (h, p)) = "https://" ^ h ^ implode_path p
   | implode_url (Ftp (h, p)) = "ftp://" ^ h ^ implode_path p;
 
 
 (* explode *)
 

 
 val scan_path = Scan.many Symbol.not_eof >> (Path.explode o implode);
 val scan_path_root = Scan.many Symbol.not_eof >> (Path.explode o implode o cons "/");
 
 val scan_url =
-  Scan.unless (Scan.this_string "file:" ||
-    Scan.this_string "http:" || Scan.this_string "ftp:") scan_path >> File ||
+  Scan.unless
+    (Scan.this_string "file:" || Scan.this_string "http:" ||
+      Scan.this_string "https:" || 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
     >> (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 "https://" |-- scan_host -- scan_path >> Https ||
   Scan.this_string "ftp://" |-- scan_host -- scan_path >> Ftp;
 
 in
 
 fun explode_url s = Symbol.scanner "Malformed URL" scan_url (Symbol.explode s);