diff -r c8087e6bd2ce -r 40630fec3b5d src/Pure/PIDE/xml.scala
--- a/src/Pure/PIDE/xml.scala	Sat Apr 09 14:51:54 2022 +0200
+++ b/src/Pure/PIDE/xml.scala	Sat Apr 09 15:28:55 2022 +0200
@@ -333,7 +333,7 @@
 
   object Decode {
     type T[A] = XML.Body => A
-    type V[A] = (List[String], XML.Body) => A
+    type V[A] = PartialFunction[(List[String], XML.Body), A]
     type P[A] = PartialFunction[List[String], A]