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