src/Pure/Tools/print_operation.scala
changeset 72155 837b86b214d3
parent 71601 97ccf48c2f0c
child 72212 53e8858b839f
equal deleted inserted replaced
72154:2b41b710f6ef 72155:837b86b214d3
     8 
     8 
     9 
     9 
    10 object Print_Operation
    10 object Print_Operation
    11 {
    11 {
    12   def print_operations(session: Session): List[(String, String)] =
    12   def print_operations(session: Session): List[(String, String)] =
    13     session.get_protocol_handler("isabelle.Print_Operation$Handler") match {
    13     session.get_protocol_handler(classOf[Handler].getName) match {
    14       case Some(handler: Handler) => handler.get
    14       case Some(handler: Handler) => handler.get
    15       case _ => Nil
    15       case _ => Nil
    16     }
    16     }
    17 
    17 
    18 
    18