changeset 72155 | 837b86b214d3 |
parent 71601 | 97ccf48c2f0c |
child 72212 | 53e8858b839f |
--- 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 }