author | wenzelm |
Fri, 14 Dec 2012 12:16:08 +0100 | |
changeset 50508 | 5b7150395568 |
parent 50507 | 9605b0d93d1e |
child 50540 | f4aac67a6405 |
permissions | -rw-r--r-- |
36676 | 1 |
/* Title: Pure/PIDE/command.scala |
2 |
Author: Fabian Immler, TU Munich |
|
3 |
Author: Makarius |
|
4 |
||
5 |
Prover commands with semantic state. |
|
6 |
*/ |
|
34407 | 7 |
|
34871
e596a0b71f3c
incorporate "proofdocument" part into main Isabelle/Pure.jar -- except for html_panel.scala, which depends on external library (Lobo/Cobra browser);
wenzelm
parents:
34865
diff
changeset
|
8 |
package isabelle |
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
9 |
|
43520
cec9b95fa35d
explicit import java.lang.System to prevent odd scope problems;
wenzelm
parents:
40572
diff
changeset
|
10 |
import java.lang.System |
34451 | 11 |
|
45644 | 12 |
import scala.collection.mutable |
38872 | 13 |
import scala.collection.immutable.SortedMap |
14 |
||
15 |
||
34637 | 16 |
object Command |
17 |
{ |
|
38361 | 18 |
/** accumulated results from prover **/ |
19 |
||
50507 | 20 |
/* results */ |
21 |
||
22 |
object Results |
|
23 |
{ |
|
24 |
val empty = new Results(SortedMap.empty) |
|
25 |
def merge(rs: Iterable[Results]): Results = (empty /: rs.iterator)(_ ++ _) |
|
26 |
} |
|
27 |
||
50508
5b7150395568
tuned implementation according to Library.insert/merge in ML;
wenzelm
parents:
50507
diff
changeset
|
28 |
final class Results private(rep: SortedMap[Long, XML.Tree]) |
50507 | 29 |
{ |
30 |
def defined(serial: Long): Boolean = rep.isDefinedAt(serial) |
|
31 |
def get(serial: Long): Option[XML.Tree] = rep.get(serial) |
|
32 |
def entries: Iterator[(Long, XML.Tree)] = rep.iterator |
|
50508
5b7150395568
tuned implementation according to Library.insert/merge in ML;
wenzelm
parents:
50507
diff
changeset
|
33 |
|
5b7150395568
tuned implementation according to Library.insert/merge in ML;
wenzelm
parents:
50507
diff
changeset
|
34 |
def + (entry: (Long, XML.Tree)): Results = |
5b7150395568
tuned implementation according to Library.insert/merge in ML;
wenzelm
parents:
50507
diff
changeset
|
35 |
if (defined(entry._1)) this |
5b7150395568
tuned implementation according to Library.insert/merge in ML;
wenzelm
parents:
50507
diff
changeset
|
36 |
else new Results(rep + entry) |
5b7150395568
tuned implementation according to Library.insert/merge in ML;
wenzelm
parents:
50507
diff
changeset
|
37 |
|
5b7150395568
tuned implementation according to Library.insert/merge in ML;
wenzelm
parents:
50507
diff
changeset
|
38 |
def ++ (other: Results): Results = |
5b7150395568
tuned implementation according to Library.insert/merge in ML;
wenzelm
parents:
50507
diff
changeset
|
39 |
if (this eq other) this |
5b7150395568
tuned implementation according to Library.insert/merge in ML;
wenzelm
parents:
50507
diff
changeset
|
40 |
else if (rep.isEmpty) other |
5b7150395568
tuned implementation according to Library.insert/merge in ML;
wenzelm
parents:
50507
diff
changeset
|
41 |
else (this /: other.entries)(_ + _) |
50507 | 42 |
} |
43 |
||
44 |
||
45 |
/* state */ |
|
50501
6f41f1646617
more careful handling of Dialog_Result, with active area and color feedback;
wenzelm
parents:
50500
diff
changeset
|
46 |
|
43714 | 47 |
sealed case class State( |
50501
6f41f1646617
more careful handling of Dialog_Result, with active area and color feedback;
wenzelm
parents:
50500
diff
changeset
|
48 |
command: Command, |
6f41f1646617
more careful handling of Dialog_Result, with active area and color feedback;
wenzelm
parents:
50500
diff
changeset
|
49 |
status: List[Markup] = Nil, |
50507 | 50 |
results: Results = Results.empty, |
50501
6f41f1646617
more careful handling of Dialog_Result, with active area and color feedback;
wenzelm
parents:
50500
diff
changeset
|
51 |
markup: Markup_Tree = Markup_Tree.empty) |
38361 | 52 |
{ |
49645 | 53 |
def markup_to_XML(filter: XML.Elem => Boolean): XML.Body = |
54 |
markup.to_XML(command.range, command.source, filter) |
|
49614 | 55 |
|
56 |
||
46152
793cecd4ffc0
accumulate status as regular markup for command range;
wenzelm
parents:
45709
diff
changeset
|
57 |
/* accumulate content */ |
38361 | 58 |
|
46152
793cecd4ffc0
accumulate status as regular markup for command range;
wenzelm
parents:
45709
diff
changeset
|
59 |
private def add_status(st: Markup): State = copy(status = st :: status) |
793cecd4ffc0
accumulate status as regular markup for command range;
wenzelm
parents:
45709
diff
changeset
|
60 |
private def add_markup(m: Text.Markup): State = copy(markup = markup + m) |
38361 | 61 |
|
49527 | 62 |
def + (alt_id: Document.ID, message: XML.Elem): Command.State = |
38361 | 63 |
message match { |
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
50163
diff
changeset
|
64 |
case XML.Elem(Markup(Markup.STATUS, _), msgs) => |
38714 | 65 |
(this /: msgs)((state, msg) => |
66 |
msg match { |
|
46152
793cecd4ffc0
accumulate status as regular markup for command range;
wenzelm
parents:
45709
diff
changeset
|
67 |
case elem @ XML.Elem(markup, Nil) => |
50499
f496b2b7bafb
rendering of selected dialog_result as active_result_color, depending on dynamic command status in output panel, but not static popups etc.;
wenzelm
parents:
50201
diff
changeset
|
68 |
state.add_status(markup) |
f496b2b7bafb
rendering of selected dialog_result as active_result_color, depending on dynamic command status in output panel, but not static popups etc.;
wenzelm
parents:
50201
diff
changeset
|
69 |
.add_markup(Text.Info(command.proper_range, elem)) // FIXME cumulation order!? |
46152
793cecd4ffc0
accumulate status as regular markup for command range;
wenzelm
parents:
45709
diff
changeset
|
70 |
|
38714 | 71 |
case _ => System.err.println("Ignored status message: " + msg); state |
72 |
}) |
|
38581
d503a0912e14
simplified Command.status again, reverting most of e5eed57913d0 (note that more complex information can be represented with full markup reports);
wenzelm
parents:
38579
diff
changeset
|
73 |
|
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
50163
diff
changeset
|
74 |
case XML.Elem(Markup(Markup.REPORT, _), msgs) => |
38572
0fe2c01ef7da
Command.State: accumulate markup reports uniformly;
wenzelm
parents:
38564
diff
changeset
|
75 |
(this /: msgs)((state, msg) => |
0fe2c01ef7da
Command.State: accumulate markup reports uniformly;
wenzelm
parents:
38564
diff
changeset
|
76 |
msg match { |
39173
ed3946086358
Command.State.accumulate: check actual source range;
wenzelm
parents:
39172
diff
changeset
|
77 |
case XML.Elem(Markup(name, atts @ Position.Id_Range(id, raw_range)), args) |
49527 | 78 |
if (id == command.id || id == alt_id) && |
79 |
command.range.contains(command.decode(raw_range)) => |
|
39173
ed3946086358
Command.State.accumulate: check actual source range;
wenzelm
parents:
39172
diff
changeset
|
80 |
val range = command.decode(raw_range) |
38872 | 81 |
val props = Position.purge(atts) |
45455 | 82 |
val info: Text.Markup = Text.Info(range, XML.Elem(Markup(name, props), args)) |
38723 | 83 |
state.add_markup(info) |
49526
6d1465c00f2e
more restrictive pattern, to avoid malformed positions intruding the command range (cf. d7a1973b063c);
wenzelm
parents:
49493
diff
changeset
|
84 |
case XML.Elem(Markup(name, atts), args) |
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
50163
diff
changeset
|
85 |
if !atts.exists({ case (a, _) => Markup.POSITION_PROPERTIES(a) }) => |
49037
d7a1973b063c
more markup for failed goal forks, reusing "bad";
wenzelm
parents:
48922
diff
changeset
|
86 |
val range = command.proper_range |
d7a1973b063c
more markup for failed goal forks, reusing "bad";
wenzelm
parents:
48922
diff
changeset
|
87 |
val props = Position.purge(atts) |
d7a1973b063c
more markup for failed goal forks, reusing "bad";
wenzelm
parents:
48922
diff
changeset
|
88 |
val info: Text.Markup = Text.Info(range, XML.Elem(Markup(name, props), args)) |
d7a1973b063c
more markup for failed goal forks, reusing "bad";
wenzelm
parents:
48922
diff
changeset
|
89 |
state.add_markup(info) |
40572 | 90 |
case _ => |
91 |
// FIXME System.err.println("Ignored report message: " + msg) |
|
92 |
state |
|
38361 | 93 |
}) |
38872 | 94 |
case XML.Elem(Markup(name, atts), body) => |
95 |
atts match { |
|
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
50163
diff
changeset
|
96 |
case Markup.Serial(i) => |
50163
c62ce309dc26
more abstract Sendback operations, with explicit id/exec_id properties;
wenzelm
parents:
50158
diff
changeset
|
97 |
val props = Position.purge(atts) |
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
50163
diff
changeset
|
98 |
val message1 = XML.Elem(Markup(Markup.message(name), props), body) |
50163
c62ce309dc26
more abstract Sendback operations, with explicit id/exec_id properties;
wenzelm
parents:
50158
diff
changeset
|
99 |
val message2 = XML.Elem(Markup(name, props), body) |
c62ce309dc26
more abstract Sendback operations, with explicit id/exec_id properties;
wenzelm
parents:
50158
diff
changeset
|
100 |
|
c62ce309dc26
more abstract Sendback operations, with explicit id/exec_id properties;
wenzelm
parents:
50158
diff
changeset
|
101 |
val st0 = copy(results = results + (i -> message1)) |
39441
4110cc1b8f9f
allow embedded reports in regular prover messages, to avoid side-effects for errors for example;
wenzelm
parents:
39173
diff
changeset
|
102 |
val st1 = |
50500
c94bba7906d2
identify dialogs via official serial and maintain as result message;
wenzelm
parents:
50499
diff
changeset
|
103 |
if (Protocol.is_inlined(message)) |
45709
87017fcbad83
clarified modules (again) -- NB: both Document and Protocol are specific to this particular prover;
wenzelm
parents:
45672
diff
changeset
|
104 |
(st0 /: Protocol.message_positions(command, message))( |
50163
c62ce309dc26
more abstract Sendback operations, with explicit id/exec_id properties;
wenzelm
parents:
50158
diff
changeset
|
105 |
(st, range) => st.add_markup(Text.Info(range, message2))) |
50500
c94bba7906d2
identify dialogs via official serial and maintain as result message;
wenzelm
parents:
50499
diff
changeset
|
106 |
else st0 |
49445
638cefe3ee99
earlier treatment of embedded report/no_report messages (see also 4110cc1b8f9f);
wenzelm
parents:
49418
diff
changeset
|
107 |
|
638cefe3ee99
earlier treatment of embedded report/no_report messages (see also 4110cc1b8f9f);
wenzelm
parents:
49418
diff
changeset
|
108 |
st1 |
38872 | 109 |
case _ => System.err.println("Ignored message without serial number: " + message); this |
110 |
} |
|
38361 | 111 |
} |
112 |
} |
|
38367 | 113 |
|
114 |
||
45644 | 115 |
/* make commands */ |
116 |
||
48745 | 117 |
type Span = List[Token] |
118 |
||
50501
6f41f1646617
more careful handling of Dialog_Result, with active area and color feedback;
wenzelm
parents:
50500
diff
changeset
|
119 |
def apply(id: Document.Command_ID, node_name: Document.Node.Name, span: Span, |
50507 | 120 |
results: Results = Results.empty, markup: Markup_Tree = Markup_Tree.empty): Command = |
45644 | 121 |
{ |
122 |
val source: String = |
|
48745 | 123 |
span match { |
45644 | 124 |
case List(tok) => tok.source |
48745 | 125 |
case _ => span.map(_.source).mkString |
45644 | 126 |
} |
127 |
||
48745 | 128 |
val span1 = new mutable.ListBuffer[Token] |
45644 | 129 |
var i = 0 |
48745 | 130 |
for (Token(kind, s) <- span) { |
45644 | 131 |
val n = s.length |
132 |
val s1 = source.substring(i, i + n) |
|
48745 | 133 |
span1 += Token(kind, s1) |
45644 | 134 |
i += n |
135 |
} |
|
136 |
||
50501
6f41f1646617
more careful handling of Dialog_Result, with active area and color feedback;
wenzelm
parents:
50500
diff
changeset
|
137 |
new Command(id, node_name, span1.toList, source, results, markup) |
45644 | 138 |
} |
139 |
||
50501
6f41f1646617
more careful handling of Dialog_Result, with active area and color feedback;
wenzelm
parents:
50500
diff
changeset
|
140 |
val empty = Command(Document.no_id, Document.Node.Name.empty, Nil) |
49414 | 141 |
|
50501
6f41f1646617
more careful handling of Dialog_Result, with active area and color feedback;
wenzelm
parents:
50500
diff
changeset
|
142 |
def unparsed(id: Document.Command_ID, source: String, results: Results, markup: Markup_Tree) |
6f41f1646617
more careful handling of Dialog_Result, with active area and color feedback;
wenzelm
parents:
50500
diff
changeset
|
143 |
: Command = |
6f41f1646617
more careful handling of Dialog_Result, with active area and color feedback;
wenzelm
parents:
50500
diff
changeset
|
144 |
Command(id, Document.Node.Name.empty, List(Token(Token.Kind.UNPARSED, source)), results, markup) |
49414 | 145 |
|
50501
6f41f1646617
more careful handling of Dialog_Result, with active area and color feedback;
wenzelm
parents:
50500
diff
changeset
|
146 |
def unparsed(source: String): Command = |
50507 | 147 |
unparsed(Document.no_id, source, Results.empty, Markup_Tree.empty) |
44384 | 148 |
|
50501
6f41f1646617
more careful handling of Dialog_Result, with active area and color feedback;
wenzelm
parents:
50500
diff
changeset
|
149 |
def rich_text(id: Document.Command_ID, results: Results, body: XML.Body): Command = |
49414 | 150 |
{ |
49466 | 151 |
val text = XML.content(body) |
152 |
val markup = Markup_Tree.from_XML(body) |
|
50501
6f41f1646617
more careful handling of Dialog_Result, with active area and color feedback;
wenzelm
parents:
50500
diff
changeset
|
153 |
unparsed(id, text, results, markup) |
49414 | 154 |
} |
49359
c1262d7389fb
refined output panel: more value-oriented approach to update and caret focus;
wenzelm
parents:
49037
diff
changeset
|
155 |
|
44384 | 156 |
|
157 |
/* perspective */ |
|
158 |
||
44474 | 159 |
object Perspective |
160 |
{ |
|
161 |
val empty: Perspective = Perspective(Nil) |
|
162 |
} |
|
44385
e7fdb008aa7d
propagate editor perspective through document model;
wenzelm
parents:
44384
diff
changeset
|
163 |
|
44474 | 164 |
sealed case class Perspective(commands: List[Command]) // visible commands in canonical order |
44385
e7fdb008aa7d
propagate editor perspective through document model;
wenzelm
parents:
44384
diff
changeset
|
165 |
{ |
44474 | 166 |
def same(that: Perspective): Boolean = |
167 |
{ |
|
168 |
val cmds1 = this.commands |
|
169 |
val cmds2 = that.commands |
|
48754
c2c1e5944536
clarified undefined, unparsed, unfinished command spans;
wenzelm
parents:
48745
diff
changeset
|
170 |
require(!cmds1.exists(_.is_undefined)) |
c2c1e5944536
clarified undefined, unparsed, unfinished command spans;
wenzelm
parents:
48745
diff
changeset
|
171 |
require(!cmds2.exists(_.is_undefined)) |
44474 | 172 |
cmds1.length == cmds2.length && |
173 |
(cmds1.iterator zip cmds2.iterator).forall({ case (c1, c2) => c1.id == c2.id }) |
|
174 |
} |
|
44385
e7fdb008aa7d
propagate editor perspective through document model;
wenzelm
parents:
44384
diff
changeset
|
175 |
} |
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
176 |
} |
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
177 |
|
38361 | 178 |
|
46712 | 179 |
final class Command private( |
38150
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
37373
diff
changeset
|
180 |
val id: Document.Command_ID, |
44615 | 181 |
val node_name: Document.Node.Name, |
48745 | 182 |
val span: Command.Span, |
49414 | 183 |
val source: String, |
50501
6f41f1646617
more careful handling of Dialog_Result, with active area and color feedback;
wenzelm
parents:
50500
diff
changeset
|
184 |
val init_results: Command.Results, |
49414 | 185 |
val init_markup: Markup_Tree) |
34451 | 186 |
{ |
34859 | 187 |
/* classification */ |
34500
384427c750c8
state_results: separate buffer for messages from running command;
wenzelm
parents:
34497
diff
changeset
|
188 |
|
48754
c2c1e5944536
clarified undefined, unparsed, unfinished command spans;
wenzelm
parents:
48745
diff
changeset
|
189 |
def is_undefined: Boolean = id == Document.no_id |
c2c1e5944536
clarified undefined, unparsed, unfinished command spans;
wenzelm
parents:
48745
diff
changeset
|
190 |
val is_unparsed: Boolean = span.exists(_.is_unparsed) |
c2c1e5944536
clarified undefined, unparsed, unfinished command spans;
wenzelm
parents:
48745
diff
changeset
|
191 |
val is_unfinished: Boolean = span.exists(_.is_unfinished) |
44385
e7fdb008aa7d
propagate editor perspective through document model;
wenzelm
parents:
44384
diff
changeset
|
192 |
|
48599 | 193 |
val is_ignored: Boolean = !span.exists(_.is_proper) |
48754
c2c1e5944536
clarified undefined, unparsed, unfinished command spans;
wenzelm
parents:
48745
diff
changeset
|
194 |
val is_malformed: Boolean = !is_ignored && (!span.head.is_command || span.exists(_.is_error)) |
47012
0e246130486b
clarified command span classification: strict Command.is_command, permissive Command.name;
wenzelm
parents:
46910
diff
changeset
|
195 |
def is_command: Boolean = !is_ignored && !is_malformed |
34859 | 196 |
|
47012
0e246130486b
clarified command span classification: strict Command.is_command, permissive Command.name;
wenzelm
parents:
46910
diff
changeset
|
197 |
def name: String = |
48718 | 198 |
span.find(_.is_command) match { case Some(tok) => tok.source case _ => "" } |
47012
0e246130486b
clarified command span classification: strict Command.is_command, permissive Command.name;
wenzelm
parents:
46910
diff
changeset
|
199 |
|
37129 | 200 |
override def toString = |
37373
25078ba44436
tuned Command.toString -- preserving uniqueness allows the Scala toplevel to print Linear_Set[Command] results without crashing;
wenzelm
parents:
37197
diff
changeset
|
201 |
id + "/" + (if (is_command) name else if (is_ignored) "IGNORED" else "MALFORMED") |
34495 | 202 |
|
34859 | 203 |
|
204 |
/* source text */ |
|
34451 | 205 |
|
46813 | 206 |
def length: Int = source.length |
207 |
val range: Text.Range = Text.Range(0, length) |
|
208 |
||
209 |
val proper_range: Text.Range = |
|
47459
373e456149cc
include trailing comments in proper_command range;
wenzelm
parents:
47012
diff
changeset
|
210 |
Text.Range(0, (length /: span.reverse.iterator.takeWhile(_.is_space))(_ - _.source.length)) |
46813 | 211 |
|
38426 | 212 |
def source(range: Text.Range): String = source.substring(range.start, range.stop) |
38572
0fe2c01ef7da
Command.State: accumulate markup reports uniformly;
wenzelm
parents:
38564
diff
changeset
|
213 |
|
34859 | 214 |
lazy val symbol_index = new Symbol.Index(source) |
38579 | 215 |
def decode(i: Text.Offset): Text.Offset = symbol_index.decode(i) |
216 |
def decode(r: Text.Range): Text.Range = symbol_index.decode(r) |
|
38370
8b15d0f98962
explicit Document.State value, instead of individual state variables in Session, Command, Document;
wenzelm
parents:
38367
diff
changeset
|
217 |
|
8b15d0f98962
explicit Document.State value, instead of individual state variables in Session, Command, Document;
wenzelm
parents:
38367
diff
changeset
|
218 |
|
8b15d0f98962
explicit Document.State value, instead of individual state variables in Session, Command, Document;
wenzelm
parents:
38367
diff
changeset
|
219 |
/* accumulated results */ |
8b15d0f98962
explicit Document.State value, instead of individual state variables in Session, Command, Document;
wenzelm
parents:
38367
diff
changeset
|
220 |
|
50501
6f41f1646617
more careful handling of Dialog_Result, with active area and color feedback;
wenzelm
parents:
50500
diff
changeset
|
221 |
val init_state: Command.State = |
6f41f1646617
more careful handling of Dialog_Result, with active area and color feedback;
wenzelm
parents:
50500
diff
changeset
|
222 |
Command.State(this, results = init_results, markup = init_markup) |
34676
9e725d34df7b
Command and Command_State handle results from prover as Accumulator
immler@in.tum.de
parents:
34675
diff
changeset
|
223 |
} |