src/Pure/PIDE/xml.scala

--- a/src/Pure/PIDE/xml.scala	Thu Oct 10 15:52:30 2019 +0200
+++ b/src/Pure/PIDE/xml.scala	Thu Oct 10 16:51:47 2019 +0200
@@ -241,6 +241,7 @@
   {
     type T[A] = A => XML.Body
     type V[A] = PartialFunction[A, (List[String], XML.Body)]
+    type P[A] = PartialFunction[A, List[String]]
 
 
     /* atomic values */
@@ -309,6 +310,7 @@
   {
     type T[A] = XML.Body => A
     type V[A] = (List[String], XML.Body) => A
+    type P[A] = PartialFunction[List[String], A]
 
 
     /* atomic values */