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 =