changeset 75436 | 40630fec3b5d |
parent 75393 | 87ebf5a50283 |
child 76351 | 2cee31cd92f0 |
--- 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]