--- a/src/Pure/PIDE/session.scala Mon Dec 26 21:28:20 2022 +0100
+++ b/src/Pure/PIDE/session.scala Tue Dec 27 11:44:37 2022 +0100
@@ -356,10 +356,7 @@
private val protocol_handlers = Protocol_Handlers.init(session)
def get_protocol_handler[C <: Session.Protocol_Handler](c: Class[C]): Option[C] =
- protocol_handlers.get(c.getName) match {
- case Some(h) if Library.is_subclass(h.getClass, c) => Some(h.asInstanceOf[C])
- case _ => None
- }
+ protocol_handlers.get(c.getName).flatMap(Library.as_subclass(c))
def init_protocol_handler(handler: Session.Protocol_Handler): Unit =
protocol_handlers.init(handler)
--- a/src/Pure/library.scala Mon Dec 26 21:28:20 2022 +0100
+++ b/src/Pure/library.scala Tue Dec 27 11:44:37 2022 +0100
@@ -291,4 +291,7 @@
}
subclass(a)
}
+
+ def as_subclass[C](c: Class[C])(x: AnyRef): Option[C] =
+ if (x == null || is_subclass(x.getClass, c)) Some(x.asInstanceOf[C]) else None
}