src/Pure/PIDE/prover.scala
author wenzelm
Tue Aug 12 17:28:07 2014 +0200 (2014-08-12)
changeset 57915 448325de6e4f
parent 57906 020df63dd0a9
child 57916 2c2c24dbf0a4
permissions -rw-r--r--
more abstract Prover.System_Process, which allows to bypass Isabelle_System.Managed_Process;
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@57915
    10
import java.io.BufferedReader
wenzelm@57915
    11
wenzelm@57915
    12
wenzelm@56385
    13
object Prover
wenzelm@56385
    14
{
wenzelm@56393
    15
  /* syntax */
wenzelm@56393
    16
wenzelm@56393
    17
  trait Syntax
wenzelm@56393
    18
  {
wenzelm@56393
    19
    def add_keywords(keywords: Thy_Header.Keywords): Syntax
wenzelm@57906
    20
    def parse_spans(input: CharSequence): List[Command_Span.Span]
wenzelm@57901
    21
    def load_command(name: String): Option[List[String]]
wenzelm@56393
    22
    def load_commands_in(text: String): Boolean
wenzelm@56393
    23
  }
wenzelm@56393
    24
wenzelm@56393
    25
wenzelm@57915
    26
  /* underlying system process */
wenzelm@57915
    27
wenzelm@57915
    28
  trait System_Process
wenzelm@57915
    29
  {
wenzelm@57915
    30
    def channel: System_Channel
wenzelm@57915
    31
    def stdout: BufferedReader
wenzelm@57915
    32
    def stderr: BufferedReader
wenzelm@57915
    33
    def terminate: Unit
wenzelm@57915
    34
    def join: Int
wenzelm@57915
    35
  }
wenzelm@57915
    36
wenzelm@57915
    37
wenzelm@56385
    38
  /* messages */
wenzelm@56385
    39
wenzelm@56385
    40
  sealed abstract class Message
wenzelm@56385
    41
wenzelm@56386
    42
  class Input(val name: String, val args: List[String]) extends Message
wenzelm@56385
    43
  {
wenzelm@56385
    44
    override def toString: String =
wenzelm@56385
    45
      XML.Elem(Markup(Markup.PROVER_COMMAND, List((Markup.NAME, name))),
wenzelm@56385
    46
        args.map(s =>
wenzelm@56385
    47
          List(XML.Text("\n"), XML.elem(Markup.PROVER_ARG, YXML.parse_body(s)))).flatten).toString
wenzelm@56385
    48
  }
wenzelm@56385
    49
wenzelm@56385
    50
  class Output(val message: XML.Elem) extends Message
wenzelm@56385
    51
  {
wenzelm@56385
    52
    def kind: String = message.markup.name
wenzelm@56385
    53
    def properties: Properties.T = message.markup.properties
wenzelm@56385
    54
    def body: XML.Body = message.body
wenzelm@56385
    55
wenzelm@56385
    56
    def is_init = kind == Markup.INIT
wenzelm@56385
    57
    def is_exit = kind == Markup.EXIT
wenzelm@56385
    58
    def is_stdout = kind == Markup.STDOUT
wenzelm@56385
    59
    def is_stderr = kind == Markup.STDERR
wenzelm@56385
    60
    def is_system = kind == Markup.SYSTEM
wenzelm@56385
    61
    def is_status = kind == Markup.STATUS
wenzelm@56385
    62
    def is_report = kind == Markup.REPORT
wenzelm@56385
    63
    def is_syslog = is_init || is_exit || is_system || is_stderr
wenzelm@56385
    64
wenzelm@56385
    65
    override def toString: String =
wenzelm@56385
    66
    {
wenzelm@56385
    67
      val res =
wenzelm@56385
    68
        if (is_status || is_report) message.body.map(_.toString).mkString
wenzelm@56385
    69
        else Pretty.string_of(message.body)
wenzelm@56385
    70
      if (properties.isEmpty)
wenzelm@56385
    71
        kind.toString + " [[" + res + "]]"
wenzelm@56385
    72
      else
wenzelm@56385
    73
        kind.toString + " " +
wenzelm@56385
    74
          (for ((x, y) <- properties) yield x + "=" + y).mkString("{", ",", "}") + " [[" + res + "]]"
wenzelm@56385
    75
    }
wenzelm@56385
    76
  }
wenzelm@56385
    77
wenzelm@56385
    78
  class Protocol_Output(props: Properties.T, val bytes: Bytes)
wenzelm@56385
    79
    extends Output(XML.Elem(Markup(Markup.PROTOCOL, props), Nil))
wenzelm@56385
    80
  {
wenzelm@56385
    81
    lazy val text: String = bytes.toString
wenzelm@56385
    82
  }
wenzelm@56385
    83
}
wenzelm@56385
    84
wenzelm@56393
    85
wenzelm@56387
    86
trait Prover
wenzelm@56387
    87
{
wenzelm@56387
    88
  /* text and tree data */
wenzelm@56387
    89
wenzelm@56387
    90
  def encode(s: String): String
wenzelm@56387
    91
  def decode(s: String): String
wenzelm@56387
    92
wenzelm@56387
    93
  object Encode
wenzelm@56387
    94
  {
wenzelm@56387
    95
    val string: XML.Encode.T[String] = (s => XML.Encode.string(encode(s)))
wenzelm@56387
    96
  }
wenzelm@56387
    97
wenzelm@56387
    98
  def xml_cache: XML.Cache
wenzelm@56387
    99
wenzelm@56387
   100
wenzelm@56387
   101
  /* process management */
wenzelm@56387
   102
wenzelm@56387
   103
  def join(): Unit
wenzelm@56387
   104
  def terminate(): Unit
wenzelm@56387
   105
wenzelm@56387
   106
  def protocol_command_bytes(name: String, args: Bytes*): Unit
wenzelm@56387
   107
  def protocol_command(name: String, args: String*): Unit
wenzelm@56387
   108
wenzelm@56387
   109
wenzelm@56387
   110
  /* PIDE protocol commands */
wenzelm@56387
   111
wenzelm@56387
   112
  def options(opts: Options): Unit
wenzelm@56387
   113
wenzelm@56387
   114
  def define_blob(digest: SHA1.Digest, bytes: Bytes): Unit
wenzelm@56387
   115
  def define_command(command: Command): Unit
wenzelm@56387
   116
wenzelm@56387
   117
  def discontinue_execution(): Unit
wenzelm@56387
   118
  def cancel_exec(id: Document_ID.Exec): Unit
wenzelm@56387
   119
wenzelm@56387
   120
  def update(old_id: Document_ID.Version, new_id: Document_ID.Version,
wenzelm@56387
   121
    edits: List[Document.Edit_Command]): Unit
wenzelm@56387
   122
  def remove_versions(versions: List[Document.Version]): Unit
wenzelm@56387
   123
wenzelm@56387
   124
  def dialog_result(serial: Long, result: String): Unit
wenzelm@56387
   125
}
wenzelm@56387
   126