# HG changeset patch
# User wenzelm
# Date 1672137877 -3600
# Node ID ce44e714d57321d6a8c2113fa818f9a06a20e2e3
# Parent  9e5a27486ca23defab1a0d112cedc2d30dec078c
clarified signature: more explicit types;

diff -r 9e5a27486ca2 -r ce44e714d573 src/Pure/PIDE/session.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)
diff -r 9e5a27486ca2 -r ce44e714d573 src/Pure/library.scala
--- 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
 }