clarified signature: more explicit types;
authorwenzelm
Tue, 27 Dec 2022 11:44:37 +0100
changeset 76788 ce44e714d573
parent 76785 9e5a27486ca2
child 76789 27a8e9e8761e
clarified signature: more explicit types;
src/Pure/PIDE/session.scala
src/Pure/library.scala
--- 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
 }