# HG changeset patch
# User wenzelm
# Date 1645445970 -3600
# Node ID ecaac5050ec2f307a2f211bb5201a24cc8993b63
# Parent  3c8f24e9eff128cc2e4f3f85fcc0e233540dd02c
tuned;

diff -r 3c8f24e9eff1 -r ecaac5050ec2 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 =