equal
deleted
inserted
replaced
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 |