# HG changeset patch
# User wenzelm
# Date 1621256043 -7200
# Node ID 00ef0f401a29221ac3ddc564fab3ae54dccb38f4
# Parent  bf51c23f3f99e839c2595d13910b7bbd2b891291
more uniform use of Properties.Eq.unapply, with slightly changed semantics in boundary cases;

diff -r bf51c23f3f99 -r 00ef0f401a29 src/Pure/General/http.scala
--- a/src/Pure/General/http.scala	Mon May 17 14:07:51 2021 +0200
+++ b/src/Pure/General/http.scala	Mon May 17 14:54:03 2021 +0200
@@ -200,10 +200,10 @@
   sealed case class Arg(method: String, uri: URI, request: Bytes)
   {
     def decode_properties: Properties.T =
-      space_explode('&', request.text).map(s =>
-        space_explode('=', s) match {
-          case List(a, b) => Url.decode(a) -> Url.decode(b)
-          case _ => error("Malformed key-value pair in HTTP/POST: " + quote(s))
+      space_explode('&', request.text).map(
+        {
+          case Properties.Eq(a, b) => Url.decode(a) -> Url.decode(b)
+          case s => error("Malformed key-value pair in HTTP/POST: " + quote(s))
         })
   }
 
diff -r bf51c23f3f99 -r 00ef0f401a29 src/Pure/ML/ml_statistics.scala
--- a/src/Pure/ML/ml_statistics.scala	Mon May 17 14:07:51 2021 +0200
+++ b/src/Pure/ML/ml_statistics.scala	Mon May 17 14:54:03 2021 +0200
@@ -58,12 +58,7 @@
   {
     def progress_stdout(line: String): Unit =
     {
-      val props =
-        Library.space_explode(',', line).flatMap((entry: String) =>
-          Library.space_explode('=', entry) match {
-            case List(a, b) => Some((a, b))
-            case _ => None
-          })
+      val props = Library.space_explode(',', line).flatMap(Properties.Eq.unapply)
       if (props.nonEmpty) consume(props)
     }
 
diff -r bf51c23f3f99 -r 00ef0f401a29 src/Pure/System/isabelle_platform.scala
--- a/src/Pure/System/isabelle_platform.scala	Mon May 17 14:07:51 2021 +0200
+++ b/src/Pure/System/isabelle_platform.scala	Mon May 17 14:54:03 2021 +0200
@@ -29,10 +29,7 @@
         val result = ssh.execute("bash -c " + Bash.string(script)).check
         new Isabelle_Platform(
           result.out_lines.map(line =>
-            space_explode('=', line) match {
-              case List(a, b) => (a, b)
-              case _ => error("Bad output: " + quote(result.out))
-            }))
+            Properties.Eq.unapply(line) getOrElse error("Bad output: " + quote(result.out))))
     }
   }