src/Pure/Tools/print_operation.scala
author wenzelm
Mon, 05 May 2014 15:17:07 +0200
changeset 56864 0446c7ac2e32
child 59366 e94df7f6b608
permissions -rw-r--r--
support print operations as asynchronous query;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
56864
0446c7ac2e32 support print operations as asynchronous query;
wenzelm
parents:
diff changeset
     1
/*  Title:      Pure/System/print_operation.scala
0446c7ac2e32 support print operations as asynchronous query;
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
0446c7ac2e32 support print operations as asynchronous query;
wenzelm
parents:
diff changeset
     3
0446c7ac2e32 support print operations as asynchronous query;
wenzelm
parents:
diff changeset
     4
Print operations as asynchronous query.
0446c7ac2e32 support print operations as asynchronous query;
wenzelm
parents:
diff changeset
     5
*/
0446c7ac2e32 support print operations as asynchronous query;
wenzelm
parents:
diff changeset
     6
0446c7ac2e32 support print operations as asynchronous query;
wenzelm
parents:
diff changeset
     7
package isabelle
0446c7ac2e32 support print operations as asynchronous query;
wenzelm
parents:
diff changeset
     8
0446c7ac2e32 support print operations as asynchronous query;
wenzelm
parents:
diff changeset
     9
0446c7ac2e32 support print operations as asynchronous query;
wenzelm
parents:
diff changeset
    10
object Print_Operation
0446c7ac2e32 support print operations as asynchronous query;
wenzelm
parents:
diff changeset
    11
{
0446c7ac2e32 support print operations as asynchronous query;
wenzelm
parents:
diff changeset
    12
  def print_operations(session: Session): List[(String, String)] =
0446c7ac2e32 support print operations as asynchronous query;
wenzelm
parents:
diff changeset
    13
    session.protocol_handler("isabelle.Print_Operation$Handler") match {
0446c7ac2e32 support print operations as asynchronous query;
wenzelm
parents:
diff changeset
    14
      case Some(handler: Handler) => handler.get
0446c7ac2e32 support print operations as asynchronous query;
wenzelm
parents:
diff changeset
    15
      case _ => Nil
0446c7ac2e32 support print operations as asynchronous query;
wenzelm
parents:
diff changeset
    16
    }
0446c7ac2e32 support print operations as asynchronous query;
wenzelm
parents:
diff changeset
    17
0446c7ac2e32 support print operations as asynchronous query;
wenzelm
parents:
diff changeset
    18
0446c7ac2e32 support print operations as asynchronous query;
wenzelm
parents:
diff changeset
    19
  /* protocol handler */
0446c7ac2e32 support print operations as asynchronous query;
wenzelm
parents:
diff changeset
    20
0446c7ac2e32 support print operations as asynchronous query;
wenzelm
parents:
diff changeset
    21
  class Handler extends Session.Protocol_Handler
0446c7ac2e32 support print operations as asynchronous query;
wenzelm
parents:
diff changeset
    22
  {
0446c7ac2e32 support print operations as asynchronous query;
wenzelm
parents:
diff changeset
    23
    private val print_operations = Synchronized(Nil: List[(String, String)])
0446c7ac2e32 support print operations as asynchronous query;
wenzelm
parents:
diff changeset
    24
0446c7ac2e32 support print operations as asynchronous query;
wenzelm
parents:
diff changeset
    25
    def get: List[(String, String)] = print_operations.value
0446c7ac2e32 support print operations as asynchronous query;
wenzelm
parents:
diff changeset
    26
0446c7ac2e32 support print operations as asynchronous query;
wenzelm
parents:
diff changeset
    27
    private def put(prover: Prover, msg: Prover.Protocol_Output): Boolean =
0446c7ac2e32 support print operations as asynchronous query;
wenzelm
parents:
diff changeset
    28
    {
0446c7ac2e32 support print operations as asynchronous query;
wenzelm
parents:
diff changeset
    29
      val ops =
0446c7ac2e32 support print operations as asynchronous query;
wenzelm
parents:
diff changeset
    30
      {
0446c7ac2e32 support print operations as asynchronous query;
wenzelm
parents:
diff changeset
    31
        import XML.Decode._
0446c7ac2e32 support print operations as asynchronous query;
wenzelm
parents:
diff changeset
    32
        list(pair(string, string))(YXML.parse_body(msg.text))
0446c7ac2e32 support print operations as asynchronous query;
wenzelm
parents:
diff changeset
    33
      }
0446c7ac2e32 support print operations as asynchronous query;
wenzelm
parents:
diff changeset
    34
      print_operations.change(_ => ops)
0446c7ac2e32 support print operations as asynchronous query;
wenzelm
parents:
diff changeset
    35
      true
0446c7ac2e32 support print operations as asynchronous query;
wenzelm
parents:
diff changeset
    36
    }
0446c7ac2e32 support print operations as asynchronous query;
wenzelm
parents:
diff changeset
    37
0446c7ac2e32 support print operations as asynchronous query;
wenzelm
parents:
diff changeset
    38
    override def start(prover: Prover): Unit =
0446c7ac2e32 support print operations as asynchronous query;
wenzelm
parents:
diff changeset
    39
      prover.protocol_command(Markup.PRINT_OPERATIONS)
0446c7ac2e32 support print operations as asynchronous query;
wenzelm
parents:
diff changeset
    40
0446c7ac2e32 support print operations as asynchronous query;
wenzelm
parents:
diff changeset
    41
    val functions = Map(Markup.PRINT_OPERATIONS -> put _)
0446c7ac2e32 support print operations as asynchronous query;
wenzelm
parents:
diff changeset
    42
  }
0446c7ac2e32 support print operations as asynchronous query;
wenzelm
parents:
diff changeset
    43
}