tuned;
authorwenzelm
Mon, 21 Feb 2022 13:19:30 +0100
changeset 75111 ecaac5050ec2
parent 75110 3c8f24e9eff1
child 75112 899e70a9af83
tuned;
src/Pure/General/http.scala
--- a/src/Pure/General/http.scala	Mon Feb 21 13:17:52 2022 +0100
+++ b/src/Pure/General/http.scala	Mon Feb 21 13:19:30 2022 +0100
@@ -189,11 +189,9 @@
 
     def uri_path: Option[Path] =
       for {
-        s1 <- Option(uri.getPath)
-        s2 <- Library.try_unprefix(root, s1)
-        if Path.is_wellformed(s2)
-        p = Path.explode(s2)
-        if p.all_basic
+        s <- Option(uri.getPath).flatMap(Library.try_unprefix(root, _))
+        if Path.is_wellformed(s)
+        p = Path.explode(s) if p.all_basic
       } yield p
 
     def decode_properties: Properties.T =