wenzelm@36714
|
1 |
/* Title: Pure/PIDE/command.scala
|
wenzelm@36714
|
2 |
Author: Fabian Immler, TU Munich
|
wenzelm@36714
|
3 |
Author: Makarius
|
wenzelm@36714
|
4 |
|
wenzelm@36714
|
5 |
Prover commands with semantic state.
|
wenzelm@36714
|
6 |
*/
|
wenzelm@34410
|
7 |
|
wenzelm@34874
|
8 |
package isabelle
|
wenzelm@34321
|
9 |
|
wenzelm@34454
|
10 |
|
wenzelm@34640
|
11 |
object Command
|
wenzelm@34640
|
12 |
{
|
wenzelm@38643
|
13 |
/** accumulated results from prover **/
|
wenzelm@38643
|
14 |
|
wenzelm@38644
|
15 |
case class State(
|
wenzelm@38643
|
16 |
val command: Command,
|
wenzelm@38875
|
17 |
val status: List[Markup],
|
wenzelm@38643
|
18 |
val reverse_results: List[XML.Tree],
|
wenzelm@38797
|
19 |
val markup: Markup_Tree)
|
wenzelm@38643
|
20 |
{
|
wenzelm@38643
|
21 |
/* content */
|
wenzelm@38643
|
22 |
|
wenzelm@38644
|
23 |
lazy val results = reverse_results.reverse
|
wenzelm@38643
|
24 |
|
wenzelm@38962
|
25 |
def add_status(st: Markup): State = copy(status = st :: status)
|
wenzelm@38962
|
26 |
def add_markup(info: Text.Info[Any]): State = copy(markup = markup + info)
|
wenzelm@38644
|
27 |
def add_result(result: XML.Tree): State = copy(reverse_results = result :: reverse_results)
|
wenzelm@38643
|
28 |
|
wenzelm@38946
|
29 |
def root_info: Text.Info[Any] =
|
wenzelm@38875
|
30 |
new Text.Info(command.range,
|
wenzelm@38946
|
31 |
XML.Elem(Markup(Markup.STATUS, Nil), status.reverse.map(XML.Elem(_, Nil))))
|
wenzelm@38946
|
32 |
def root_markup: Markup_Tree = markup + root_info
|
wenzelm@38643
|
33 |
|
wenzelm@38643
|
34 |
|
wenzelm@38643
|
35 |
/* message dispatch */
|
wenzelm@38643
|
36 |
|
wenzelm@38643
|
37 |
def accumulate(message: XML.Tree): Command.State =
|
wenzelm@38643
|
38 |
message match {
|
wenzelm@38962
|
39 |
case XML.Elem(Markup(Markup.STATUS, _), msgs) =>
|
wenzelm@38962
|
40 |
(this /: msgs)((state, msg) =>
|
wenzelm@38962
|
41 |
msg match {
|
wenzelm@38962
|
42 |
case XML.Elem(markup, Nil) => state.add_status(markup)
|
wenzelm@38962
|
43 |
case _ => System.err.println("Ignored status message: " + msg); state
|
wenzelm@38962
|
44 |
})
|
wenzelm@38875
|
45 |
|
wenzelm@38866
|
46 |
case XML.Elem(Markup(Markup.REPORT, _), msgs) =>
|
wenzelm@38866
|
47 |
(this /: msgs)((state, msg) =>
|
wenzelm@38866
|
48 |
msg match {
|
wenzelm@38996
|
49 |
case XML.Elem(Markup(name, atts @ Position.Range(range)), args)
|
wenzelm@38996
|
50 |
if Position.Id.unapply(atts) == Some(command.id) =>
|
wenzelm@38996
|
51 |
val props = atts.filterNot(p => Markup.POSITION_PROPERTIES(p._1))
|
wenzelm@38996
|
52 |
val info =
|
wenzelm@38996
|
53 |
Text.Info[Any](command.decode(range), XML.Elem(Markup(name, props), args))
|
wenzelm@38996
|
54 |
state.add_markup(info)
|
wenzelm@38866
|
55 |
case _ => System.err.println("Ignored report message: " + msg); state
|
wenzelm@38643
|
56 |
})
|
wenzelm@38643
|
57 |
case _ => add_result(message)
|
wenzelm@38643
|
58 |
}
|
wenzelm@38643
|
59 |
}
|
wenzelm@38649
|
60 |
|
wenzelm@38649
|
61 |
|
wenzelm@38649
|
62 |
/* unparsed dummy commands */
|
wenzelm@38649
|
63 |
|
wenzelm@38649
|
64 |
def unparsed(source: String) =
|
wenzelm@38649
|
65 |
new Command(Document.NO_ID, List(Token(Token.Kind.UNPARSED, source)))
|
wenzelm@34321
|
66 |
}
|
wenzelm@34321
|
67 |
|
wenzelm@38643
|
68 |
|
wenzelm@34700
|
69 |
class Command(
|
wenzelm@38453
|
70 |
val id: Document.Command_ID,
|
wenzelm@38655
|
71 |
val span: List[Token])
|
wenzelm@34454
|
72 |
{
|
wenzelm@34862
|
73 |
/* classification */
|
wenzelm@34503
|
74 |
|
wenzelm@36036
|
75 |
def is_command: Boolean = !span.isEmpty && span.head.is_command
|
wenzelm@34868
|
76 |
def is_ignored: Boolean = span.forall(_.is_ignored)
|
wenzelm@34862
|
77 |
def is_malformed: Boolean = !is_command && !is_ignored
|
wenzelm@34498
|
78 |
|
wenzelm@38649
|
79 |
def is_unparsed = id == Document.NO_ID
|
wenzelm@38649
|
80 |
|
wenzelm@36036
|
81 |
def name: String = if (is_command) span.head.content else ""
|
wenzelm@37138
|
82 |
override def toString =
|
wenzelm@37475
|
83 |
id + "/" + (if (is_command) name else if (is_ignored) "IGNORED" else "MALFORMED")
|
immler@34399
|
84 |
|
wenzelm@34858
|
85 |
|
wenzelm@34862
|
86 |
/* source text */
|
wenzelm@34862
|
87 |
|
wenzelm@34862
|
88 |
val source: String = span.map(_.source).mkString
|
wenzelm@38685
|
89 |
def source(range: Text.Range): String = source.substring(range.start, range.stop)
|
wenzelm@34862
|
90 |
def length: Int = source.length
|
wenzelm@38866
|
91 |
|
wenzelm@38797
|
92 |
val range: Text.Range = Text.Range(0, length)
|
wenzelm@34862
|
93 |
|
wenzelm@34862
|
94 |
lazy val symbol_index = new Symbol.Index(source)
|
wenzelm@38873
|
95 |
def decode(i: Text.Offset): Text.Offset = symbol_index.decode(i)
|
wenzelm@38873
|
96 |
def decode(r: Text.Range): Text.Range = symbol_index.decode(r)
|
wenzelm@38652
|
97 |
|
wenzelm@38652
|
98 |
|
wenzelm@38652
|
99 |
/* accumulated results */
|
wenzelm@38652
|
100 |
|
wenzelm@38797
|
101 |
val empty_state: Command.State = Command.State(this, Nil, Nil, Markup_Tree.empty)
|
immler@34679
|
102 |
}
|