src/Pure/Tools/print_operation.scala
author wenzelm
Wed Nov 26 20:05:34 2014 +0100 (2014-11-26)
changeset 59058 a78612c67ec0
parent 56864 0446c7ac2e32
child 59366 e94df7f6b608
permissions -rw-r--r--
renamed "pairself" to "apply2", in accordance to @{apply 2};
     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 }