src/Pure/General/url.scala

--- a/src/Pure/General/url.scala	Thu Dec 21 17:28:39 2017 +0100
+++ b/src/Pure/General/url.scala	Thu Dec 21 21:44:09 2017 +0100
@@ -9,8 +9,7 @@
 
 import java.io.{File => JFile}
 import java.nio.file.{Paths, FileSystemNotFoundException}
-import java.net.{URI, URISyntaxException}
-import java.net.{URL, MalformedURLException}
+import java.net.{URI, URISyntaxException, URL, MalformedURLException, URLDecoder, URLEncoder}
 import java.util.zip.GZIPInputStream
 
 
@@ -34,6 +33,12 @@
     catch { case ERROR(_) => false }
 
 
+  /* strings */
+
+  def decode(s: String): String = URLDecoder.decode(s, UTF8.charset_name)
+  def encode(s: String): String = URLEncoder.encode(s, UTF8.charset_name)
+
+
   /* read */
 
   private def read(url: URL, gzip: Boolean): String =