1/* Title: Pure/Tools/print_operation.scala 2 Author: Makarius 3 4Print operations as asynchronous query. 5*/ 6 7package isabelle 8 9 10object Print_Operation 11{ 12 def print_operations(session: Session): List[(String, String)] = 13 session.get_protocol_handler("isabelle.Print_Operation$Handler") match { 14 case Some(handler: Handler) => handler.get 15 case _ => Nil 16 } 17 18 19 /* protocol handler */ 20 21 class Handler extends Session.Protocol_Handler 22 { 23 private val print_operations = Synchronized[List[(String, String)]](Nil) 24 25 override def init(session: Session): Unit = 26 session.protocol_command(Markup.PRINT_OPERATIONS) 27 28 def get: List[(String, String)] = print_operations.value 29 30 private def put(msg: Prover.Protocol_Output): Boolean = 31 { 32 val ops = 33 { 34 import XML.Decode._ 35 list(pair(string, string))(Symbol.decode_yxml(msg.text)) 36 } 37 print_operations.change(_ => ops) 38 true 39 } 40 41 val functions = List(Markup.PRINT_OPERATIONS -> put _) 42 } 43} 44