--- a/src/Pure/PIDE/xml.scala Mon Mar 20 15:37:14 2017 +0100
+++ b/src/Pure/PIDE/xml.scala Mon Mar 20 17:24:40 2017 +0100
@@ -214,6 +214,7 @@
object Encode
{
type T[A] = A => XML.Body
+ type V[A] = PartialFunction[A, (List[String], XML.Body)]
/* atomic values */
@@ -270,7 +271,7 @@
case Some(x) => List(node(f(x)))
}
- def variant[A](fs: List[PartialFunction[A, (List[String], XML.Body)]]): T[A] =
+ def variant[A](fs: List[V[A]]): T[A] =
{
case x =>
val (f, tag) = fs.iterator.zipWithIndex.find(p => p._1.isDefinedAt(x)).get