author | wenzelm |
Tue, 19 Nov 2013 19:33:27 +0100 | |
changeset 54519 | 5fed81762406 |
parent 54515 | 570ba266f5b5 |
child 54524 | 14609d36cab8 |
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 |
|
52563 | 14 |
object Assign_Update |
44476
e8a87398f35d
propagate information about last command with exec state assignment through document model;
wenzelm
parents:
44474
diff
changeset
|
15 |
{ |
52563 | 16 |
def unapply(text: String): Option[(Document_ID.Version, Document.Assign_Update)] = |
44661
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) |
52527
dbac84eab3bc
separate exec_id assignment for Command.print states, without affecting result of eval;
wenzelm
parents:
52111
diff
changeset
|
20 |
Some(pair(long, list(pair(long, list(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 |
51987 | 24 |
case _: XML.Error => None |
38412
c23f3abbf42d
moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff
changeset
|
25 |
} |
c23f3abbf42d
moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff
changeset
|
26 |
} |
38567
b670faa807c9
concentrate protocol message formats in Isar_Document;
wenzelm
parents:
38483
diff
changeset
|
27 |
|
44676 | 28 |
object Removed |
29 |
{ |
|
52530
99dd8b4ef3fe
explicit module Document_ID as source of globally unique identifiers across ML/Scala;
wenzelm
parents:
52527
diff
changeset
|
30 |
def unapply(text: String): Option[List[Document_ID.Version]] = |
44676 | 31 |
try { |
32 |
import XML.Decode._ |
|
33 |
Some(list(long)(YXML.parse_body(text))) |
|
34 |
} |
|
35 |
catch { |
|
36 |
case ERROR(_) => None |
|
51987 | 37 |
case _: XML.Error => None |
44676 | 38 |
} |
39 |
} |
|
40 |
||
38567
b670faa807c9
concentrate protocol message formats in Isar_Document;
wenzelm
parents:
38483
diff
changeset
|
41 |
|
46209 | 42 |
/* command status */ |
38567
b670faa807c9
concentrate protocol message formats in Isar_Document;
wenzelm
parents:
38483
diff
changeset
|
43 |
|
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
|
44 |
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
|
45 |
{ |
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 |
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
|
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 |
|
46166 | 49 |
sealed case class Status( |
49036
4680c4046814
further refinement of command status, to accomodate forked proofs;
wenzelm
parents:
49009
diff
changeset
|
50 |
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
|
51 |
private val accepted: Boolean = false, |
46166 | 52 |
private val failed: Boolean = false, |
49036
4680c4046814
further refinement of command status, to accomodate forked proofs;
wenzelm
parents:
49009
diff
changeset
|
53 |
forks: Int = 0, |
4680c4046814
further refinement of command status, to accomodate forked proofs;
wenzelm
parents:
49009
diff
changeset
|
54 |
runs: Int = 0) |
38567
b670faa807c9
concentrate protocol message formats in Isar_Document;
wenzelm
parents:
38483
diff
changeset
|
55 |
{ |
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
|
56 |
def + (that: Status): Status = |
49036
4680c4046814
further refinement of command status, to accomodate forked proofs;
wenzelm
parents:
49009
diff
changeset
|
57 |
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
|
58 |
forks + that.forks, runs + that.runs) |
4680c4046814
further refinement of command status, to accomodate forked proofs;
wenzelm
parents:
49009
diff
changeset
|
59 |
|
4680c4046814
further refinement of command status, to accomodate forked proofs;
wenzelm
parents:
49009
diff
changeset
|
60 |
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
|
61 |
def is_running: Boolean = runs != 0 |
49039 | 62 |
def is_finished: Boolean = !failed && touched && forks == 0 && runs == 0 |
49036
4680c4046814
further refinement of command status, to accomodate forked proofs;
wenzelm
parents:
49009
diff
changeset
|
63 |
def is_failed: Boolean = failed |
46166 | 64 |
} |
65 |
||
66 |
val command_status_markup: Set[String] = |
|
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
50157
diff
changeset
|
67 |
Set(Markup.ACCEPTED, Markup.FORKED, Markup.JOINED, Markup.RUNNING, |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
50157
diff
changeset
|
68 |
Markup.FINISHED, Markup.FAILED) |
46166 | 69 |
|
70 |
def command_status(status: Status, markup: Markup): Status = |
|
71 |
markup match { |
|
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
50157
diff
changeset
|
72 |
case Markup(Markup.ACCEPTED, _) => status.copy(accepted = true) |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
50157
diff
changeset
|
73 |
case Markup(Markup.FORKED, _) => status.copy(touched = true, forks = status.forks + 1) |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
50157
diff
changeset
|
74 |
case Markup(Markup.JOINED, _) => status.copy(forks = status.forks - 1) |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
50157
diff
changeset
|
75 |
case Markup(Markup.RUNNING, _) => status.copy(touched = true, runs = status.runs + 1) |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
50157
diff
changeset
|
76 |
case Markup(Markup.FINISHED, _) => status.copy(runs = status.runs - 1) |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
50157
diff
changeset
|
77 |
case Markup(Markup.FAILED, _) => status.copy(failed = true) |
46166 | 78 |
case _ => status |
38567
b670faa807c9
concentrate protocol message formats in Isar_Document;
wenzelm
parents:
38483
diff
changeset
|
79 |
} |
46166 | 80 |
|
81 |
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
|
82 |
(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
|
83 |
|
46209 | 84 |
|
51818
517f232e867d
clarified module dependencies: avoid Properties and Document introding minimal "PIDE";
wenzelm
parents:
51533
diff
changeset
|
85 |
/* command timing */ |
517f232e867d
clarified module dependencies: avoid Properties and Document introding minimal "PIDE";
wenzelm
parents:
51533
diff
changeset
|
86 |
|
517f232e867d
clarified module dependencies: avoid Properties and Document introding minimal "PIDE";
wenzelm
parents:
51533
diff
changeset
|
87 |
object Command_Timing |
517f232e867d
clarified module dependencies: avoid Properties and Document introding minimal "PIDE";
wenzelm
parents:
51533
diff
changeset
|
88 |
{ |
52531 | 89 |
def unapply(props: Properties.T): Option[(Document_ID.Generic, isabelle.Timing)] = |
51818
517f232e867d
clarified module dependencies: avoid Properties and Document introding minimal "PIDE";
wenzelm
parents:
51533
diff
changeset
|
90 |
props match { |
517f232e867d
clarified module dependencies: avoid Properties and Document introding minimal "PIDE";
wenzelm
parents:
51533
diff
changeset
|
91 |
case (Markup.FUNCTION, Markup.COMMAND_TIMING) :: args => |
517f232e867d
clarified module dependencies: avoid Properties and Document introding minimal "PIDE";
wenzelm
parents:
51533
diff
changeset
|
92 |
(args, args) match { |
517f232e867d
clarified module dependencies: avoid Properties and Document introding minimal "PIDE";
wenzelm
parents:
51533
diff
changeset
|
93 |
case (Position.Id(id), Markup.Timing_Properties(timing)) => Some((id, timing)) |
517f232e867d
clarified module dependencies: avoid Properties and Document introding minimal "PIDE";
wenzelm
parents:
51533
diff
changeset
|
94 |
case _ => None |
517f232e867d
clarified module dependencies: avoid Properties and Document introding minimal "PIDE";
wenzelm
parents:
51533
diff
changeset
|
95 |
} |
517f232e867d
clarified module dependencies: avoid Properties and Document introding minimal "PIDE";
wenzelm
parents:
51533
diff
changeset
|
96 |
case _ => None |
517f232e867d
clarified module dependencies: avoid Properties and Document introding minimal "PIDE";
wenzelm
parents:
51533
diff
changeset
|
97 |
} |
517f232e867d
clarified module dependencies: avoid Properties and Document introding minimal "PIDE";
wenzelm
parents:
51533
diff
changeset
|
98 |
} |
517f232e867d
clarified module dependencies: avoid Properties and Document introding minimal "PIDE";
wenzelm
parents:
51533
diff
changeset
|
99 |
|
517f232e867d
clarified module dependencies: avoid Properties and Document introding minimal "PIDE";
wenzelm
parents:
51533
diff
changeset
|
100 |
|
46209 | 101 |
/* node status */ |
102 |
||
46688 | 103 |
sealed case class Node_Status( |
104 |
unprocessed: Int, running: Int, finished: Int, warned: Int, failed: Int) |
|
44866 | 105 |
{ |
46688 | 106 |
def total: Int = unprocessed + running + finished + warned + failed |
44866 | 107 |
} |
44613 | 108 |
|
109 |
def node_status( |
|
110 |
state: Document.State, version: Document.Version, node: Document.Node): Node_Status = |
|
111 |
{ |
|
112 |
var unprocessed = 0 |
|
113 |
var running = 0 |
|
114 |
var finished = 0 |
|
46688 | 115 |
var warned = 0 |
44613 | 116 |
var failed = 0 |
117 |
node.commands.foreach(command => |
|
46166 | 118 |
{ |
46688 | 119 |
val st = state.command_state(version, command) |
120 |
val status = command_status(st.status) |
|
46166 | 121 |
if (status.is_running) running += 1 |
46688 | 122 |
else if (status.is_finished) { |
50507 | 123 |
if (st.results.entries.exists(p => is_warning(p._2))) warned += 1 |
46688 | 124 |
else finished += 1 |
125 |
} |
|
46166 | 126 |
else if (status.is_failed) failed += 1 |
127 |
else unprocessed += 1 |
|
44613 | 128 |
}) |
46688 | 129 |
Node_Status(unprocessed, running, finished, warned, failed) |
44613 | 130 |
} |
131 |
||
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
|
132 |
|
51533 | 133 |
/* node timing */ |
134 |
||
135 |
sealed case class Node_Timing(total: Double, commands: Map[Command, Double]) |
|
136 |
||
137 |
val empty_node_timing = Node_Timing(0.0, Map.empty) |
|
138 |
||
139 |
def node_timing( |
|
140 |
state: Document.State, |
|
141 |
version: Document.Version, |
|
142 |
node: Document.Node, |
|
143 |
threshold: Double): Node_Timing = |
|
144 |
{ |
|
145 |
var total = 0.0 |
|
146 |
var commands = Map.empty[Command, Double] |
|
147 |
for { |
|
148 |
command <- node.commands.iterator |
|
149 |
st = state.command_state(version, command) |
|
150 |
command_timing = |
|
151 |
(0.0 /: st.status)({ |
|
152 |
case (timing, Markup.Timing(t)) => timing + t.elapsed.seconds |
|
153 |
case (timing, _) => timing |
|
154 |
}) |
|
155 |
} { |
|
156 |
total += command_timing |
|
157 |
if (command_timing >= threshold) commands += (command -> command_timing) |
|
158 |
} |
|
159 |
Node_Timing(total, commands) |
|
160 |
} |
|
161 |
||
162 |
||
39441
4110cc1b8f9f
allow embedded reports in regular prover messages, to avoid side-effects for errors for example;
wenzelm
parents:
39439
diff
changeset
|
163 |
/* 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
|
164 |
|
50450
358b6020f8b6
generalized notion of active area, where sendback is just one application;
wenzelm
parents:
50201
diff
changeset
|
165 |
private val clean = Set(Markup.REPORT, Markup.NO_REPORT) |
358b6020f8b6
generalized notion of active area, where sendback is just one application;
wenzelm
parents:
50201
diff
changeset
|
166 |
|
39439
1c294d150ded
eliminated markup "location" in favour of more explicit "no_report", which is actually deleted from messages;
wenzelm
parents:
39181
diff
changeset
|
167 |
def clean_message(body: XML.Body): XML.Body = |
49445
638cefe3ee99
earlier treatment of embedded report/no_report messages (see also 4110cc1b8f9f);
wenzelm
parents:
49418
diff
changeset
|
168 |
body filter { |
50450
358b6020f8b6
generalized notion of active area, where sendback is just one application;
wenzelm
parents:
50201
diff
changeset
|
169 |
case XML.Wrapped_Elem(Markup(name, _), _, _) => !clean(name) |
358b6020f8b6
generalized notion of active area, where sendback is just one application;
wenzelm
parents:
50201
diff
changeset
|
170 |
case XML.Elem(Markup(name, _), _) => !clean(name) |
49445
638cefe3ee99
earlier treatment of embedded report/no_report messages (see also 4110cc1b8f9f);
wenzelm
parents:
49418
diff
changeset
|
171 |
case _ => true |
49650
9fad6480300d
support for wrapped XML elements, which allows to preserve full markup tree information in to_XML/from_XML conversion;
wenzelm
parents:
49648
diff
changeset
|
172 |
} map { |
9fad6480300d
support for wrapped XML elements, which allows to preserve full markup tree information in to_XML/from_XML conversion;
wenzelm
parents:
49648
diff
changeset
|
173 |
case XML.Wrapped_Elem(markup, body, ts) => XML.Wrapped_Elem(markup, body, clean_message(ts)) |
9fad6480300d
support for wrapped XML elements, which allows to preserve full markup tree information in to_XML/from_XML conversion;
wenzelm
parents:
49648
diff
changeset
|
174 |
case XML.Elem(markup, ts) => XML.Elem(markup, clean_message(ts)) |
9fad6480300d
support for wrapped XML elements, which allows to preserve full markup tree information in to_XML/from_XML conversion;
wenzelm
parents:
49648
diff
changeset
|
175 |
case t => t |
9fad6480300d
support for wrapped XML elements, which allows to preserve full markup tree information in to_XML/from_XML conversion;
wenzelm
parents:
49648
diff
changeset
|
176 |
} |
39439
1c294d150ded
eliminated markup "location" in favour of more explicit "no_report", which is actually deleted from messages;
wenzelm
parents:
39181
diff
changeset
|
177 |
|
49445
638cefe3ee99
earlier treatment of embedded report/no_report messages (see also 4110cc1b8f9f);
wenzelm
parents:
49418
diff
changeset
|
178 |
def message_reports(props: Properties.T, body: XML.Body): List[XML.Elem] = |
638cefe3ee99
earlier treatment of embedded report/no_report messages (see also 4110cc1b8f9f);
wenzelm
parents:
49418
diff
changeset
|
179 |
body flatMap { |
50450
358b6020f8b6
generalized notion of active area, where sendback is just one application;
wenzelm
parents:
50201
diff
changeset
|
180 |
case XML.Wrapped_Elem(Markup(Markup.REPORT, ps), body, ts) => |
358b6020f8b6
generalized notion of active area, where sendback is just one application;
wenzelm
parents:
50201
diff
changeset
|
181 |
List(XML.Wrapped_Elem(Markup(Markup.REPORT, props ::: ps), body, ts)) |
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
50157
diff
changeset
|
182 |
case XML.Elem(Markup(Markup.REPORT, ps), ts) => |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
50157
diff
changeset
|
183 |
List(XML.Elem(Markup(Markup.REPORT, props ::: ps), ts)) |
49650
9fad6480300d
support for wrapped XML elements, which allows to preserve full markup tree information in to_XML/from_XML conversion;
wenzelm
parents:
49648
diff
changeset
|
184 |
case XML.Wrapped_Elem(_, _, ts) => message_reports(props, ts) |
49445
638cefe3ee99
earlier treatment of embedded report/no_report messages (see also 4110cc1b8f9f);
wenzelm
parents:
49418
diff
changeset
|
185 |
case XML.Elem(_, ts) => message_reports(props, ts) |
39441
4110cc1b8f9f
allow embedded reports in regular prover messages, to avoid side-effects for errors for example;
wenzelm
parents:
39439
diff
changeset
|
186 |
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
|
187 |
} |
4110cc1b8f9f
allow embedded reports in regular prover messages, to avoid side-effects for errors for example;
wenzelm
parents:
39439
diff
changeset
|
188 |
|
39439
1c294d150ded
eliminated markup "location" in favour of more explicit "no_report", which is actually deleted from messages;
wenzelm
parents:
39181
diff
changeset
|
189 |
|
39511 | 190 |
/* specific messages */ |
191 |
||
50500
c94bba7906d2
identify dialogs via official serial and maintain as result message;
wenzelm
parents:
50498
diff
changeset
|
192 |
def is_inlined(msg: XML.Tree): Boolean = |
c94bba7906d2
identify dialogs via official serial and maintain as result message;
wenzelm
parents:
50498
diff
changeset
|
193 |
!(is_result(msg) || is_tracing(msg) || is_state(msg)) |
c94bba7906d2
identify dialogs via official serial and maintain as result message;
wenzelm
parents:
50498
diff
changeset
|
194 |
|
c94bba7906d2
identify dialogs via official serial and maintain as result message;
wenzelm
parents:
50498
diff
changeset
|
195 |
def is_result(msg: XML.Tree): Boolean = |
c94bba7906d2
identify dialogs via official serial and maintain as result message;
wenzelm
parents:
50498
diff
changeset
|
196 |
msg match { |
c94bba7906d2
identify dialogs via official serial and maintain as result message;
wenzelm
parents:
50498
diff
changeset
|
197 |
case XML.Elem(Markup(Markup.RESULT, _), _) => true |
c94bba7906d2
identify dialogs via official serial and maintain as result message;
wenzelm
parents:
50498
diff
changeset
|
198 |
case _ => false |
c94bba7906d2
identify dialogs via official serial and maintain as result message;
wenzelm
parents:
50498
diff
changeset
|
199 |
} |
c94bba7906d2
identify dialogs via official serial and maintain as result message;
wenzelm
parents:
50498
diff
changeset
|
200 |
|
50157 | 201 |
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
|
202 |
msg match { |
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
50157
diff
changeset
|
203 |
case XML.Elem(Markup(Markup.TRACING, _), _) => true |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
50157
diff
changeset
|
204 |
case XML.Elem(Markup(Markup.TRACING_MESSAGE, _), _) => true |
39622
53365ba766ac
Command.accumulate: refrain from adding tracing messages to markup tree -- potential scalability problem;
wenzelm
parents:
39511
diff
changeset
|
205 |
case _ => false |
53365ba766ac
Command.accumulate: refrain from adding tracing messages to markup tree -- potential scalability problem;
wenzelm
parents:
39511
diff
changeset
|
206 |
} |
53365ba766ac
Command.accumulate: refrain from adding tracing messages to markup tree -- potential scalability problem;
wenzelm
parents:
39511
diff
changeset
|
207 |
|
52650 | 208 |
def is_writeln_markup(msg: XML.Tree, name: String): Boolean = |
50500
c94bba7906d2
identify dialogs via official serial and maintain as result message;
wenzelm
parents:
50498
diff
changeset
|
209 |
msg match { |
c94bba7906d2
identify dialogs via official serial and maintain as result message;
wenzelm
parents:
50498
diff
changeset
|
210 |
case XML.Elem(Markup(Markup.WRITELN, _), |
52650 | 211 |
List(XML.Elem(markup, _))) => markup.name == name |
50500
c94bba7906d2
identify dialogs via official serial and maintain as result message;
wenzelm
parents:
50498
diff
changeset
|
212 |
case XML.Elem(Markup(Markup.WRITELN_MESSAGE, _), |
52650 | 213 |
List(XML.Elem(markup, _))) => markup.name == name |
50500
c94bba7906d2
identify dialogs via official serial and maintain as result message;
wenzelm
parents:
50498
diff
changeset
|
214 |
case _ => false |
c94bba7906d2
identify dialogs via official serial and maintain as result message;
wenzelm
parents:
50498
diff
changeset
|
215 |
} |
c94bba7906d2
identify dialogs via official serial and maintain as result message;
wenzelm
parents:
50498
diff
changeset
|
216 |
|
52650 | 217 |
def is_state(msg: XML.Tree): Boolean = is_writeln_markup(msg, Markup.STATE) |
218 |
def is_information(msg: XML.Tree): Boolean = is_writeln_markup(msg, Markup.INFORMATION) |
|
219 |
||
39511 | 220 |
def is_warning(msg: XML.Tree): Boolean = |
221 |
msg match { |
|
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
50157
diff
changeset
|
222 |
case XML.Elem(Markup(Markup.WARNING, _), _) => true |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
50157
diff
changeset
|
223 |
case XML.Elem(Markup(Markup.WARNING_MESSAGE, _), _) => true |
39511 | 224 |
case _ => false |
225 |
} |
|
226 |
||
227 |
def is_error(msg: XML.Tree): Boolean = |
|
228 |
msg match { |
|
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
50157
diff
changeset
|
229 |
case XML.Elem(Markup(Markup.ERROR, _), _) => true |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
50157
diff
changeset
|
230 |
case XML.Elem(Markup(Markup.ERROR_MESSAGE, _), _) => true |
39511 | 231 |
case _ => false |
232 |
} |
|
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
|
233 |
|
50500
c94bba7906d2
identify dialogs via official serial and maintain as result message;
wenzelm
parents:
50498
diff
changeset
|
234 |
|
c94bba7906d2
identify dialogs via official serial and maintain as result message;
wenzelm
parents:
50498
diff
changeset
|
235 |
/* dialogs */ |
c94bba7906d2
identify dialogs via official serial and maintain as result message;
wenzelm
parents:
50498
diff
changeset
|
236 |
|
c94bba7906d2
identify dialogs via official serial and maintain as result message;
wenzelm
parents:
50498
diff
changeset
|
237 |
object Dialog_Args |
c94bba7906d2
identify dialogs via official serial and maintain as result message;
wenzelm
parents:
50498
diff
changeset
|
238 |
{ |
52531 | 239 |
def unapply(props: Properties.T): Option[(Document_ID.Generic, Long, String)] = |
50500
c94bba7906d2
identify dialogs via official serial and maintain as result message;
wenzelm
parents:
50498
diff
changeset
|
240 |
(props, props, props) match { |
c94bba7906d2
identify dialogs via official serial and maintain as result message;
wenzelm
parents:
50498
diff
changeset
|
241 |
case (Position.Id(id), Markup.Serial(serial), Markup.Result(result)) => |
c94bba7906d2
identify dialogs via official serial and maintain as result message;
wenzelm
parents:
50498
diff
changeset
|
242 |
Some((id, serial, result)) |
c94bba7906d2
identify dialogs via official serial and maintain as result message;
wenzelm
parents:
50498
diff
changeset
|
243 |
case _ => None |
c94bba7906d2
identify dialogs via official serial and maintain as result message;
wenzelm
parents:
50498
diff
changeset
|
244 |
} |
c94bba7906d2
identify dialogs via official serial and maintain as result message;
wenzelm
parents:
50498
diff
changeset
|
245 |
} |
c94bba7906d2
identify dialogs via official serial and maintain as result message;
wenzelm
parents:
50498
diff
changeset
|
246 |
|
c94bba7906d2
identify dialogs via official serial and maintain as result message;
wenzelm
parents:
50498
diff
changeset
|
247 |
object Dialog |
c94bba7906d2
identify dialogs via official serial and maintain as result message;
wenzelm
parents:
50498
diff
changeset
|
248 |
{ |
52531 | 249 |
def unapply(tree: XML.Tree): Option[(Document_ID.Generic, Long, String)] = |
50500
c94bba7906d2
identify dialogs via official serial and maintain as result message;
wenzelm
parents:
50498
diff
changeset
|
250 |
tree match { |
c94bba7906d2
identify dialogs via official serial and maintain as result message;
wenzelm
parents:
50498
diff
changeset
|
251 |
case XML.Elem(Markup(Markup.DIALOG, Dialog_Args(id, serial, result)), _) => |
c94bba7906d2
identify dialogs via official serial and maintain as result message;
wenzelm
parents:
50498
diff
changeset
|
252 |
Some((id, serial, result)) |
c94bba7906d2
identify dialogs via official serial and maintain as result message;
wenzelm
parents:
50498
diff
changeset
|
253 |
case _ => None |
c94bba7906d2
identify dialogs via official serial and maintain as result message;
wenzelm
parents:
50498
diff
changeset
|
254 |
} |
c94bba7906d2
identify dialogs via official serial and maintain as result message;
wenzelm
parents:
50498
diff
changeset
|
255 |
} |
c94bba7906d2
identify dialogs via official serial and maintain as result message;
wenzelm
parents:
50498
diff
changeset
|
256 |
|
c94bba7906d2
identify dialogs via official serial and maintain as result message;
wenzelm
parents:
50498
diff
changeset
|
257 |
object Dialog_Result |
c94bba7906d2
identify dialogs via official serial and maintain as result message;
wenzelm
parents:
50498
diff
changeset
|
258 |
{ |
52531 | 259 |
def apply(id: Document_ID.Generic, serial: Long, result: String): XML.Elem = |
50501
6f41f1646617
more careful handling of Dialog_Result, with active area and color feedback;
wenzelm
parents:
50500
diff
changeset
|
260 |
{ |
6f41f1646617
more careful handling of Dialog_Result, with active area and color feedback;
wenzelm
parents:
50500
diff
changeset
|
261 |
val props = Position.Id(id) ::: Markup.Serial(serial) |
6f41f1646617
more careful handling of Dialog_Result, with active area and color feedback;
wenzelm
parents:
50500
diff
changeset
|
262 |
XML.Elem(Markup(Markup.RESULT, props), List(XML.Text(result))) |
6f41f1646617
more careful handling of Dialog_Result, with active area and color feedback;
wenzelm
parents:
50500
diff
changeset
|
263 |
} |
50500
c94bba7906d2
identify dialogs via official serial and maintain as result message;
wenzelm
parents:
50498
diff
changeset
|
264 |
|
50501
6f41f1646617
more careful handling of Dialog_Result, with active area and color feedback;
wenzelm
parents:
50500
diff
changeset
|
265 |
def unapply(tree: XML.Tree): Option[String] = |
50500
c94bba7906d2
identify dialogs via official serial and maintain as result message;
wenzelm
parents:
50498
diff
changeset
|
266 |
tree match { |
50501
6f41f1646617
more careful handling of Dialog_Result, with active area and color feedback;
wenzelm
parents:
50500
diff
changeset
|
267 |
case XML.Elem(Markup(Markup.RESULT, _), List(XML.Text(result))) => Some(result) |
50500
c94bba7906d2
identify dialogs via official serial and maintain as result message;
wenzelm
parents:
50498
diff
changeset
|
268 |
case _ => None |
c94bba7906d2
identify dialogs via official serial and maintain as result message;
wenzelm
parents:
50498
diff
changeset
|
269 |
} |
c94bba7906d2
identify dialogs via official serial and maintain as result message;
wenzelm
parents:
50498
diff
changeset
|
270 |
} |
39170
04ad0fed81f5
Isar_Document.reported_positions: exclude proof state output;
wenzelm
parents:
39042
diff
changeset
|
271 |
|
39511 | 272 |
|
273 |
/* reported positions */ |
|
274 |
||
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
50157
diff
changeset
|
275 |
private val include_pos = Set(Markup.BINDING, Markup.ENTITY, Markup.REPORT, Markup.POSITION) |
39441
4110cc1b8f9f
allow embedded reports in regular prover messages, to avoid side-effects for errors for example;
wenzelm
parents:
39439
diff
changeset
|
276 |
|
4110cc1b8f9f
allow embedded reports in regular prover messages, to avoid side-effects for errors for example;
wenzelm
parents:
39439
diff
changeset
|
277 |
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
|
278 |
{ |
49650
9fad6480300d
support for wrapped XML elements, which allows to preserve full markup tree information in to_XML/from_XML conversion;
wenzelm
parents:
49648
diff
changeset
|
279 |
def elem_positions(raw_range: Text.Range, set: Set[Text.Range], body: XML.Body) |
9fad6480300d
support for wrapped XML elements, which allows to preserve full markup tree information in to_XML/from_XML conversion;
wenzelm
parents:
49648
diff
changeset
|
280 |
: Set[Text.Range] = |
9fad6480300d
support for wrapped XML elements, which allows to preserve full markup tree information in to_XML/from_XML conversion;
wenzelm
parents:
49648
diff
changeset
|
281 |
{ |
9fad6480300d
support for wrapped XML elements, which allows to preserve full markup tree information in to_XML/from_XML conversion;
wenzelm
parents:
49648
diff
changeset
|
282 |
val range = command.decode(raw_range).restrict(command.range) |
9fad6480300d
support for wrapped XML elements, which allows to preserve full markup tree information in to_XML/from_XML conversion;
wenzelm
parents:
49648
diff
changeset
|
283 |
body.foldLeft(if (range.is_singularity) set else set + range)(positions) |
9fad6480300d
support for wrapped XML elements, which allows to preserve full markup tree information in to_XML/from_XML conversion;
wenzelm
parents:
49648
diff
changeset
|
284 |
} |
50157 | 285 |
|
39441
4110cc1b8f9f
allow embedded reports in regular prover messages, to avoid side-effects for errors for example;
wenzelm
parents:
39439
diff
changeset
|
286 |
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
|
287 |
tree match { |
49650
9fad6480300d
support for wrapped XML elements, which allows to preserve full markup tree information in to_XML/from_XML conversion;
wenzelm
parents:
49648
diff
changeset
|
288 |
case XML.Wrapped_Elem(Markup(name, Position.Id_Range(id, range)), _, body) |
9fad6480300d
support for wrapped XML elements, which allows to preserve full markup tree information in to_XML/from_XML conversion;
wenzelm
parents:
49648
diff
changeset
|
289 |
if include_pos(name) && id == command.id => elem_positions(range, set, body) |
9fad6480300d
support for wrapped XML elements, which allows to preserve full markup tree information in to_XML/from_XML conversion;
wenzelm
parents:
49648
diff
changeset
|
290 |
|
9fad6480300d
support for wrapped XML elements, which allows to preserve full markup tree information in to_XML/from_XML conversion;
wenzelm
parents:
49648
diff
changeset
|
291 |
case XML.Elem(Markup(name, Position.Id_Range(id, range)), body) |
9fad6480300d
support for wrapped XML elements, which allows to preserve full markup tree information in to_XML/from_XML conversion;
wenzelm
parents:
49648
diff
changeset
|
292 |
if include_pos(name) && id == command.id => elem_positions(range, set, body) |
9fad6480300d
support for wrapped XML elements, which allows to preserve full markup tree information in to_XML/from_XML conversion;
wenzelm
parents:
49648
diff
changeset
|
293 |
|
9fad6480300d
support for wrapped XML elements, which allows to preserve full markup tree information in to_XML/from_XML conversion;
wenzelm
parents:
49648
diff
changeset
|
294 |
case XML.Wrapped_Elem(_, _, body) => body.foldLeft(set)(positions) |
9fad6480300d
support for wrapped XML elements, which allows to preserve full markup tree information in to_XML/from_XML conversion;
wenzelm
parents:
49648
diff
changeset
|
295 |
|
9fad6480300d
support for wrapped XML elements, which allows to preserve full markup tree information in to_XML/from_XML conversion;
wenzelm
parents:
49648
diff
changeset
|
296 |
case XML.Elem(_, body) => body.foldLeft(set)(positions) |
9fad6480300d
support for wrapped XML elements, which allows to preserve full markup tree information in to_XML/from_XML conversion;
wenzelm
parents:
49648
diff
changeset
|
297 |
|
39042
470fd769ae53
Isar_Document.reported_positions: more precise include/exclude, include root as last resort only;
wenzelm
parents:
38887
diff
changeset
|
298 |
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
|
299 |
} |
50157 | 300 |
|
39441
4110cc1b8f9f
allow embedded reports in regular prover messages, to avoid side-effects for errors for example;
wenzelm
parents:
39439
diff
changeset
|
301 |
val set = positions(Set.empty, message) |
50500
c94bba7906d2
identify dialogs via official serial and maintain as result message;
wenzelm
parents:
50498
diff
changeset
|
302 |
if (set.isEmpty) |
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
|
303 |
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
|
304 |
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
|
305 |
} |
38412
c23f3abbf42d
moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff
changeset
|
306 |
} |
c23f3abbf42d
moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff
changeset
|
307 |
|
c23f3abbf42d
moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff
changeset
|
308 |
|
45709
87017fcbad83
clarified modules (again) -- NB: both Document and Protocol are specific to this particular prover;
wenzelm
parents:
45672
diff
changeset
|
309 |
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
|
310 |
{ |
54519
5fed81762406
maintain blobs within document state: digest + text in ML, digest-only in Scala;
wenzelm
parents:
54515
diff
changeset
|
311 |
/* inlined files */ |
5fed81762406
maintain blobs within document state: digest + text in ML, digest-only in Scala;
wenzelm
parents:
54515
diff
changeset
|
312 |
|
5fed81762406
maintain blobs within document state: digest + text in ML, digest-only in Scala;
wenzelm
parents:
54515
diff
changeset
|
313 |
def define_blob(blob: Bytes): Unit = |
5fed81762406
maintain blobs within document state: digest + text in ML, digest-only in Scala;
wenzelm
parents:
54515
diff
changeset
|
314 |
protocol_command_raw("Document.define_blob", Bytes(blob.sha1_digest.toString), blob) |
5fed81762406
maintain blobs within document state: digest + text in ML, digest-only in Scala;
wenzelm
parents:
54515
diff
changeset
|
315 |
|
5fed81762406
maintain blobs within document state: digest + text in ML, digest-only in Scala;
wenzelm
parents:
54515
diff
changeset
|
316 |
|
38412
c23f3abbf42d
moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff
changeset
|
317 |
/* commands */ |
c23f3abbf42d
moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff
changeset
|
318 |
|
44644
317e4962dd0f
clarified define_command: store name as structural information;
wenzelm
parents:
44615
diff
changeset
|
319 |
def define_command(command: Command): Unit = |
54519
5fed81762406
maintain blobs within document state: digest + text in ML, digest-only in Scala;
wenzelm
parents:
54515
diff
changeset
|
320 |
{ |
5fed81762406
maintain blobs within document state: digest + text in ML, digest-only in Scala;
wenzelm
parents:
54515
diff
changeset
|
321 |
val blobs_yxml = |
5fed81762406
maintain blobs within document state: digest + text in ML, digest-only in Scala;
wenzelm
parents:
54515
diff
changeset
|
322 |
{ import XML.Encode._ |
5fed81762406
maintain blobs within document state: digest + text in ML, digest-only in Scala;
wenzelm
parents:
54515
diff
changeset
|
323 |
val encode_blob: T[Command.Blob] = |
5fed81762406
maintain blobs within document state: digest + text in ML, digest-only in Scala;
wenzelm
parents:
54515
diff
changeset
|
324 |
variant(List( |
5fed81762406
maintain blobs within document state: digest + text in ML, digest-only in Scala;
wenzelm
parents:
54515
diff
changeset
|
325 |
{ case Exn.Res((a, b)) => (List(a.node, b.toString), Nil) }, |
5fed81762406
maintain blobs within document state: digest + text in ML, digest-only in Scala;
wenzelm
parents:
54515
diff
changeset
|
326 |
{ case Exn.Exn(e) => (List(Exn.message(e)), Nil) })) |
5fed81762406
maintain blobs within document state: digest + text in ML, digest-only in Scala;
wenzelm
parents:
54515
diff
changeset
|
327 |
YXML.string_of_body(list(encode_blob)(command.blobs)) |
5fed81762406
maintain blobs within document state: digest + text in ML, digest-only in Scala;
wenzelm
parents:
54515
diff
changeset
|
328 |
} |
52582 | 329 |
protocol_command("Document.define_command", |
54519
5fed81762406
maintain blobs within document state: digest + text in ML, digest-only in Scala;
wenzelm
parents:
54515
diff
changeset
|
330 |
Document_ID(command.id), encode(command.name), blobs_yxml, encode(command.source)) |
5fed81762406
maintain blobs within document state: digest + text in ML, digest-only in Scala;
wenzelm
parents:
54515
diff
changeset
|
331 |
} |
38412
c23f3abbf42d
moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff
changeset
|
332 |
|
c23f3abbf42d
moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff
changeset
|
333 |
|
52931
ac6648c0c0fb
cancel_query via direct access to the exec_id of the running query process;
wenzelm
parents:
52862
diff
changeset
|
334 |
/* execution */ |
ac6648c0c0fb
cancel_query via direct access to the exec_id of the running query process;
wenzelm
parents:
52862
diff
changeset
|
335 |
|
ac6648c0c0fb
cancel_query via direct access to the exec_id of the running query process;
wenzelm
parents:
52862
diff
changeset
|
336 |
def discontinue_execution(): Unit = |
ac6648c0c0fb
cancel_query via direct access to the exec_id of the running query process;
wenzelm
parents:
52862
diff
changeset
|
337 |
protocol_command("Document.discontinue_execution") |
38412
c23f3abbf42d
moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff
changeset
|
338 |
|
52931
ac6648c0c0fb
cancel_query via direct access to the exec_id of the running query process;
wenzelm
parents:
52862
diff
changeset
|
339 |
def cancel_exec(id: Document_ID.Exec): Unit = |
ac6648c0c0fb
cancel_query via direct access to the exec_id of the running query process;
wenzelm
parents:
52862
diff
changeset
|
340 |
protocol_command("Document.cancel_exec", Document_ID(id)) |
ac6648c0c0fb
cancel_query via direct access to the exec_id of the running query process;
wenzelm
parents:
52862
diff
changeset
|
341 |
|
ac6648c0c0fb
cancel_query via direct access to the exec_id of the running query process;
wenzelm
parents:
52862
diff
changeset
|
342 |
|
ac6648c0c0fb
cancel_query via direct access to the exec_id of the running query process;
wenzelm
parents:
52862
diff
changeset
|
343 |
/* document versions */ |
47343
b8aeab386414
less aggressive discontinue_execution before document update, to avoid unstable execs that need to be re-assigned;
wenzelm
parents:
46938
diff
changeset
|
344 |
|
52530
99dd8b4ef3fe
explicit module Document_ID as source of globally unique identifiers across ML/Scala;
wenzelm
parents:
52527
diff
changeset
|
345 |
def update(old_id: Document_ID.Version, new_id: Document_ID.Version, |
44383 | 346 |
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
|
347 |
{ |
44157
a21d3e1e64fd
uniform treatment of header edits as document edits;
wenzelm
parents:
44156
diff
changeset
|
348 |
val edits_yxml = |
43767 | 349 |
{ import XML.Encode._ |
44383 | 350 |
def id: T[Command] = (cmd => long(cmd.id)) |
46737 | 351 |
def encode_edit(name: Document.Node.Name) |
52849 | 352 |
: T[Document.Node.Edit[Command.Edit, Command.Perspective]] = |
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
|
353 |
variant(List( |
54509
1f77110c94ef
maintain document model for all files, with document view for theory only, and special blob for non-theory files;
wenzelm
parents:
52931
diff
changeset
|
354 |
// FIXME Document.Node.Blob (!??) |
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
|
355 |
{ 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
|
356 |
{ 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
|
357 |
{ case Document.Node.Deps(header) => |
54515 | 358 |
val master_dir = Isabelle_System.posix_path(name.master_dir) |
48707
ba531af91148
simplified Document.Node.Header -- internalized errors;
wenzelm
parents:
48705
diff
changeset
|
359 |
val imports = header.imports.map(_.node) |
50128
599c935aac82
alternative completion for outer syntax keywords;
wenzelm
parents:
49650
diff
changeset
|
360 |
val keywords = header.keywords.map({ case (a, b, _) => (a, b) }) |
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
|
361 |
(Nil, |
48707
ba531af91148
simplified Document.Node.Header -- internalized errors;
wenzelm
parents:
48705
diff
changeset
|
362 |
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
|
363 |
pair(list(pair(Encode.string, |
3ee314ae1e0a
added keyword kind "thy_load" (with optional list of file extensions);
wenzelm
parents:
48755
diff
changeset
|
364 |
option(pair(pair(Encode.string, list(Encode.string)), list(Encode.string))))), |
51294
0850d43cb355
discontinued obsolete header "files" -- these are loaded explicitly after exploring dependencies;
wenzelm
parents:
51293
diff
changeset
|
365 |
list(Encode.string)))))( |
54515 | 366 |
(master_dir, (name.theory, (imports, (keywords, header.errors)))))) }, |
52849 | 367 |
{ case Document.Node.Perspective(a, b, c) => |
368 |
(bool_atom(a) :: b.commands.map(cmd => long_atom(cmd.id)), |
|
52862
930ce8eacb87
tuned signature -- more uniform treatment of overlays as command mapping;
wenzelm
parents:
52849
diff
changeset
|
369 |
list(pair(id, pair(Encode.string, list(Encode.string))))(c.dest)) })) |
48705
dd32321d6eef
tuned signature -- slightly more abstract text representation of prover process;
wenzelm
parents:
47542
diff
changeset
|
370 |
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
|
371 |
{ |
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
|
372 |
val (name, edit) = node_edit |
46737 | 373 |
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
|
374 |
}) |
48705
dd32321d6eef
tuned signature -- slightly more abstract text representation of prover process;
wenzelm
parents:
47542
diff
changeset
|
375 |
YXML.string_of_body(encode_edits(edits)) } |
52582 | 376 |
protocol_command("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
|
377 |
} |
43748 | 378 |
|
44673 | 379 |
def remove_versions(versions: List[Document.Version]) |
380 |
{ |
|
381 |
val versions_yxml = |
|
382 |
{ import XML.Encode._ |
|
383 |
YXML.string_of_body(list(long)(versions.map(_.id))) } |
|
52582 | 384 |
protocol_command("Document.remove_versions", versions_yxml) |
44673 | 385 |
} |
386 |
||
43748 | 387 |
|
50498 | 388 |
/* dialog via document content */ |
389 |
||
52931
ac6648c0c0fb
cancel_query via direct access to the exec_id of the running query process;
wenzelm
parents:
52862
diff
changeset
|
390 |
def dialog_result(serial: Long, result: String): Unit = |
52582 | 391 |
protocol_command("Document.dialog_result", Properties.Value.Long(serial), result) |
38412
c23f3abbf42d
moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff
changeset
|
392 |
} |