src/Pure/PIDE/prover.scala
author wenzelm
Sat May 03 22:47:43 2014 +0200 (2014-05-03 ago)
changeset 56843 b2bfcd8cda80
parent 56394 bbf4d512f395
child 57901 e1abca2527da
permissions -rw-r--r--
support for path completion based on file-system content;
     1 /*  Title:      Pure/PIDE/prover.scala
     2     Author:     Makarius
     3 
     4 General prover operations.
     5 */
     6 
     7 package isabelle
     8 
     9 
    10 object Prover
    11 {
    12   /* syntax */
    13 
    14   trait Syntax
    15   {
    16     def add_keywords(keywords: Thy_Header.Keywords): Syntax
    17     def scan(input: CharSequence): List[Token]
    18     def load(span: List[Token]): Option[List[String]]
    19     def load_commands_in(text: String): Boolean
    20   }
    21 
    22 
    23   /* messages */
    24 
    25   sealed abstract class Message
    26 
    27   class Input(val name: String, val args: List[String]) extends Message
    28   {
    29     override def toString: String =
    30       XML.Elem(Markup(Markup.PROVER_COMMAND, List((Markup.NAME, name))),
    31         args.map(s =>
    32           List(XML.Text("\n"), XML.elem(Markup.PROVER_ARG, YXML.parse_body(s)))).flatten).toString
    33   }
    34 
    35   class Output(val message: XML.Elem) extends Message
    36   {
    37     def kind: String = message.markup.name
    38     def properties: Properties.T = message.markup.properties
    39     def body: XML.Body = message.body
    40 
    41     def is_init = kind == Markup.INIT
    42     def is_exit = kind == Markup.EXIT
    43     def is_stdout = kind == Markup.STDOUT
    44     def is_stderr = kind == Markup.STDERR
    45     def is_system = kind == Markup.SYSTEM
    46     def is_status = kind == Markup.STATUS
    47     def is_report = kind == Markup.REPORT
    48     def is_syslog = is_init || is_exit || is_system || is_stderr
    49 
    50     override def toString: String =
    51     {
    52       val res =
    53         if (is_status || is_report) message.body.map(_.toString).mkString
    54         else Pretty.string_of(message.body)
    55       if (properties.isEmpty)
    56         kind.toString + " [[" + res + "]]"
    57       else
    58         kind.toString + " " +
    59           (for ((x, y) <- properties) yield x + "=" + y).mkString("{", ",", "}") + " [[" + res + "]]"
    60     }
    61   }
    62 
    63   class Protocol_Output(props: Properties.T, val bytes: Bytes)
    64     extends Output(XML.Elem(Markup(Markup.PROTOCOL, props), Nil))
    65   {
    66     lazy val text: String = bytes.toString
    67   }
    68 }
    69 
    70 
    71 trait Prover
    72 {
    73   /* text and tree data */
    74 
    75   def encode(s: String): String
    76   def decode(s: String): String
    77 
    78   object Encode
    79   {
    80     val string: XML.Encode.T[String] = (s => XML.Encode.string(encode(s)))
    81   }
    82 
    83   def xml_cache: XML.Cache
    84 
    85 
    86   /* process management */
    87 
    88   def join(): Unit
    89   def terminate(): Unit
    90 
    91   def protocol_command_bytes(name: String, args: Bytes*): Unit
    92   def protocol_command(name: String, args: String*): Unit
    93 
    94 
    95   /* PIDE protocol commands */
    96 
    97   def options(opts: Options): Unit
    98 
    99   def define_blob(digest: SHA1.Digest, bytes: Bytes): Unit
   100   def define_command(command: Command): Unit
   101 
   102   def discontinue_execution(): Unit
   103   def cancel_exec(id: Document_ID.Exec): Unit
   104 
   105   def update(old_id: Document_ID.Version, new_id: Document_ID.Version,
   106     edits: List[Document.Edit_Command]): Unit
   107   def remove_versions(versions: List[Document.Version]): Unit
   108 
   109   def dialog_result(serial: Long, result: String): Unit
   110 }
   111