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@44400
|
10 |
import java.lang.System
|
wenzelm@34454
|
11 |
|
wenzelm@46515
|
12 |
import scala.collection.mutable
|
wenzelm@39198
|
13 |
import scala.collection.immutable.SortedMap
|
wenzelm@39198
|
14 |
|
wenzelm@39198
|
15 |
|
wenzelm@34640
|
16 |
object Command
|
wenzelm@34640
|
17 |
{
|
wenzelm@38643
|
18 |
/** accumulated results from prover **/
|
wenzelm@38643
|
19 |
|
wenzelm@51522
|
20 |
/* results */
|
wenzelm@51522
|
21 |
|
wenzelm@51522
|
22 |
object Results
|
wenzelm@51522
|
23 |
{
|
wenzelm@51522
|
24 |
val empty = new Results(SortedMap.empty)
|
wenzelm@51522
|
25 |
def merge(rs: Iterable[Results]): Results = (empty /: rs.iterator)(_ ++ _)
|
wenzelm@51522
|
26 |
}
|
wenzelm@51522
|
27 |
|
wenzelm@51523
|
28 |
final class Results private(rep: SortedMap[Long, XML.Tree])
|
wenzelm@51522
|
29 |
{
|
wenzelm@51522
|
30 |
def defined(serial: Long): Boolean = rep.isDefinedAt(serial)
|
wenzelm@51522
|
31 |
def get(serial: Long): Option[XML.Tree] = rep.get(serial)
|
wenzelm@51522
|
32 |
def entries: Iterator[(Long, XML.Tree)] = rep.iterator
|
wenzelm@51523
|
33 |
|
wenzelm@51523
|
34 |
def + (entry: (Long, XML.Tree)): Results =
|
wenzelm@51523
|
35 |
if (defined(entry._1)) this
|
wenzelm@51523
|
36 |
else new Results(rep + entry)
|
wenzelm@51523
|
37 |
|
wenzelm@51523
|
38 |
def ++ (other: Results): Results =
|
wenzelm@51523
|
39 |
if (this eq other) this
|
wenzelm@51523
|
40 |
else if (rep.isEmpty) other
|
wenzelm@51523
|
41 |
else (this /: other.entries)(_ + _)
|
wenzelm@51555
|
42 |
|
wenzelm@51555
|
43 |
override def toString: String = entries.mkString("Results(", ", ", ")")
|
wenzelm@51522
|
44 |
}
|
wenzelm@51522
|
45 |
|
wenzelm@51522
|
46 |
|
wenzelm@51522
|
47 |
/* state */
|
wenzelm@51516
|
48 |
|
wenzelm@44596
|
49 |
sealed case class State(
|
wenzelm@51516
|
50 |
command: Command,
|
wenzelm@51516
|
51 |
status: List[Markup] = Nil,
|
wenzelm@51522
|
52 |
results: Results = Results.empty,
|
wenzelm@51516
|
53 |
markup: Markup_Tree = Markup_Tree.empty)
|
wenzelm@38643
|
54 |
{
|
wenzelm@50660
|
55 |
def markup_to_XML(filter: XML.Elem => Boolean): XML.Body =
|
wenzelm@50660
|
56 |
markup.to_XML(command.range, command.source, filter)
|
wenzelm@50629
|
57 |
|
wenzelm@50629
|
58 |
|
wenzelm@47023
|
59 |
/* accumulate content */
|
wenzelm@38643
|
60 |
|
wenzelm@47023
|
61 |
private def add_status(st: Markup): State = copy(status = st :: status)
|
wenzelm@47023
|
62 |
private def add_markup(m: Text.Markup): State = copy(markup = markup + m)
|
wenzelm@38643
|
63 |
|
wenzelm@50542
|
64 |
def + (alt_id: Document.ID, message: XML.Elem): Command.State =
|
wenzelm@38643
|
65 |
message match {
|
wenzelm@51216
|
66 |
case XML.Elem(Markup(Markup.STATUS, _), msgs) =>
|
wenzelm@38962
|
67 |
(this /: msgs)((state, msg) =>
|
wenzelm@38962
|
68 |
msg match {
|
wenzelm@47023
|
69 |
case elem @ XML.Elem(markup, Nil) =>
|
wenzelm@51514
|
70 |
state.add_status(markup)
|
wenzelm@51514
|
71 |
.add_markup(Text.Info(command.proper_range, elem)) // FIXME cumulation order!?
|
wenzelm@47023
|
72 |
|
wenzelm@38962
|
73 |
case _ => System.err.println("Ignored status message: " + msg); state
|
wenzelm@38962
|
74 |
})
|
wenzelm@38875
|
75 |
|
wenzelm@51216
|
76 |
case XML.Elem(Markup(Markup.REPORT, _), msgs) =>
|
wenzelm@38866
|
77 |
(this /: msgs)((state, msg) =>
|
wenzelm@38866
|
78 |
msg match {
|
wenzelm@39454
|
79 |
case XML.Elem(Markup(name, atts @ Position.Id_Range(id, raw_range)), args)
|
wenzelm@50542
|
80 |
if (id == command.id || id == alt_id) &&
|
wenzelm@50542
|
81 |
command.range.contains(command.decode(raw_range)) =>
|
wenzelm@39454
|
82 |
val range = command.decode(raw_range)
|
wenzelm@39198
|
83 |
val props = Position.purge(atts)
|
wenzelm@46331
|
84 |
val info: Text.Markup = Text.Info(range, XML.Elem(Markup(name, props), args))
|
wenzelm@38996
|
85 |
state.add_markup(info)
|
wenzelm@50541
|
86 |
case XML.Elem(Markup(name, atts), args)
|
wenzelm@51216
|
87 |
if !atts.exists({ case (a, _) => Markup.POSITION_PROPERTIES(a) }) =>
|
wenzelm@50052
|
88 |
val range = command.proper_range
|
wenzelm@50052
|
89 |
val props = Position.purge(atts)
|
wenzelm@50052
|
90 |
val info: Text.Markup = Text.Info(range, XML.Elem(Markup(name, props), args))
|
wenzelm@50052
|
91 |
state.add_markup(info)
|
wenzelm@40830
|
92 |
case _ =>
|
wenzelm@40830
|
93 |
// FIXME System.err.println("Ignored report message: " + msg)
|
wenzelm@40830
|
94 |
state
|
wenzelm@38643
|
95 |
})
|
wenzelm@39198
|
96 |
case XML.Elem(Markup(name, atts), body) =>
|
wenzelm@39198
|
97 |
atts match {
|
wenzelm@51216
|
98 |
case Markup.Serial(i) =>
|
wenzelm@51178
|
99 |
val props = Position.purge(atts)
|
wenzelm@51216
|
100 |
val message1 = XML.Elem(Markup(Markup.message(name), props), body)
|
wenzelm@51178
|
101 |
val message2 = XML.Elem(Markup(name, props), body)
|
wenzelm@51178
|
102 |
|
wenzelm@51178
|
103 |
val st0 = copy(results = results + (i -> message1))
|
wenzelm@39750
|
104 |
val st1 =
|
wenzelm@51515
|
105 |
if (Protocol.is_inlined(message))
|
wenzelm@46587
|
106 |
(st0 /: Protocol.message_positions(command, message))(
|
wenzelm@51178
|
107 |
(st, range) => st.add_markup(Text.Info(range, message2)))
|
wenzelm@51515
|
108 |
else st0
|
wenzelm@50460
|
109 |
|
wenzelm@50460
|
110 |
st1
|
wenzelm@39198
|
111 |
case _ => System.err.println("Ignored message without serial number: " + message); this
|
wenzelm@39198
|
112 |
}
|
wenzelm@38643
|
113 |
}
|
wenzelm@38643
|
114 |
}
|
wenzelm@38649
|
115 |
|
wenzelm@38649
|
116 |
|
wenzelm@46515
|
117 |
/* make commands */
|
wenzelm@46515
|
118 |
|
wenzelm@49760
|
119 |
type Span = List[Token]
|
wenzelm@49760
|
120 |
|
wenzelm@51516
|
121 |
def apply(id: Document.Command_ID, node_name: Document.Node.Name, span: Span,
|
wenzelm@51522
|
122 |
results: Results = Results.empty, markup: Markup_Tree = Markup_Tree.empty): Command =
|
wenzelm@46515
|
123 |
{
|
wenzelm@46515
|
124 |
val source: String =
|
wenzelm@49760
|
125 |
span match {
|
wenzelm@46515
|
126 |
case List(tok) => tok.source
|
wenzelm@49760
|
127 |
case _ => span.map(_.source).mkString
|
wenzelm@46515
|
128 |
}
|
wenzelm@46515
|
129 |
|
wenzelm@49760
|
130 |
val span1 = new mutable.ListBuffer[Token]
|
wenzelm@46515
|
131 |
var i = 0
|
wenzelm@49760
|
132 |
for (Token(kind, s) <- span) {
|
wenzelm@46515
|
133 |
val n = s.length
|
wenzelm@46515
|
134 |
val s1 = source.substring(i, i + n)
|
wenzelm@49760
|
135 |
span1 += Token(kind, s1)
|
wenzelm@46515
|
136 |
i += n
|
wenzelm@46515
|
137 |
}
|
wenzelm@46515
|
138 |
|
wenzelm@51516
|
139 |
new Command(id, node_name, span1.toList, source, results, markup)
|
wenzelm@46515
|
140 |
}
|
wenzelm@46515
|
141 |
|
wenzelm@51516
|
142 |
val empty = Command(Document.no_id, Document.Node.Name.empty, Nil)
|
wenzelm@45291
|
143 |
|
wenzelm@51516
|
144 |
def unparsed(id: Document.Command_ID, source: String, results: Results, markup: Markup_Tree)
|
wenzelm@51516
|
145 |
: Command =
|
wenzelm@51516
|
146 |
Command(id, Document.Node.Name.empty, List(Token(Token.Kind.UNPARSED, source)), results, markup)
|
wenzelm@50429
|
147 |
|
wenzelm@51516
|
148 |
def unparsed(source: String): Command =
|
wenzelm@51522
|
149 |
unparsed(Document.no_id, source, Results.empty, Markup_Tree.empty)
|
wenzelm@50429
|
150 |
|
wenzelm@51516
|
151 |
def rich_text(id: Document.Command_ID, results: Results, body: XML.Body): Command =
|
wenzelm@50429
|
152 |
{
|
wenzelm@50481
|
153 |
val text = XML.content(body)
|
wenzelm@50481
|
154 |
val markup = Markup_Tree.from_XML(body)
|
wenzelm@51516
|
155 |
unparsed(id, text, results, markup)
|
wenzelm@50429
|
156 |
}
|
wenzelm@50374
|
157 |
|
wenzelm@45291
|
158 |
|
wenzelm@45291
|
159 |
/* perspective */
|
wenzelm@45291
|
160 |
|
wenzelm@45395
|
161 |
object Perspective
|
wenzelm@45395
|
162 |
{
|
wenzelm@45395
|
163 |
val empty: Perspective = Perspective(Nil)
|
wenzelm@45395
|
164 |
}
|
wenzelm@45292
|
165 |
|
wenzelm@45395
|
166 |
sealed case class Perspective(commands: List[Command]) // visible commands in canonical order
|
wenzelm@45292
|
167 |
{
|
wenzelm@45395
|
168 |
def same(that: Perspective): Boolean =
|
wenzelm@45395
|
169 |
{
|
wenzelm@45395
|
170 |
val cmds1 = this.commands
|
wenzelm@45395
|
171 |
val cmds2 = that.commands
|
wenzelm@49769
|
172 |
require(!cmds1.exists(_.is_undefined))
|
wenzelm@49769
|
173 |
require(!cmds2.exists(_.is_undefined))
|
wenzelm@45395
|
174 |
cmds1.length == cmds2.length &&
|
wenzelm@45395
|
175 |
(cmds1.iterator zip cmds2.iterator).forall({ case (c1, c2) => c1.id == c2.id })
|
wenzelm@45395
|
176 |
}
|
wenzelm@45292
|
177 |
}
|
wenzelm@34321
|
178 |
}
|
wenzelm@34321
|
179 |
|
wenzelm@38643
|
180 |
|
wenzelm@47583
|
181 |
final class Command private(
|
wenzelm@38453
|
182 |
val id: Document.Command_ID,
|
wenzelm@45506
|
183 |
val node_name: Document.Node.Name,
|
wenzelm@49760
|
184 |
val span: Command.Span,
|
wenzelm@50429
|
185 |
val source: String,
|
wenzelm@51516
|
186 |
val init_results: Command.Results,
|
wenzelm@50429
|
187 |
val init_markup: Markup_Tree)
|
wenzelm@34454
|
188 |
{
|
wenzelm@34862
|
189 |
/* classification */
|
wenzelm@34503
|
190 |
|
wenzelm@49769
|
191 |
def is_undefined: Boolean = id == Document.no_id
|
wenzelm@49769
|
192 |
val is_unparsed: Boolean = span.exists(_.is_unparsed)
|
wenzelm@49769
|
193 |
val is_unfinished: Boolean = span.exists(_.is_unfinished)
|
wenzelm@45292
|
194 |
|
wenzelm@49614
|
195 |
val is_ignored: Boolean = !span.exists(_.is_proper)
|
wenzelm@49769
|
196 |
val is_malformed: Boolean = !is_ignored && (!span.head.is_command || span.exists(_.is_error))
|
wenzelm@47888
|
197 |
def is_command: Boolean = !is_ignored && !is_malformed
|
wenzelm@34498
|
198 |
|
wenzelm@47888
|
199 |
def name: String =
|
wenzelm@49733
|
200 |
span.find(_.is_command) match { case Some(tok) => tok.source case _ => "" }
|
wenzelm@47888
|
201 |
|
wenzelm@37138
|
202 |
override def toString =
|
wenzelm@37475
|
203 |
id + "/" + (if (is_command) name else if (is_ignored) "IGNORED" else "MALFORMED")
|
immler@34399
|
204 |
|
wenzelm@34858
|
205 |
|
wenzelm@34862
|
206 |
/* source text */
|
wenzelm@34862
|
207 |
|
wenzelm@47684
|
208 |
def length: Int = source.length
|
wenzelm@47684
|
209 |
val range: Text.Range = Text.Range(0, length)
|
wenzelm@47684
|
210 |
|
wenzelm@47684
|
211 |
val proper_range: Text.Range =
|
wenzelm@52016
|
212 |
Text.Range(0, (length /: span.reverse.iterator.takeWhile(_.is_improper))(_ - _.source.length))
|
wenzelm@47684
|
213 |
|
wenzelm@38685
|
214 |
def source(range: Text.Range): String = source.substring(range.start, range.stop)
|
wenzelm@38866
|
215 |
|
wenzelm@34862
|
216 |
lazy val symbol_index = new Symbol.Index(source)
|
wenzelm@38873
|
217 |
def decode(i: Text.Offset): Text.Offset = symbol_index.decode(i)
|
wenzelm@38873
|
218 |
def decode(r: Text.Range): Text.Range = symbol_index.decode(r)
|
wenzelm@38652
|
219 |
|
wenzelm@38652
|
220 |
|
wenzelm@38652
|
221 |
/* accumulated results */
|
wenzelm@38652
|
222 |
|
wenzelm@51516
|
223 |
val init_state: Command.State =
|
wenzelm@51516
|
224 |
Command.State(this, results = init_results, markup = init_markup)
|
immler@34679
|
225 |
}
|