# HG changeset patch
# User wenzelm
# Date 1598526418 -7200
# Node ID 8f9cffa78112959a97178ebe906568886b03f7cc
# Parent  5924c1da3c45d42739a871ff6dcfa98258fcd1af
clarified signature;

diff -r 5924c1da3c45 -r 8f9cffa78112 src/Pure/PIDE/session.scala
--- a/src/Pure/PIDE/session.scala	Thu Aug 27 12:51:57 2020 +0200
+++ b/src/Pure/PIDE/session.scala	Thu Aug 27 13:06:58 2020 +0200
@@ -363,8 +363,11 @@
 
   private val protocol_handlers = Protocol_Handlers.init(session)
 
-  def get_protocol_handler(name: String): Option[Session.Protocol_Handler] =
-    protocol_handlers.get(name)
+  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
+    }
 
   def init_protocol_handler(handler: Session.Protocol_Handler): Unit =
     protocol_handlers.init(handler)
diff -r 5924c1da3c45 -r 8f9cffa78112 src/Pure/Tools/print_operation.scala
--- a/src/Pure/Tools/print_operation.scala	Thu Aug 27 12:51:57 2020 +0200
+++ b/src/Pure/Tools/print_operation.scala	Thu Aug 27 13:06:58 2020 +0200
@@ -9,9 +9,9 @@
 
 object Print_Operation
 {
-  def print_operations(session: Session): List[(String, String)] =
-    session.get_protocol_handler(classOf[Handler].getName) match {
-      case Some(handler: Handler) => handler.get
+  def get(session: Session): List[(String, String)] =
+    session.get_protocol_handler(classOf[Handler]) match {
+      case Some(h) => h.get
       case _ => Nil
     }
 
@@ -22,11 +22,11 @@
   {
     private val print_operations = Synchronized[List[(String, String)]](Nil)
 
+    def get: List[(String, String)] = print_operations.value
+
     override def init(session: Session): Unit =
       session.protocol_command(Markup.PRINT_OPERATIONS)
 
-    def get: List[(String, String)] = print_operations.value
-
     private def put(msg: Prover.Protocol_Output): Boolean =
     {
       val ops =
diff -r 5924c1da3c45 -r 8f9cffa78112 src/Tools/jEdit/src/query_dockable.scala
--- a/src/Tools/jEdit/src/query_dockable.scala	Thu Aug 27 12:51:57 2020 +0200
+++ b/src/Tools/jEdit/src/query_dockable.scala	Thu Aug 27 13:06:58 2020 +0200
@@ -215,10 +215,8 @@
         }
 
       _items =
-        Print_Operation.print_operations(PIDE.session).map(
-          {
-            case (name, description) => new Item(name, description, was_selected(name))
-          })
+        for ((name, description) <- Print_Operation.get(PIDE.session))
+        yield new Item(name, description, was_selected(name))
       _items
     }