src/Pure/Tools/print_operation.scala
author wenzelm
Tue Mar 14 00:09:15 2017 +0100 (2017-03-14)
changeset 65219 ed4b47b8c7dc
parent 65213 51c0f094dc02
child 65220 420f55912b3e
permissions -rw-r--r--
misc tuning and simplification;
wenzelm@59720
     1
/*  Title:      Pure/Tools/print_operation.scala
wenzelm@56864
     2
    Author:     Makarius
wenzelm@56864
     3
wenzelm@56864
     4
Print operations as asynchronous query.
wenzelm@56864
     5
*/
wenzelm@56864
     6
wenzelm@56864
     7
package isabelle
wenzelm@56864
     8
wenzelm@56864
     9
wenzelm@56864
    10
object Print_Operation
wenzelm@56864
    11
{
wenzelm@56864
    12
  def print_operations(session: Session): List[(String, String)] =
wenzelm@59366
    13
    session.get_protocol_handler("isabelle.Print_Operation$Handler") match {
wenzelm@56864
    14
      case Some(handler: Handler) => handler.get
wenzelm@56864
    15
      case _ => Nil
wenzelm@56864
    16
    }
wenzelm@56864
    17
wenzelm@56864
    18
wenzelm@56864
    19
  /* protocol handler */
wenzelm@56864
    20
wenzelm@56864
    21
  class Handler extends Session.Protocol_Handler
wenzelm@56864
    22
  {
wenzelm@61590
    23
    private val print_operations = Synchronized[List[(String, String)]](Nil)
wenzelm@56864
    24
wenzelm@56864
    25
    def get: List[(String, String)] = print_operations.value
wenzelm@56864
    26
wenzelm@65219
    27
    private def put(msg: Prover.Protocol_Output): Boolean =
wenzelm@56864
    28
    {
wenzelm@56864
    29
      val ops =
wenzelm@56864
    30
      {
wenzelm@56864
    31
        import XML.Decode._
wenzelm@56864
    32
        list(pair(string, string))(YXML.parse_body(msg.text))
wenzelm@56864
    33
      }
wenzelm@56864
    34
      print_operations.change(_ => ops)
wenzelm@56864
    35
      true
wenzelm@56864
    36
    }
wenzelm@56864
    37
wenzelm@65219
    38
    override def init(session: Session): Unit =
wenzelm@65219
    39
      session.protocol_command(Markup.PRINT_OPERATIONS)
wenzelm@56864
    40
wenzelm@65219
    41
    val functions = List(Markup.PRINT_OPERATIONS -> put _)
wenzelm@56864
    42
  }
wenzelm@56864
    43
}