author | wenzelm |
Fri, 31 Aug 2012 13:23:25 +0200 | |
changeset 49036 | 4680c4046814 |
parent 49009 | 15381ea111ec |
child 49039 | e780d1bf767e |
permissions | -rw-r--r-- |
45709
87017fcbad83
clarified modules (again) -- NB: both Document and Protocol are specific to this particular prover;
wenzelm
parents:
45672
diff
changeset
|
1 |
/* Title: Pure/PIDE/protocol.scala |
38412
c23f3abbf42d
moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff
changeset
|
2 |
Author: Makarius |
c23f3abbf42d
moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff
changeset
|
3 |
|
45709
87017fcbad83
clarified modules (again) -- NB: both Document and Protocol are specific to this particular prover;
wenzelm
parents:
45672
diff
changeset
|
4 |
Protocol message formats for interactive proof documents. |
38412
c23f3abbf42d
moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff
changeset
|
5 |
*/ |
c23f3abbf42d
moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff
changeset
|
6 |
|
c23f3abbf42d
moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff
changeset
|
7 |
package isabelle |
c23f3abbf42d
moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff
changeset
|
8 |
|
c23f3abbf42d
moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff
changeset
|
9 |
|
45709
87017fcbad83
clarified modules (again) -- NB: both Document and Protocol are specific to this particular prover;
wenzelm
parents:
45672
diff
changeset
|
10 |
object Protocol |
38412
c23f3abbf42d
moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff
changeset
|
11 |
{ |
38567
b670faa807c9
concentrate protocol message formats in Isar_Document;
wenzelm
parents:
38483
diff
changeset
|
12 |
/* document editing */ |
38412
c23f3abbf42d
moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff
changeset
|
13 |
|
44476
e8a87398f35d
propagate information about last command with exec state assignment through document model;
wenzelm
parents:
44474
diff
changeset
|
14 |
object Assign |
e8a87398f35d
propagate information about last command with exec state assignment through document model;
wenzelm
parents:
44474
diff
changeset
|
15 |
{ |
44661
383c9d758a56
raw message function "assign_execs" avoids full overhead of decoding and caching message body;
wenzelm
parents:
44644
diff
changeset
|
16 |
def unapply(text: String): Option[(Document.Version_ID, Document.Assign)] = |
383c9d758a56
raw message function "assign_execs" avoids full overhead of decoding and caching message body;
wenzelm
parents:
44644
diff
changeset
|
17 |
try { |
383c9d758a56
raw message function "assign_execs" avoids full overhead of decoding and caching message body;
wenzelm
parents:
44644
diff
changeset
|
18 |
import XML.Decode._ |
383c9d758a56
raw message function "assign_execs" avoids full overhead of decoding and caching message body;
wenzelm
parents:
44644
diff
changeset
|
19 |
val body = YXML.parse_body(text) |
47388
fe4b245af74c
discontinued obsolete last_execs (cf. cd3ab7625519);
wenzelm
parents:
47346
diff
changeset
|
20 |
Some(pair(long, list(pair(long, option(long))))(body)) |
44661
383c9d758a56
raw message function "assign_execs" avoids full overhead of decoding and caching message body;
wenzelm
parents:
44644
diff
changeset
|
21 |
} |
383c9d758a56
raw message function "assign_execs" avoids full overhead of decoding and caching message body;
wenzelm
parents:
44644
diff
changeset
|
22 |
catch { |
383c9d758a56
raw message function "assign_execs" avoids full overhead of decoding and caching message body;
wenzelm
parents:
44644
diff
changeset
|
23 |
case ERROR(_) => None |
383c9d758a56
raw message function "assign_execs" avoids full overhead of decoding and caching message body;
wenzelm
parents:
44644
diff
changeset
|
24 |
case _: XML.XML_Atom => None |
383c9d758a56
raw message function "assign_execs" avoids full overhead of decoding and caching message body;
wenzelm
parents:
44644
diff
changeset
|
25 |
case _: XML.XML_Body => None |
38412
c23f3abbf42d
moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff
changeset
|
26 |
} |
c23f3abbf42d
moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff
changeset
|
27 |
} |
38567
b670faa807c9
concentrate protocol message formats in Isar_Document;
wenzelm
parents:
38483
diff
changeset
|
28 |
|
44676 | 29 |
object Removed |
30 |
{ |
|
31 |
def unapply(text: String): Option[List[Document.Version_ID]] = |
|
32 |
try { |
|
33 |
import XML.Decode._ |
|
34 |
Some(list(long)(YXML.parse_body(text))) |
|
35 |
} |
|
36 |
catch { |
|
37 |
case ERROR(_) => None |
|
38 |
case _: XML.XML_Atom => None |
|
39 |
case _: XML.XML_Body => None |
|
40 |
} |
|
41 |
} |
|
42 |
||
38567
b670faa807c9
concentrate protocol message formats in Isar_Document;
wenzelm
parents:
38483
diff
changeset
|
43 |
|
46209 | 44 |
/* command status */ |
38567
b670faa807c9
concentrate protocol message formats in Isar_Document;
wenzelm
parents:
38483
diff
changeset
|
45 |
|
46227
4aa84f84d5e8
more precise rendering of overview_color/gutter_message/squiggly_underline based on cumulation of command status and warning/error messages;
wenzelm
parents:
46209
diff
changeset
|
46 |
object Status |
4aa84f84d5e8
more precise rendering of overview_color/gutter_message/squiggly_underline based on cumulation of command status and warning/error messages;
wenzelm
parents:
46209
diff
changeset
|
47 |
{ |
4aa84f84d5e8
more precise rendering of overview_color/gutter_message/squiggly_underline based on cumulation of command status and warning/error messages;
wenzelm
parents:
46209
diff
changeset
|
48 |
val init = Status() |
4aa84f84d5e8
more precise rendering of overview_color/gutter_message/squiggly_underline based on cumulation of command status and warning/error messages;
wenzelm
parents:
46209
diff
changeset
|
49 |
} |
4aa84f84d5e8
more precise rendering of overview_color/gutter_message/squiggly_underline based on cumulation of command status and warning/error messages;
wenzelm
parents:
46209
diff
changeset
|
50 |
|
46166 | 51 |
sealed case class Status( |
49036
4680c4046814
further refinement of command status, to accomodate forked proofs;
wenzelm
parents:
49009
diff
changeset
|
52 |
private val touched: Boolean = false, |
47395
e6261a493f04
added static command status markup, to emphasize accepted but unassigned/unparsed commands (notably in overview panel);
wenzelm
parents:
47388
diff
changeset
|
53 |
private val accepted: Boolean = false, |
46166 | 54 |
private val failed: Boolean = false, |
49036
4680c4046814
further refinement of command status, to accomodate forked proofs;
wenzelm
parents:
49009
diff
changeset
|
55 |
forks: Int = 0, |
4680c4046814
further refinement of command status, to accomodate forked proofs;
wenzelm
parents:
49009
diff
changeset
|
56 |
runs: Int = 0) |
38567
b670faa807c9
concentrate protocol message formats in Isar_Document;
wenzelm
parents:
38483
diff
changeset
|
57 |
{ |
46227
4aa84f84d5e8
more precise rendering of overview_color/gutter_message/squiggly_underline based on cumulation of command status and warning/error messages;
wenzelm
parents:
46209
diff
changeset
|
58 |
def + (that: Status): Status = |
49036
4680c4046814
further refinement of command status, to accomodate forked proofs;
wenzelm
parents:
49009
diff
changeset
|
59 |
Status(touched || that.touched, accepted || that.accepted, failed || that.failed, |
4680c4046814
further refinement of command status, to accomodate forked proofs;
wenzelm
parents:
49009
diff
changeset
|
60 |
forks + that.forks, runs + that.runs) |
4680c4046814
further refinement of command status, to accomodate forked proofs;
wenzelm
parents:
49009
diff
changeset
|
61 |
|
4680c4046814
further refinement of command status, to accomodate forked proofs;
wenzelm
parents:
49009
diff
changeset
|
62 |
def is_unprocessed: Boolean = accepted && !failed && (!touched || (forks != 0 && runs == 0)) |
4680c4046814
further refinement of command status, to accomodate forked proofs;
wenzelm
parents:
49009
diff
changeset
|
63 |
def is_running: Boolean = runs != 0 |
4680c4046814
further refinement of command status, to accomodate forked proofs;
wenzelm
parents:
49009
diff
changeset
|
64 |
def is_finished: Boolean = !failed && forks == 0 && runs == 0 |
4680c4046814
further refinement of command status, to accomodate forked proofs;
wenzelm
parents:
49009
diff
changeset
|
65 |
def is_failed: Boolean = failed |
46166 | 66 |
} |
67 |
||
68 |
val command_status_markup: Set[String] = |
|
49036
4680c4046814
further refinement of command status, to accomodate forked proofs;
wenzelm
parents:
49009
diff
changeset
|
69 |
Set(Isabelle_Markup.ACCEPTED, Isabelle_Markup.FORKED, Isabelle_Markup.JOINED, |
4680c4046814
further refinement of command status, to accomodate forked proofs;
wenzelm
parents:
49009
diff
changeset
|
70 |
Isabelle_Markup.RUNNING, Isabelle_Markup.FINISHED, Isabelle_Markup.FAILED) |
46166 | 71 |
|
72 |
def command_status(status: Status, markup: Markup): Status = |
|
73 |
markup match { |
|
47395
e6261a493f04
added static command status markup, to emphasize accepted but unassigned/unparsed commands (notably in overview panel);
wenzelm
parents:
47388
diff
changeset
|
74 |
case Markup(Isabelle_Markup.ACCEPTED, _) => status.copy(accepted = true) |
49036
4680c4046814
further refinement of command status, to accomodate forked proofs;
wenzelm
parents:
49009
diff
changeset
|
75 |
case Markup(Isabelle_Markup.FORKED, _) => status.copy(touched = true, forks = status.forks + 1) |
4680c4046814
further refinement of command status, to accomodate forked proofs;
wenzelm
parents:
49009
diff
changeset
|
76 |
case Markup(Isabelle_Markup.JOINED, _) => status.copy(forks = status.forks - 1) |
4680c4046814
further refinement of command status, to accomodate forked proofs;
wenzelm
parents:
49009
diff
changeset
|
77 |
case Markup(Isabelle_Markup.RUNNING, _) => status.copy(touched = true, runs = status.runs + 1) |
4680c4046814
further refinement of command status, to accomodate forked proofs;
wenzelm
parents:
49009
diff
changeset
|
78 |
case Markup(Isabelle_Markup.FINISHED, _) => status.copy(runs = status.runs - 1) |
46166 | 79 |
case Markup(Isabelle_Markup.FAILED, _) => status.copy(failed = true) |
80 |
case _ => status |
|
38567
b670faa807c9
concentrate protocol message formats in Isar_Document;
wenzelm
parents:
38483
diff
changeset
|
81 |
} |
46166 | 82 |
|
83 |
def command_status(markups: List[Markup]): Status = |
|
46227
4aa84f84d5e8
more precise rendering of overview_color/gutter_message/squiggly_underline based on cumulation of command status and warning/error messages;
wenzelm
parents:
46209
diff
changeset
|
84 |
(Status.init /: markups)(command_status(_, _)) |
38887
1261481ef5e5
Command.State: add reported positions to markup tree, according main message position or Markup.binding/entity/report occurrences in body;
wenzelm
parents:
38581
diff
changeset
|
85 |
|
46209 | 86 |
|
87 |
/* node status */ |
|
88 |
||
46688 | 89 |
sealed case class Node_Status( |
90 |
unprocessed: Int, running: Int, finished: Int, warned: Int, failed: Int) |
|
44866 | 91 |
{ |
46688 | 92 |
def total: Int = unprocessed + running + finished + warned + failed |
44866 | 93 |
} |
44613 | 94 |
|
95 |
def node_status( |
|
96 |
state: Document.State, version: Document.Version, node: Document.Node): Node_Status = |
|
97 |
{ |
|
98 |
var unprocessed = 0 |
|
99 |
var running = 0 |
|
100 |
var finished = 0 |
|
46688 | 101 |
var warned = 0 |
44613 | 102 |
var failed = 0 |
103 |
node.commands.foreach(command => |
|
46166 | 104 |
{ |
46688 | 105 |
val st = state.command_state(version, command) |
106 |
val status = command_status(st.status) |
|
46166 | 107 |
if (status.is_running) running += 1 |
46688 | 108 |
else if (status.is_finished) { |
109 |
if (st.results.exists(p => is_warning(p._2))) warned += 1 |
|
110 |
else finished += 1 |
|
111 |
} |
|
46166 | 112 |
else if (status.is_failed) failed += 1 |
113 |
else unprocessed += 1 |
|
44613 | 114 |
}) |
46688 | 115 |
Node_Status(unprocessed, running, finished, warned, failed) |
44613 | 116 |
} |
117 |
||
38887
1261481ef5e5
Command.State: add reported positions to markup tree, according main message position or Markup.binding/entity/report occurrences in body;
wenzelm
parents:
38581
diff
changeset
|
118 |
|
39441
4110cc1b8f9f
allow embedded reports in regular prover messages, to avoid side-effects for errors for example;
wenzelm
parents:
39439
diff
changeset
|
119 |
/* result messages */ |
39439
1c294d150ded
eliminated markup "location" in favour of more explicit "no_report", which is actually deleted from messages;
wenzelm
parents:
39181
diff
changeset
|
120 |
|
1c294d150ded
eliminated markup "location" in favour of more explicit "no_report", which is actually deleted from messages;
wenzelm
parents:
39181
diff
changeset
|
121 |
def clean_message(body: XML.Body): XML.Body = |
45666 | 122 |
body filter { case XML.Elem(Markup(Isabelle_Markup.NO_REPORT, _), _) => false case _ => true } map |
39439
1c294d150ded
eliminated markup "location" in favour of more explicit "no_report", which is actually deleted from messages;
wenzelm
parents:
39181
diff
changeset
|
123 |
{ case XML.Elem(markup, ts) => XML.Elem(markup, clean_message(ts)) case t => t } |
1c294d150ded
eliminated markup "location" in favour of more explicit "no_report", which is actually deleted from messages;
wenzelm
parents:
39181
diff
changeset
|
124 |
|
39441
4110cc1b8f9f
allow embedded reports in regular prover messages, to avoid side-effects for errors for example;
wenzelm
parents:
39439
diff
changeset
|
125 |
def message_reports(msg: XML.Tree): List[XML.Elem] = |
4110cc1b8f9f
allow embedded reports in regular prover messages, to avoid side-effects for errors for example;
wenzelm
parents:
39439
diff
changeset
|
126 |
msg match { |
45666 | 127 |
case elem @ XML.Elem(Markup(Isabelle_Markup.REPORT, _), _) => List(elem) |
39441
4110cc1b8f9f
allow embedded reports in regular prover messages, to avoid side-effects for errors for example;
wenzelm
parents:
39439
diff
changeset
|
128 |
case XML.Elem(_, body) => body.flatMap(message_reports) |
4110cc1b8f9f
allow embedded reports in regular prover messages, to avoid side-effects for errors for example;
wenzelm
parents:
39439
diff
changeset
|
129 |
case XML.Text(_) => Nil |
4110cc1b8f9f
allow embedded reports in regular prover messages, to avoid side-effects for errors for example;
wenzelm
parents:
39439
diff
changeset
|
130 |
} |
4110cc1b8f9f
allow embedded reports in regular prover messages, to avoid side-effects for errors for example;
wenzelm
parents:
39439
diff
changeset
|
131 |
|
39439
1c294d150ded
eliminated markup "location" in favour of more explicit "no_report", which is actually deleted from messages;
wenzelm
parents:
39181
diff
changeset
|
132 |
|
39511 | 133 |
/* specific messages */ |
134 |
||
39625 | 135 |
def is_tracing(msg: XML.Tree): Boolean = |
39622
53365ba766ac
Command.accumulate: refrain from adding tracing messages to markup tree -- potential scalability problem;
wenzelm
parents:
39511
diff
changeset
|
136 |
msg match { |
45666 | 137 |
case XML.Elem(Markup(Isabelle_Markup.TRACING, _), _) => true |
39622
53365ba766ac
Command.accumulate: refrain from adding tracing messages to markup tree -- potential scalability problem;
wenzelm
parents:
39511
diff
changeset
|
138 |
case _ => false |
53365ba766ac
Command.accumulate: refrain from adding tracing messages to markup tree -- potential scalability problem;
wenzelm
parents:
39511
diff
changeset
|
139 |
} |
53365ba766ac
Command.accumulate: refrain from adding tracing messages to markup tree -- potential scalability problem;
wenzelm
parents:
39511
diff
changeset
|
140 |
|
39511 | 141 |
def is_warning(msg: XML.Tree): Boolean = |
142 |
msg match { |
|
45666 | 143 |
case XML.Elem(Markup(Isabelle_Markup.WARNING, _), _) => true |
39511 | 144 |
case _ => false |
145 |
} |
|
146 |
||
147 |
def is_error(msg: XML.Tree): Boolean = |
|
148 |
msg match { |
|
45666 | 149 |
case XML.Elem(Markup(Isabelle_Markup.ERROR, _), _) => true |
39511 | 150 |
case _ => false |
151 |
} |
|
38887
1261481ef5e5
Command.State: add reported positions to markup tree, according main message position or Markup.binding/entity/report occurrences in body;
wenzelm
parents:
38581
diff
changeset
|
152 |
|
39441
4110cc1b8f9f
allow embedded reports in regular prover messages, to avoid side-effects for errors for example;
wenzelm
parents:
39439
diff
changeset
|
153 |
def is_state(msg: XML.Tree): Boolean = |
39170
04ad0fed81f5
Isar_Document.reported_positions: exclude proof state output;
wenzelm
parents:
39042
diff
changeset
|
154 |
msg match { |
45666 | 155 |
case XML.Elem(Markup(Isabelle_Markup.WRITELN, _), |
156 |
List(XML.Elem(Markup(Isabelle_Markup.STATE, _), _))) => true |
|
39170
04ad0fed81f5
Isar_Document.reported_positions: exclude proof state output;
wenzelm
parents:
39042
diff
changeset
|
157 |
case _ => false |
04ad0fed81f5
Isar_Document.reported_positions: exclude proof state output;
wenzelm
parents:
39042
diff
changeset
|
158 |
} |
04ad0fed81f5
Isar_Document.reported_positions: exclude proof state output;
wenzelm
parents:
39042
diff
changeset
|
159 |
|
47542
26d0a76fef0a
more robust Sendback handling: JVM/jEdit paranoia for case matching, treat Pretty body not just XML.Text, replace proper_range only (without trailing whitespace);
wenzelm
parents:
47395
diff
changeset
|
160 |
object Sendback |
26d0a76fef0a
more robust Sendback handling: JVM/jEdit paranoia for case matching, treat Pretty body not just XML.Text, replace proper_range only (without trailing whitespace);
wenzelm
parents:
47395
diff
changeset
|
161 |
{ |
26d0a76fef0a
more robust Sendback handling: JVM/jEdit paranoia for case matching, treat Pretty body not just XML.Text, replace proper_range only (without trailing whitespace);
wenzelm
parents:
47395
diff
changeset
|
162 |
def unapply(msg: Any): Option[XML.Body] = |
26d0a76fef0a
more robust Sendback handling: JVM/jEdit paranoia for case matching, treat Pretty body not just XML.Text, replace proper_range only (without trailing whitespace);
wenzelm
parents:
47395
diff
changeset
|
163 |
msg match { |
26d0a76fef0a
more robust Sendback handling: JVM/jEdit paranoia for case matching, treat Pretty body not just XML.Text, replace proper_range only (without trailing whitespace);
wenzelm
parents:
47395
diff
changeset
|
164 |
case XML.Elem(Markup(Isabelle_Markup.SENDBACK, _), body) => Some(body) |
26d0a76fef0a
more robust Sendback handling: JVM/jEdit paranoia for case matching, treat Pretty body not just XML.Text, replace proper_range only (without trailing whitespace);
wenzelm
parents:
47395
diff
changeset
|
165 |
case _ => None |
26d0a76fef0a
more robust Sendback handling: JVM/jEdit paranoia for case matching, treat Pretty body not just XML.Text, replace proper_range only (without trailing whitespace);
wenzelm
parents:
47395
diff
changeset
|
166 |
} |
26d0a76fef0a
more robust Sendback handling: JVM/jEdit paranoia for case matching, treat Pretty body not just XML.Text, replace proper_range only (without trailing whitespace);
wenzelm
parents:
47395
diff
changeset
|
167 |
} |
26d0a76fef0a
more robust Sendback handling: JVM/jEdit paranoia for case matching, treat Pretty body not just XML.Text, replace proper_range only (without trailing whitespace);
wenzelm
parents:
47395
diff
changeset
|
168 |
|
39511 | 169 |
|
170 |
/* reported positions */ |
|
171 |
||
39627 | 172 |
private val include_pos = |
45666 | 173 |
Set(Isabelle_Markup.BINDING, Isabelle_Markup.ENTITY, Isabelle_Markup.REPORT, |
174 |
Isabelle_Markup.POSITION) |
|
39441
4110cc1b8f9f
allow embedded reports in regular prover messages, to avoid side-effects for errors for example;
wenzelm
parents:
39439
diff
changeset
|
175 |
|
4110cc1b8f9f
allow embedded reports in regular prover messages, to avoid side-effects for errors for example;
wenzelm
parents:
39439
diff
changeset
|
176 |
def message_positions(command: Command, message: XML.Elem): Set[Text.Range] = |
38887
1261481ef5e5
Command.State: add reported positions to markup tree, according main message position or Markup.binding/entity/report occurrences in body;
wenzelm
parents:
38581
diff
changeset
|
177 |
{ |
39441
4110cc1b8f9f
allow embedded reports in regular prover messages, to avoid side-effects for errors for example;
wenzelm
parents:
39439
diff
changeset
|
178 |
def positions(set: Set[Text.Range], tree: XML.Tree): Set[Text.Range] = |
38887
1261481ef5e5
Command.State: add reported positions to markup tree, according main message position or Markup.binding/entity/report occurrences in body;
wenzelm
parents:
38581
diff
changeset
|
179 |
tree match { |
39172
31b95e0da7b7
Isar_Document.reported_positions: slightly more robust treatment of positions outside the command range, notably parsing beyond EOF;
wenzelm
parents:
39170
diff
changeset
|
180 |
case XML.Elem(Markup(name, Position.Id_Range(id, raw_range)), body) |
31b95e0da7b7
Isar_Document.reported_positions: slightly more robust treatment of positions outside the command range, notably parsing beyond EOF;
wenzelm
parents:
39170
diff
changeset
|
181 |
if include_pos(name) && id == command.id => |
31b95e0da7b7
Isar_Document.reported_positions: slightly more robust treatment of positions outside the command range, notably parsing beyond EOF;
wenzelm
parents:
39170
diff
changeset
|
182 |
val range = command.decode(raw_range).restrict(command.range) |
39441
4110cc1b8f9f
allow embedded reports in regular prover messages, to avoid side-effects for errors for example;
wenzelm
parents:
39439
diff
changeset
|
183 |
body.foldLeft(if (range.is_singularity) set else set + range)(positions) |
4110cc1b8f9f
allow embedded reports in regular prover messages, to avoid side-effects for errors for example;
wenzelm
parents:
39439
diff
changeset
|
184 |
case XML.Elem(Markup(name, _), body) => body.foldLeft(set)(positions) |
39042
470fd769ae53
Isar_Document.reported_positions: more precise include/exclude, include root as last resort only;
wenzelm
parents:
38887
diff
changeset
|
185 |
case _ => set |
38887
1261481ef5e5
Command.State: add reported positions to markup tree, according main message position or Markup.binding/entity/report occurrences in body;
wenzelm
parents:
38581
diff
changeset
|
186 |
} |
39441
4110cc1b8f9f
allow embedded reports in regular prover messages, to avoid side-effects for errors for example;
wenzelm
parents:
39439
diff
changeset
|
187 |
val set = positions(Set.empty, message) |
39170
04ad0fed81f5
Isar_Document.reported_positions: exclude proof state output;
wenzelm
parents:
39042
diff
changeset
|
188 |
if (set.isEmpty && !is_state(message)) |
39172
31b95e0da7b7
Isar_Document.reported_positions: slightly more robust treatment of positions outside the command range, notably parsing beyond EOF;
wenzelm
parents:
39170
diff
changeset
|
189 |
set ++ Position.Range.unapply(message.markup.properties).map(command.decode(_)) |
39042
470fd769ae53
Isar_Document.reported_positions: more precise include/exclude, include root as last resort only;
wenzelm
parents:
38887
diff
changeset
|
190 |
else set |
38887
1261481ef5e5
Command.State: add reported positions to markup tree, according main message position or Markup.binding/entity/report occurrences in body;
wenzelm
parents:
38581
diff
changeset
|
191 |
} |
38412
c23f3abbf42d
moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff
changeset
|
192 |
} |
c23f3abbf42d
moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff
changeset
|
193 |
|
c23f3abbf42d
moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff
changeset
|
194 |
|
45709
87017fcbad83
clarified modules (again) -- NB: both Document and Protocol are specific to this particular prover;
wenzelm
parents:
45672
diff
changeset
|
195 |
trait Protocol extends Isabelle_Process |
38412
c23f3abbf42d
moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff
changeset
|
196 |
{ |
c23f3abbf42d
moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff
changeset
|
197 |
/* commands */ |
c23f3abbf42d
moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff
changeset
|
198 |
|
44644
317e4962dd0f
clarified define_command: store name as structural information;
wenzelm
parents:
44615
diff
changeset
|
199 |
def define_command(command: Command): Unit = |
45709
87017fcbad83
clarified modules (again) -- NB: both Document and Protocol are specific to this particular prover;
wenzelm
parents:
45672
diff
changeset
|
200 |
input("Document.define_command", |
48705
dd32321d6eef
tuned signature -- slightly more abstract text representation of prover process;
wenzelm
parents:
47542
diff
changeset
|
201 |
Document.ID(command.id), encode(command.name), encode(command.source)) |
38412
c23f3abbf42d
moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff
changeset
|
202 |
|
c23f3abbf42d
moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff
changeset
|
203 |
|
38417 | 204 |
/* document versions */ |
38412
c23f3abbf42d
moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff
changeset
|
205 |
|
47343
b8aeab386414
less aggressive discontinue_execution before document update, to avoid unstable execs that need to be re-assigned;
wenzelm
parents:
46938
diff
changeset
|
206 |
def discontinue_execution() { input("Document.discontinue_execution") } |
b8aeab386414
less aggressive discontinue_execution before document update, to avoid unstable execs that need to be re-assigned;
wenzelm
parents:
46938
diff
changeset
|
207 |
|
b8aeab386414
less aggressive discontinue_execution before document update, to avoid unstable execs that need to be re-assigned;
wenzelm
parents:
46938
diff
changeset
|
208 |
def cancel_execution() { input("Document.cancel_execution") } |
44612
990ac978854c
explicit cancel_execution before queueing new edits -- potential performance improvement for machines with few cores;
wenzelm
parents:
44481
diff
changeset
|
209 |
|
44481 | 210 |
def update(old_id: Document.Version_ID, new_id: Document.Version_ID, |
44383 | 211 |
edits: List[Document.Edit_Command]) |
38412
c23f3abbf42d
moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff
changeset
|
212 |
{ |
44157
a21d3e1e64fd
uniform treatment of header edits as document edits;
wenzelm
parents:
44156
diff
changeset
|
213 |
val edits_yxml = |
43767 | 214 |
{ import XML.Encode._ |
44383 | 215 |
def id: T[Command] = (cmd => long(cmd.id)) |
46737 | 216 |
def encode_edit(name: Document.Node.Name) |
44979
68b990e950b1
explicit master_dir as part of header -- still required (for Cygwin) since Scala layer does not pass file content yet;
wenzelm
parents:
44866
diff
changeset
|
217 |
: T[Document.Node.Edit[(Option[Command], Option[Command]), Command.Perspective]] = |
68b990e950b1
explicit master_dir as part of header -- still required (for Cygwin) since Scala layer does not pass file content yet;
wenzelm
parents:
44866
diff
changeset
|
218 |
variant(List( |
48755
393a37003851
apply all text edits to each node, before determining the resulting doc_edits -- allow several iterations to consolidate spans etc.;
wenzelm
parents:
48707
diff
changeset
|
219 |
{ case Document.Node.Clear() => (Nil, Nil) }, // FIXME unused !? |
44979
68b990e950b1
explicit master_dir as part of header -- still required (for Cygwin) since Scala layer does not pass file content yet;
wenzelm
parents:
44866
diff
changeset
|
220 |
{ case Document.Node.Edits(a) => (Nil, list(pair(option(id), option(id)))(a)) }, |
48707
ba531af91148
simplified Document.Node.Header -- internalized errors;
wenzelm
parents:
48705
diff
changeset
|
221 |
{ case Document.Node.Deps(header) => |
46770
44c28a33c461
retain original "uses" (again) -- still required for Thy_Load.use_file etc. in ML (notably for maintaining required/provided);
wenzelm
parents:
46755
diff
changeset
|
222 |
val dir = Isabelle_System.posix_path(name.dir) |
48707
ba531af91148
simplified Document.Node.Header -- internalized errors;
wenzelm
parents:
48705
diff
changeset
|
223 |
val imports = header.imports.map(_.node) |
46770
44c28a33c461
retain original "uses" (again) -- still required for Thy_Load.use_file etc. in ML (notably for maintaining required/provided);
wenzelm
parents:
46755
diff
changeset
|
224 |
// FIXME val uses = deps.uses.map(p => (Isabelle_System.posix_path(p._1), p._2)) |
48707
ba531af91148
simplified Document.Node.Header -- internalized errors;
wenzelm
parents:
48705
diff
changeset
|
225 |
val uses = header.uses |
44979
68b990e950b1
explicit master_dir as part of header -- still required (for Cygwin) since Scala layer does not pass file content yet;
wenzelm
parents:
44866
diff
changeset
|
226 |
(Nil, |
48707
ba531af91148
simplified Document.Node.Header -- internalized errors;
wenzelm
parents:
48705
diff
changeset
|
227 |
pair(Encode.string, pair(Encode.string, pair(list(Encode.string), |
48864
3ee314ae1e0a
added keyword kind "thy_load" (with optional list of file extensions);
wenzelm
parents:
48755
diff
changeset
|
228 |
pair(list(pair(Encode.string, |
3ee314ae1e0a
added keyword kind "thy_load" (with optional list of file extensions);
wenzelm
parents:
48755
diff
changeset
|
229 |
option(pair(pair(Encode.string, list(Encode.string)), list(Encode.string))))), |
48707
ba531af91148
simplified Document.Node.Header -- internalized errors;
wenzelm
parents:
48705
diff
changeset
|
230 |
pair(list(pair(Encode.string, bool)), list(Encode.string))))))( |
ba531af91148
simplified Document.Node.Header -- internalized errors;
wenzelm
parents:
48705
diff
changeset
|
231 |
(dir, (name.theory, (imports, (header.keywords, (uses, header.errors))))))) }, |
44979
68b990e950b1
explicit master_dir as part of header -- still required (for Cygwin) since Scala layer does not pass file content yet;
wenzelm
parents:
44866
diff
changeset
|
232 |
{ case Document.Node.Perspective(a) => (a.commands.map(c => long_atom(c.id)), Nil) })) |
48705
dd32321d6eef
tuned signature -- slightly more abstract text representation of prover process;
wenzelm
parents:
47542
diff
changeset
|
233 |
def encode_edits: T[List[Document.Edit_Command]] = list((node_edit: Document.Edit_Command) => |
44979
68b990e950b1
explicit master_dir as part of header -- still required (for Cygwin) since Scala layer does not pass file content yet;
wenzelm
parents:
44866
diff
changeset
|
234 |
{ |
68b990e950b1
explicit master_dir as part of header -- still required (for Cygwin) since Scala layer does not pass file content yet;
wenzelm
parents:
44866
diff
changeset
|
235 |
val (name, edit) = node_edit |
46737 | 236 |
pair(string, encode_edit(name))(name.node, edit) |
44979
68b990e950b1
explicit master_dir as part of header -- still required (for Cygwin) since Scala layer does not pass file content yet;
wenzelm
parents:
44866
diff
changeset
|
237 |
}) |
48705
dd32321d6eef
tuned signature -- slightly more abstract text representation of prover process;
wenzelm
parents:
47542
diff
changeset
|
238 |
YXML.string_of_body(encode_edits(edits)) } |
45709
87017fcbad83
clarified modules (again) -- NB: both Document and Protocol are specific to this particular prover;
wenzelm
parents:
45672
diff
changeset
|
239 |
input("Document.update", Document.ID(old_id), Document.ID(new_id), edits_yxml) |
38412
c23f3abbf42d
moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff
changeset
|
240 |
} |
43748 | 241 |
|
44673 | 242 |
def remove_versions(versions: List[Document.Version]) |
243 |
{ |
|
244 |
val versions_yxml = |
|
245 |
{ import XML.Encode._ |
|
246 |
YXML.string_of_body(list(long)(versions.map(_.id))) } |
|
45709
87017fcbad83
clarified modules (again) -- NB: both Document and Protocol are specific to this particular prover;
wenzelm
parents:
45672
diff
changeset
|
247 |
input("Document.remove_versions", versions_yxml) |
44673 | 248 |
} |
249 |
||
43748 | 250 |
|
251 |
/* method invocation service */ |
|
252 |
||
253 |
def invoke_scala(id: String, tag: Invoke_Scala.Tag.Value, res: String) |
|
254 |
{ |
|
45709
87017fcbad83
clarified modules (again) -- NB: both Document and Protocol are specific to this particular prover;
wenzelm
parents:
45672
diff
changeset
|
255 |
input("Document.invoke_scala", id, tag.toString, res) |
43748 | 256 |
} |
38412
c23f3abbf42d
moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff
changeset
|
257 |
} |