author | wenzelm |
Mon, 09 Jan 2012 23:08:33 +0100 | |
changeset 46164 | a01c969f2e14 |
parent 46152 | 793cecd4ffc0 |
child 46712 | 8650d9a95736 |
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 |
||
43714 | 20 |
sealed case class State( |
38361 | 21 |
val command: Command, |
38872 | 22 |
val status: List[Markup] = Nil, |
23 |
val results: SortedMap[Long, XML.Tree] = SortedMap.empty, |
|
24 |
val markup: Markup_Tree = Markup_Tree.empty) |
|
38361 | 25 |
{ |
46152
793cecd4ffc0
accumulate status as regular markup for command range;
wenzelm
parents:
45709
diff
changeset
|
26 |
/* accumulate content */ |
38361 | 27 |
|
46152
793cecd4ffc0
accumulate status as regular markup for command range;
wenzelm
parents:
45709
diff
changeset
|
28 |
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
|
29 |
private def add_markup(m: Text.Markup): State = copy(markup = markup + m) |
38361 | 30 |
|
46152
793cecd4ffc0
accumulate status as regular markup for command range;
wenzelm
parents:
45709
diff
changeset
|
31 |
def + (message: XML.Elem): Command.State = |
38361 | 32 |
message match { |
45666 | 33 |
case XML.Elem(Markup(Isabelle_Markup.STATUS, _), msgs) => |
38714 | 34 |
(this /: msgs)((state, msg) => |
35 |
msg match { |
|
46152
793cecd4ffc0
accumulate status as regular markup for command range;
wenzelm
parents:
45709
diff
changeset
|
36 |
case elem @ XML.Elem(markup, Nil) => |
46164 | 37 |
state.add_status(markup).add_markup(Text.Info(command.range, elem)) |
46152
793cecd4ffc0
accumulate status as regular markup for command range;
wenzelm
parents:
45709
diff
changeset
|
38 |
|
38714 | 39 |
case _ => System.err.println("Ignored status message: " + msg); state |
40 |
}) |
|
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
|
41 |
|
45666 | 42 |
case XML.Elem(Markup(Isabelle_Markup.REPORT, _), msgs) => |
38572
0fe2c01ef7da
Command.State: accumulate markup reports uniformly;
wenzelm
parents:
38564
diff
changeset
|
43 |
(this /: msgs)((state, msg) => |
0fe2c01ef7da
Command.State: accumulate markup reports uniformly;
wenzelm
parents:
38564
diff
changeset
|
44 |
msg match { |
39173
ed3946086358
Command.State.accumulate: check actual source range;
wenzelm
parents:
39172
diff
changeset
|
45 |
case XML.Elem(Markup(name, atts @ Position.Id_Range(id, raw_range)), args) |
ed3946086358
Command.State.accumulate: check actual source range;
wenzelm
parents:
39172
diff
changeset
|
46 |
if id == command.id && command.range.contains(command.decode(raw_range)) => |
ed3946086358
Command.State.accumulate: check actual source range;
wenzelm
parents:
39172
diff
changeset
|
47 |
val range = command.decode(raw_range) |
38872 | 48 |
val props = Position.purge(atts) |
45455 | 49 |
val info: Text.Markup = Text.Info(range, XML.Elem(Markup(name, props), args)) |
38723 | 50 |
state.add_markup(info) |
40572 | 51 |
case _ => |
52 |
// FIXME System.err.println("Ignored report message: " + msg) |
|
53 |
state |
|
38361 | 54 |
}) |
38872 | 55 |
case XML.Elem(Markup(name, atts), body) => |
56 |
atts match { |
|
45666 | 57 |
case Isabelle_Markup.Serial(i) => |
38887
1261481ef5e5
Command.State: add reported positions to markup tree, according main message position or Markup.binding/entity/report occurrences in body;
wenzelm
parents:
38877
diff
changeset
|
58 |
val result = XML.Elem(Markup(name, Position.purge(atts)), body) |
46152
793cecd4ffc0
accumulate status as regular markup for command range;
wenzelm
parents:
45709
diff
changeset
|
59 |
val st0 = copy(results = results + (i -> result)) |
39441
4110cc1b8f9f
allow embedded reports in regular prover messages, to avoid side-effects for errors for example;
wenzelm
parents:
39173
diff
changeset
|
60 |
val st1 = |
45709
87017fcbad83
clarified modules (again) -- NB: both Document and Protocol are specific to this particular prover;
wenzelm
parents:
45672
diff
changeset
|
61 |
if (Protocol.is_tracing(message)) st0 |
39622
53365ba766ac
Command.accumulate: refrain from adding tracing messages to markup tree -- potential scalability problem;
wenzelm
parents:
39441
diff
changeset
|
62 |
else |
45709
87017fcbad83
clarified modules (again) -- NB: both Document and Protocol are specific to this particular prover;
wenzelm
parents:
45672
diff
changeset
|
63 |
(st0 /: Protocol.message_positions(command, message))( |
39622
53365ba766ac
Command.accumulate: refrain from adding tracing messages to markup tree -- potential scalability problem;
wenzelm
parents:
39441
diff
changeset
|
64 |
(st, range) => st.add_markup(Text.Info(range, result))) |
46152
793cecd4ffc0
accumulate status as regular markup for command range;
wenzelm
parents:
45709
diff
changeset
|
65 |
val st2 = (st1 /: Protocol.message_reports(message))(_ + _) |
39622
53365ba766ac
Command.accumulate: refrain from adding tracing messages to markup tree -- potential scalability problem;
wenzelm
parents:
39441
diff
changeset
|
66 |
st2 |
38872 | 67 |
case _ => System.err.println("Ignored message without serial number: " + message); this |
68 |
} |
|
38361 | 69 |
} |
70 |
} |
|
38367 | 71 |
|
72 |
||
45644 | 73 |
/* make commands */ |
74 |
||
75 |
def apply(id: Document.Command_ID, node_name: Document.Node.Name, toks: List[Token]): Command = |
|
76 |
{ |
|
77 |
val source: String = |
|
78 |
toks match { |
|
79 |
case List(tok) => tok.source |
|
80 |
case _ => toks.map(_.source).mkString |
|
81 |
} |
|
82 |
||
83 |
val span = new mutable.ListBuffer[Token] |
|
84 |
var i = 0 |
|
85 |
for (Token(kind, s) <- toks) { |
|
86 |
val n = s.length |
|
87 |
val s1 = source.substring(i, i + n) |
|
88 |
span += Token(kind, s1) |
|
89 |
i += n |
|
90 |
} |
|
91 |
||
92 |
new Command(id, node_name, span.toList, source) |
|
93 |
} |
|
94 |
||
95 |
def apply(node_name: Document.Node.Name, toks: List[Token]): Command = |
|
96 |
Command(Document.no_id, node_name, toks) |
|
38367 | 97 |
|
40454
2516ea25a54b
some support for nested source structure, based on section headings;
wenzelm
parents:
39622
diff
changeset
|
98 |
def unparsed(source: String): Command = |
45644 | 99 |
Command(Document.no_id, Document.Node.Name.empty, List(Token(Token.Kind.UNPARSED, source))) |
44384 | 100 |
|
101 |
||
102 |
/* perspective */ |
|
103 |
||
44474 | 104 |
object Perspective |
105 |
{ |
|
106 |
val empty: Perspective = Perspective(Nil) |
|
107 |
} |
|
44385
e7fdb008aa7d
propagate editor perspective through document model;
wenzelm
parents:
44384
diff
changeset
|
108 |
|
44474 | 109 |
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
|
110 |
{ |
44474 | 111 |
def same(that: Perspective): Boolean = |
112 |
{ |
|
113 |
val cmds1 = this.commands |
|
114 |
val cmds2 = that.commands |
|
115 |
require(cmds1.forall(_.is_defined)) |
|
116 |
require(cmds2.forall(_.is_defined)) |
|
117 |
cmds1.length == cmds2.length && |
|
118 |
(cmds1.iterator zip cmds2.iterator).forall({ case (c1, c2) => c1.id == c2.id }) |
|
119 |
} |
|
44385
e7fdb008aa7d
propagate editor perspective through document model;
wenzelm
parents:
44384
diff
changeset
|
120 |
} |
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
121 |
} |
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
122 |
|
38361 | 123 |
|
45644 | 124 |
class Command private( |
38150
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
37373
diff
changeset
|
125 |
val id: Document.Command_ID, |
44615 | 126 |
val node_name: Document.Node.Name, |
45644 | 127 |
val span: List[Token], |
128 |
val source: String) |
|
34451 | 129 |
{ |
34859 | 130 |
/* classification */ |
34500
384427c750c8
state_results: separate buffer for messages from running command;
wenzelm
parents:
34497
diff
changeset
|
131 |
|
44385
e7fdb008aa7d
propagate editor perspective through document model;
wenzelm
parents:
44384
diff
changeset
|
132 |
def is_defined: Boolean = id != Document.no_id |
e7fdb008aa7d
propagate editor perspective through document model;
wenzelm
parents:
44384
diff
changeset
|
133 |
|
36012 | 134 |
def is_command: Boolean = !span.isEmpty && span.head.is_command |
34865 | 135 |
def is_ignored: Boolean = span.forall(_.is_ignored) |
34859 | 136 |
def is_malformed: Boolean = !is_command && !is_ignored |
137 |
||
36012 | 138 |
def name: String = if (is_command) span.head.content else "" |
37129 | 139 |
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
|
140 |
id + "/" + (if (is_command) name else if (is_ignored) "IGNORED" else "MALFORMED") |
34495 | 141 |
|
34859 | 142 |
|
143 |
/* source text */ |
|
34451 | 144 |
|
38426 | 145 |
def source(range: Text.Range): String = source.substring(range.start, range.stop) |
34859 | 146 |
def length: Int = source.length |
38572
0fe2c01ef7da
Command.State: accumulate markup reports uniformly;
wenzelm
parents:
38564
diff
changeset
|
147 |
|
38877 | 148 |
val newlines = |
149 |
(0 /: Symbol.iterator(source)) { |
|
150 |
case (n, s) => if (Symbol.is_physical_newline(s)) n + 1 else n } |
|
151 |
||
38479
e628da370072
more efficient Markup_Tree, based on branches sorted by quasi-order;
wenzelm
parents:
38476
diff
changeset
|
152 |
val range: Text.Range = Text.Range(0, length) |
34855
81d0410dc3ac
iterators for ranges of commands/starts -- avoid extra array per document;
wenzelm
parents:
34835
diff
changeset
|
153 |
|
34859 | 154 |
lazy val symbol_index = new Symbol.Index(source) |
38579 | 155 |
def decode(i: Text.Offset): Text.Offset = symbol_index.decode(i) |
156 |
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
|
157 |
|
8b15d0f98962
explicit Document.State value, instead of individual state variables in Session, Command, Document;
wenzelm
parents:
38367
diff
changeset
|
158 |
|
8b15d0f98962
explicit Document.State value, instead of individual state variables in Session, Command, Document;
wenzelm
parents:
38367
diff
changeset
|
159 |
/* accumulated results */ |
8b15d0f98962
explicit Document.State value, instead of individual state variables in Session, Command, Document;
wenzelm
parents:
38367
diff
changeset
|
160 |
|
38872 | 161 |
val empty_state: Command.State = Command.State(this) |
34676
9e725d34df7b
Command and Command_State handle results from prover as Accumulator
immler@in.tum.de
parents:
34675
diff
changeset
|
162 |
} |