56385
|
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 |
/* messages */
|
|
13 |
|
|
14 |
sealed abstract class Message
|
|
15 |
|
56386
|
16 |
class Input(val name: String, val args: List[String]) extends Message
|
56385
|
17 |
{
|
|
18 |
override def toString: String =
|
|
19 |
XML.Elem(Markup(Markup.PROVER_COMMAND, List((Markup.NAME, name))),
|
|
20 |
args.map(s =>
|
|
21 |
List(XML.Text("\n"), XML.elem(Markup.PROVER_ARG, YXML.parse_body(s)))).flatten).toString
|
|
22 |
}
|
|
23 |
|
|
24 |
class Output(val message: XML.Elem) extends Message
|
|
25 |
{
|
|
26 |
def kind: String = message.markup.name
|
|
27 |
def properties: Properties.T = message.markup.properties
|
|
28 |
def body: XML.Body = message.body
|
|
29 |
|
|
30 |
def is_init = kind == Markup.INIT
|
|
31 |
def is_exit = kind == Markup.EXIT
|
|
32 |
def is_stdout = kind == Markup.STDOUT
|
|
33 |
def is_stderr = kind == Markup.STDERR
|
|
34 |
def is_system = kind == Markup.SYSTEM
|
|
35 |
def is_status = kind == Markup.STATUS
|
|
36 |
def is_report = kind == Markup.REPORT
|
|
37 |
def is_syslog = is_init || is_exit || is_system || is_stderr
|
|
38 |
|
|
39 |
override def toString: String =
|
|
40 |
{
|
|
41 |
val res =
|
|
42 |
if (is_status || is_report) message.body.map(_.toString).mkString
|
|
43 |
else Pretty.string_of(message.body)
|
|
44 |
if (properties.isEmpty)
|
|
45 |
kind.toString + " [[" + res + "]]"
|
|
46 |
else
|
|
47 |
kind.toString + " " +
|
|
48 |
(for ((x, y) <- properties) yield x + "=" + y).mkString("{", ",", "}") + " [[" + res + "]]"
|
|
49 |
}
|
|
50 |
}
|
|
51 |
|
|
52 |
class Protocol_Output(props: Properties.T, val bytes: Bytes)
|
|
53 |
extends Output(XML.Elem(Markup(Markup.PROTOCOL, props), Nil))
|
|
54 |
{
|
|
55 |
lazy val text: String = bytes.toString
|
|
56 |
}
|
|
57 |
}
|
|
58 |
|
56387
|
59 |
trait Prover
|
|
60 |
{
|
|
61 |
/* text and tree data */
|
|
62 |
|
|
63 |
def encode(s: String): String
|
|
64 |
def decode(s: String): String
|
|
65 |
|
|
66 |
object Encode
|
|
67 |
{
|
|
68 |
val string: XML.Encode.T[String] = (s => XML.Encode.string(encode(s)))
|
|
69 |
}
|
|
70 |
|
|
71 |
def xml_cache: XML.Cache
|
|
72 |
|
|
73 |
|
|
74 |
/* process management */
|
|
75 |
|
|
76 |
def join(): Unit
|
|
77 |
def terminate(): Unit
|
|
78 |
|
|
79 |
def protocol_command_bytes(name: String, args: Bytes*): Unit
|
|
80 |
def protocol_command(name: String, args: String*): Unit
|
|
81 |
|
|
82 |
|
|
83 |
/* PIDE protocol commands */
|
|
84 |
|
|
85 |
def options(opts: Options): Unit
|
|
86 |
|
|
87 |
def define_blob(digest: SHA1.Digest, bytes: Bytes): Unit
|
|
88 |
def define_command(command: Command): Unit
|
|
89 |
|
|
90 |
def discontinue_execution(): Unit
|
|
91 |
def cancel_exec(id: Document_ID.Exec): Unit
|
|
92 |
|
|
93 |
def update(old_id: Document_ID.Version, new_id: Document_ID.Version,
|
|
94 |
edits: List[Document.Edit_Command]): Unit
|
|
95 |
def remove_versions(versions: List[Document.Version]): Unit
|
|
96 |
|
|
97 |
def dialog_result(serial: Long, result: String): Unit
|
|
98 |
}
|
|
99 |
|