# HG changeset patch
# User wenzelm
# Date 1597491402 -7200
# Node ID 837b86b214d315750adb5e70df9cfcbdf3363e88
# Parent  2b41b710f6ef1be390c56cd3b9e561f4d48bdebc
prefer formal name;

diff -r 2b41b710f6ef -r 837b86b214d3 src/Pure/Tools/print_operation.scala
--- 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
     }