# HG changeset patch
# User wenzelm
# Date 1605980678 -3600
# Node ID b22f1e2b4e9432fa2fa613bf9d9e1f737e987d18
# Parent  7ab733b2aecb76ad67d1bbad85117cc988d9158d
removed unused material;

diff -r 7ab733b2aecb -r b22f1e2b4e94 src/Pure/General/url.ML
--- a/src/Pure/General/url.ML	Sat Nov 21 18:16:25 2020 +0100
+++ b/src/Pure/General/url.ML	Sat Nov 21 18:44:38 2020 +0100
@@ -1,7 +1,7 @@
 (*  Title:      Pure/General/url.ML
-    Author:     Markus Wenzel, TU Muenchen
+    Author:     Makarius
 
-Basic URLs, see RFC 1738 and RFC 2396.
+Basic URLs (see RFC 1738 and RFC 2396).
 *)
 
 signature URL =
@@ -11,11 +11,7 @@
     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
-  val print: T -> string
 end;
 
 structure Url: URL =
@@ -30,25 +26,6 @@
   Ftp of string * Path.T;
 
 
-(* append *)
-
-fun append (File p) (File p') = File (p + p')
-  | append (Http (h, p)) (File p') = Http (h, p + p')
-  | append (Https (h, p)) (File p') = Https (h, p + p')
-  | append (Ftp (h, p)) (File p') = Ftp (h, 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 *)
 
 local
@@ -75,20 +52,8 @@
 
 in
 
-fun explode_url s = Symbol.scanner "Malformed URL" scan_url (Symbol.explode s);
+fun explode s = Symbol.scanner "Malformed URL" scan_url (Symbol.explode s);
 
 end;
 
-
-(* print *)
-
-val pretty = Pretty.mark_str o `Markup.url o implode_url;
-
-val print = Pretty.unformatted_string_of o pretty;
-
-
-(*final declarations of this structure!*)
-val implode = implode_url;
-val explode = explode_url;
-
 end;