prefer formal name;

--- a/src/Pure/Tools/print_operation.scala	Fri Aug 14 14:40:24 2020 +0200
+++ b/src/Pure/Tools/print_operation.scala	Sat Aug 15 13:36:42 2020 +0200
@@ -10,7 +10,7 @@
 object Print_Operation
 {
   def print_operations(session: Session): List[(String, String)] =
-    session.get_protocol_handler("isabelle.Print_Operation$Handler") match {
+    session.get_protocol_handler(classOf[Handler].getName) match {
       case Some(handler: Handler) => handler.get
       case _ => Nil
     }