# HG changeset patch
# User wenzelm
# Date 1513889049 -3600
# Node ID caa4c900100991790c901d943ac98afbb36d7a3a
# Parent  318f44a5c164bbf215727a9559358103c58ea8a7
tuned signature;

diff -r 318f44a5c164 -r caa4c9001009 src/Pure/General/http.scala
--- a/src/Pure/General/http.scala	Thu Dec 21 17:28:39 2017 +0100
+++ b/src/Pure/General/http.scala	Thu Dec 21 21:44:09 2017 +0100
@@ -7,7 +7,7 @@
 package isabelle
 
 
-import java.net.{InetAddress, InetSocketAddress, URI, URLDecoder}
+import java.net.{InetAddress, InetSocketAddress, URI}
 import com.sun.net.httpserver.{HttpExchange, HttpHandler, HttpServer}
 
 import scala.collection.immutable.SortedMap
@@ -74,9 +74,7 @@
     def decode_properties: Properties.T =
       space_explode('&', request.text).map(s =>
         space_explode('=', s) match {
-          case List(a, b) =>
-            URLDecoder.decode(a, UTF8.charset_name) ->
-            URLDecoder.decode(b, UTF8.charset_name)
+          case List(a, b) => Url.decode(a) -> Url.decode(b)
           case _ => error("Malformed key-value pair in HTTP/POST: " + quote(s))
         })
   }
diff -r 318f44a5c164 -r caa4c9001009 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 =