src/Pure/Tools/print_operation.scala
changeset 56864 0446c7ac2e32
child 59366 e94df7f6b608
equal deleted inserted replaced
56863:5fdb61a9a010 56864:0446c7ac2e32
       
     1 /*  Title:      Pure/System/print_operation.scala
       
     2     Author:     Makarius
       
     3 
       
     4 Print operations as asynchronous query.
       
     5 */
       
     6 
       
     7 package isabelle
       
     8 
       
     9 
       
    10 object Print_Operation
       
    11 {
       
    12   def print_operations(session: Session): List[(String, String)] =
       
    13     session.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(Nil: List[(String, String)])
       
    24 
       
    25     def get: List[(String, String)] = print_operations.value
       
    26 
       
    27     private def put(prover: Prover, msg: Prover.Protocol_Output): Boolean =
       
    28     {
       
    29       val ops =
       
    30       {
       
    31         import XML.Decode._
       
    32         list(pair(string, string))(YXML.parse_body(msg.text))
       
    33       }
       
    34       print_operations.change(_ => ops)
       
    35       true
       
    36     }
       
    37 
       
    38     override def start(prover: Prover): Unit =
       
    39       prover.protocol_command(Markup.PRINT_OPERATIONS)
       
    40 
       
    41     val functions = Map(Markup.PRINT_OPERATIONS -> put _)
       
    42   }
       
    43 }