src/Pure/PIDE/prover.scala
author wenzelm
Thu Apr 03 13:49:37 2014 +0200 (2014-04-03)
changeset 56386 fe520afb8041
parent 56385 76acce58aeab
child 56387 d92eb5c3960d
permissions -rw-r--r--
tuned signature -- pro forma;
wenzelm@56385
     1
/*  Title:      Pure/PIDE/prover.scala
wenzelm@56385
     2
    Author:     Makarius
wenzelm@56385
     3
wenzelm@56385
     4
General prover operations.
wenzelm@56385
     5
*/
wenzelm@56385
     6
wenzelm@56385
     7
package isabelle
wenzelm@56385
     8
wenzelm@56385
     9
wenzelm@56385
    10
object Prover
wenzelm@56385
    11
{
wenzelm@56385
    12
  /* messages */
wenzelm@56385
    13
wenzelm@56385
    14
  sealed abstract class Message
wenzelm@56385
    15
wenzelm@56386
    16
  class Input(val name: String, val args: List[String]) extends Message
wenzelm@56385
    17
  {
wenzelm@56385
    18
    override def toString: String =
wenzelm@56385
    19
      XML.Elem(Markup(Markup.PROVER_COMMAND, List((Markup.NAME, name))),
wenzelm@56385
    20
        args.map(s =>
wenzelm@56385
    21
          List(XML.Text("\n"), XML.elem(Markup.PROVER_ARG, YXML.parse_body(s)))).flatten).toString
wenzelm@56385
    22
  }
wenzelm@56385
    23
wenzelm@56385
    24
  class Output(val message: XML.Elem) extends Message
wenzelm@56385
    25
  {
wenzelm@56385
    26
    def kind: String = message.markup.name
wenzelm@56385
    27
    def properties: Properties.T = message.markup.properties
wenzelm@56385
    28
    def body: XML.Body = message.body
wenzelm@56385
    29
wenzelm@56385
    30
    def is_init = kind == Markup.INIT
wenzelm@56385
    31
    def is_exit = kind == Markup.EXIT
wenzelm@56385
    32
    def is_stdout = kind == Markup.STDOUT
wenzelm@56385
    33
    def is_stderr = kind == Markup.STDERR
wenzelm@56385
    34
    def is_system = kind == Markup.SYSTEM
wenzelm@56385
    35
    def is_status = kind == Markup.STATUS
wenzelm@56385
    36
    def is_report = kind == Markup.REPORT
wenzelm@56385
    37
    def is_syslog = is_init || is_exit || is_system || is_stderr
wenzelm@56385
    38
wenzelm@56385
    39
    override def toString: String =
wenzelm@56385
    40
    {
wenzelm@56385
    41
      val res =
wenzelm@56385
    42
        if (is_status || is_report) message.body.map(_.toString).mkString
wenzelm@56385
    43
        else Pretty.string_of(message.body)
wenzelm@56385
    44
      if (properties.isEmpty)
wenzelm@56385
    45
        kind.toString + " [[" + res + "]]"
wenzelm@56385
    46
      else
wenzelm@56385
    47
        kind.toString + " " +
wenzelm@56385
    48
          (for ((x, y) <- properties) yield x + "=" + y).mkString("{", ",", "}") + " [[" + res + "]]"
wenzelm@56385
    49
    }
wenzelm@56385
    50
  }
wenzelm@56385
    51
wenzelm@56385
    52
  class Protocol_Output(props: Properties.T, val bytes: Bytes)
wenzelm@56385
    53
    extends Output(XML.Elem(Markup(Markup.PROTOCOL, props), Nil))
wenzelm@56385
    54
  {
wenzelm@56385
    55
    lazy val text: String = bytes.toString
wenzelm@56385
    56
  }
wenzelm@56385
    57
}
wenzelm@56385
    58