author | wenzelm |
Sun, 04 Mar 2012 18:15:45 +0100 | |
changeset 46812 | 3d55ef732cd7 |
parent 46770 | 44c28a33c461 |
child 46910 | 3e068ef04b42 |
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) |
383c9d758a56
raw message function "assign_execs" avoids full overhead of decoding and caching message body;
wenzelm
parents:
44644
diff
changeset
|
20 |
Some(pair(long, pair(list(pair(long, option(long))), list(pair(string, option(long)))))(body)) |
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( |
52 |
private val finished: Boolean = false, |
|
53 |
private val failed: Boolean = false, |
|
54 |
forks: Int = 0) |
|
38567
b670faa807c9
concentrate protocol message formats in Isar_Document;
wenzelm
parents:
38483
diff
changeset
|
55 |
{ |
46166 | 56 |
def is_unprocessed: Boolean = !finished && !failed && forks == 0 |
57 |
def is_running: Boolean = forks != 0 |
|
58 |
def is_finished: Boolean = finished && forks == 0 |
|
59 |
def is_failed: Boolean = failed && forks == 0 |
|
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
|
60 |
def + (that: Status): 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
|
61 |
Status(finished || that.finished, failed || that.failed, forks + that.forks) |
46166 | 62 |
} |
63 |
||
64 |
val command_status_markup: Set[String] = |
|
65 |
Set(Isabelle_Markup.FINISHED, Isabelle_Markup.FAILED, |
|
66 |
Isabelle_Markup.FORKED, Isabelle_Markup.JOINED) |
|
67 |
||
68 |
def command_status(status: Status, markup: Markup): Status = |
|
69 |
markup match { |
|
70 |
case Markup(Isabelle_Markup.FINISHED, _) => status.copy(finished = true) |
|
71 |
case Markup(Isabelle_Markup.FAILED, _) => status.copy(failed = true) |
|
72 |
case Markup(Isabelle_Markup.FORKED, _) => status.copy(forks = status.forks + 1) |
|
73 |
case Markup(Isabelle_Markup.JOINED, _) => status.copy(forks = status.forks - 1) |
|
74 |
case _ => status |
|
38567
b670faa807c9
concentrate protocol message formats in Isar_Document;
wenzelm
parents:
38483
diff
changeset
|
75 |
} |
46166 | 76 |
|
77 |
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
|
78 |
(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
|
79 |
|
46209 | 80 |
|
81 |
/* node status */ |
|
82 |
||
46688 | 83 |
sealed case class Node_Status( |
84 |
unprocessed: Int, running: Int, finished: Int, warned: Int, failed: Int) |
|
44866 | 85 |
{ |
46688 | 86 |
def total: Int = unprocessed + running + finished + warned + failed |
44866 | 87 |
} |
44613 | 88 |
|
89 |
def node_status( |
|
90 |
state: Document.State, version: Document.Version, node: Document.Node): Node_Status = |
|
91 |
{ |
|
92 |
var unprocessed = 0 |
|
93 |
var running = 0 |
|
94 |
var finished = 0 |
|
46688 | 95 |
var warned = 0 |
44613 | 96 |
var failed = 0 |
97 |
node.commands.foreach(command => |
|
46166 | 98 |
{ |
46688 | 99 |
val st = state.command_state(version, command) |
100 |
val status = command_status(st.status) |
|
46166 | 101 |
if (status.is_running) running += 1 |
46688 | 102 |
else if (status.is_finished) { |
103 |
if (st.results.exists(p => is_warning(p._2))) warned += 1 |
|
104 |
else finished += 1 |
|
105 |
} |
|
46166 | 106 |
else if (status.is_failed) failed += 1 |
107 |
else unprocessed += 1 |
|
44613 | 108 |
}) |
46688 | 109 |
Node_Status(unprocessed, running, finished, warned, failed) |
44613 | 110 |
} |
111 |
||
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
|
112 |
|
39441
4110cc1b8f9f
allow embedded reports in regular prover messages, to avoid side-effects for errors for example;
wenzelm
parents:
39439
diff
changeset
|
113 |
/* 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
|
114 |
|
1c294d150ded
eliminated markup "location" in favour of more explicit "no_report", which is actually deleted from messages;
wenzelm
parents:
39181
diff
changeset
|
115 |
def clean_message(body: XML.Body): XML.Body = |
45666 | 116 |
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
|
117 |
{ 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
|
118 |
|
39441
4110cc1b8f9f
allow embedded reports in regular prover messages, to avoid side-effects for errors for example;
wenzelm
parents:
39439
diff
changeset
|
119 |
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
|
120 |
msg match { |
45666 | 121 |
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
|
122 |
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
|
123 |
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
|
124 |
} |
4110cc1b8f9f
allow embedded reports in regular prover messages, to avoid side-effects for errors for example;
wenzelm
parents:
39439
diff
changeset
|
125 |
|
39439
1c294d150ded
eliminated markup "location" in favour of more explicit "no_report", which is actually deleted from messages;
wenzelm
parents:
39181
diff
changeset
|
126 |
|
39511 | 127 |
/* specific messages */ |
128 |
||
39625 | 129 |
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
|
130 |
msg match { |
45666 | 131 |
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
|
132 |
case _ => false |
53365ba766ac
Command.accumulate: refrain from adding tracing messages to markup tree -- potential scalability problem;
wenzelm
parents:
39511
diff
changeset
|
133 |
} |
53365ba766ac
Command.accumulate: refrain from adding tracing messages to markup tree -- potential scalability problem;
wenzelm
parents:
39511
diff
changeset
|
134 |
|
39511 | 135 |
def is_warning(msg: XML.Tree): Boolean = |
136 |
msg match { |
|
45666 | 137 |
case XML.Elem(Markup(Isabelle_Markup.WARNING, _), _) => true |
39511 | 138 |
case _ => false |
139 |
} |
|
140 |
||
141 |
def is_error(msg: XML.Tree): Boolean = |
|
142 |
msg match { |
|
45666 | 143 |
case XML.Elem(Markup(Isabelle_Markup.ERROR, _), _) => true |
39511 | 144 |
case _ => false |
145 |
} |
|
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
|
146 |
|
39441
4110cc1b8f9f
allow embedded reports in regular prover messages, to avoid side-effects for errors for example;
wenzelm
parents:
39439
diff
changeset
|
147 |
def is_state(msg: XML.Tree): Boolean = |
39170
04ad0fed81f5
Isar_Document.reported_positions: exclude proof state output;
wenzelm
parents:
39042
diff
changeset
|
148 |
msg match { |
45666 | 149 |
case XML.Elem(Markup(Isabelle_Markup.WRITELN, _), |
150 |
List(XML.Elem(Markup(Isabelle_Markup.STATE, _), _))) => true |
|
39170
04ad0fed81f5
Isar_Document.reported_positions: exclude proof state output;
wenzelm
parents:
39042
diff
changeset
|
151 |
case _ => false |
04ad0fed81f5
Isar_Document.reported_positions: exclude proof state output;
wenzelm
parents:
39042
diff
changeset
|
152 |
} |
04ad0fed81f5
Isar_Document.reported_positions: exclude proof state output;
wenzelm
parents:
39042
diff
changeset
|
153 |
|
39511 | 154 |
|
155 |
/* reported positions */ |
|
156 |
||
39627 | 157 |
private val include_pos = |
45666 | 158 |
Set(Isabelle_Markup.BINDING, Isabelle_Markup.ENTITY, Isabelle_Markup.REPORT, |
159 |
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
|
160 |
|
4110cc1b8f9f
allow embedded reports in regular prover messages, to avoid side-effects for errors for example;
wenzelm
parents:
39439
diff
changeset
|
161 |
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
|
162 |
{ |
39441
4110cc1b8f9f
allow embedded reports in regular prover messages, to avoid side-effects for errors for example;
wenzelm
parents:
39439
diff
changeset
|
163 |
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
|
164 |
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
|
165 |
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
|
166 |
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
|
167 |
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
|
168 |
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
|
169 |
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
|
170 |
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
|
171 |
} |
39441
4110cc1b8f9f
allow embedded reports in regular prover messages, to avoid side-effects for errors for example;
wenzelm
parents:
39439
diff
changeset
|
172 |
val set = positions(Set.empty, message) |
39170
04ad0fed81f5
Isar_Document.reported_positions: exclude proof state output;
wenzelm
parents:
39042
diff
changeset
|
173 |
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
|
174 |
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
|
175 |
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
|
176 |
} |
38412
c23f3abbf42d
moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff
changeset
|
177 |
} |
c23f3abbf42d
moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff
changeset
|
178 |
|
c23f3abbf42d
moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff
changeset
|
179 |
|
45709
87017fcbad83
clarified modules (again) -- NB: both Document and Protocol are specific to this particular prover;
wenzelm
parents:
45672
diff
changeset
|
180 |
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
|
181 |
{ |
c23f3abbf42d
moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff
changeset
|
182 |
/* commands */ |
c23f3abbf42d
moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff
changeset
|
183 |
|
44644
317e4962dd0f
clarified define_command: store name as structural information;
wenzelm
parents:
44615
diff
changeset
|
184 |
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
|
185 |
input("Document.define_command", |
44644
317e4962dd0f
clarified define_command: store name as structural information;
wenzelm
parents:
44615
diff
changeset
|
186 |
Document.ID(command.id), Symbol.encode(command.name), Symbol.encode(command.source)) |
38412
c23f3abbf42d
moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff
changeset
|
187 |
|
c23f3abbf42d
moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff
changeset
|
188 |
|
38417 | 189 |
/* document versions */ |
38412
c23f3abbf42d
moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff
changeset
|
190 |
|
44612
990ac978854c
explicit cancel_execution before queueing new edits -- potential performance improvement for machines with few cores;
wenzelm
parents:
44481
diff
changeset
|
191 |
def cancel_execution() |
990ac978854c
explicit cancel_execution before queueing new edits -- potential performance improvement for machines with few cores;
wenzelm
parents:
44481
diff
changeset
|
192 |
{ |
45709
87017fcbad83
clarified modules (again) -- NB: both Document and Protocol are specific to this particular prover;
wenzelm
parents:
45672
diff
changeset
|
193 |
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
|
194 |
} |
990ac978854c
explicit cancel_execution before queueing new edits -- potential performance improvement for machines with few cores;
wenzelm
parents:
44481
diff
changeset
|
195 |
|
44436
546adfa8a6fc
update_perspective without actual edits, bypassing the full state assignment protocol;
wenzelm
parents:
44384
diff
changeset
|
196 |
def update_perspective(old_id: Document.Version_ID, new_id: Document.Version_ID, |
44615 | 197 |
name: Document.Node.Name, perspective: Command.Perspective) |
44436
546adfa8a6fc
update_perspective without actual edits, bypassing the full state assignment protocol;
wenzelm
parents:
44384
diff
changeset
|
198 |
{ |
546adfa8a6fc
update_perspective without actual edits, bypassing the full state assignment protocol;
wenzelm
parents:
44384
diff
changeset
|
199 |
val ids = |
546adfa8a6fc
update_perspective without actual edits, bypassing the full state assignment protocol;
wenzelm
parents:
44384
diff
changeset
|
200 |
{ import XML.Encode._ |
44474 | 201 |
list(long)(perspective.commands.map(_.id)) } |
44436
546adfa8a6fc
update_perspective without actual edits, bypassing the full state assignment protocol;
wenzelm
parents:
44384
diff
changeset
|
202 |
|
45709
87017fcbad83
clarified modules (again) -- NB: both Document and Protocol are specific to this particular prover;
wenzelm
parents:
45672
diff
changeset
|
203 |
input("Document.update_perspective", Document.ID(old_id), Document.ID(new_id), |
44615 | 204 |
name.node, YXML.string_of_body(ids)) |
44436
546adfa8a6fc
update_perspective without actual edits, bypassing the full state assignment protocol;
wenzelm
parents:
44384
diff
changeset
|
205 |
} |
546adfa8a6fc
update_perspective without actual edits, bypassing the full state assignment protocol;
wenzelm
parents:
44384
diff
changeset
|
206 |
|
44481 | 207 |
def update(old_id: Document.Version_ID, new_id: Document.Version_ID, |
44383 | 208 |
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
|
209 |
{ |
44157
a21d3e1e64fd
uniform treatment of header edits as document edits;
wenzelm
parents:
44156
diff
changeset
|
210 |
val edits_yxml = |
43767 | 211 |
{ import XML.Encode._ |
44383 | 212 |
def id: T[Command] = (cmd => long(cmd.id)) |
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
|
213 |
def symbol_string: T[String] = (s => string(Symbol.encode(s))) |
46737 | 214 |
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
|
215 |
: 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
|
216 |
variant(List( |
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 |
{ case Document.Node.Clear() => (Nil, Nil) }, |
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 |
{ case Document.Node.Edits(a) => (Nil, list(pair(option(id), option(id)))(a)) }, |
46737 | 219 |
{ case Document.Node.Header(Exn.Res(deps)) => |
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
|
220 |
val dir = Isabelle_System.posix_path(name.dir) |
46737 | 221 |
val imports = deps.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
|
222 |
// FIXME val uses = deps.uses.map(p => (Isabelle_System.posix_path(p._1), p._2)) |
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
|
223 |
val uses = deps.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
|
224 |
(Nil, |
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
|
225 |
triple(pair(symbol_string, symbol_string), list(symbol_string), |
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
|
226 |
list(pair(symbol_string, bool)))((dir, name.theory), imports, uses)) }, |
46755 | 227 |
{ case Document.Node.Header(Exn.Exn(e)) => (List(Symbol.encode(Exn.message(e))), Nil) }, |
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
|
228 |
{ case Document.Node.Perspective(a) => (a.commands.map(c => long_atom(c.id)), Nil) })) |
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
|
229 |
def encode: T[List[Document.Edit_Command]] = list((node_edit: Document.Edit_Command) => |
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
|
230 |
{ |
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
|
231 |
val (name, edit) = node_edit |
46737 | 232 |
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
|
233 |
}) |
44157
a21d3e1e64fd
uniform treatment of header edits as document edits;
wenzelm
parents:
44156
diff
changeset
|
234 |
YXML.string_of_body(encode(edits)) } |
45709
87017fcbad83
clarified modules (again) -- NB: both Document and Protocol are specific to this particular prover;
wenzelm
parents:
45672
diff
changeset
|
235 |
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
|
236 |
} |
43748 | 237 |
|
44673 | 238 |
def remove_versions(versions: List[Document.Version]) |
239 |
{ |
|
240 |
val versions_yxml = |
|
241 |
{ import XML.Encode._ |
|
242 |
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
|
243 |
input("Document.remove_versions", versions_yxml) |
44673 | 244 |
} |
245 |
||
43748 | 246 |
|
247 |
/* method invocation service */ |
|
248 |
||
249 |
def invoke_scala(id: String, tag: Invoke_Scala.Tag.Value, res: String) |
|
250 |
{ |
|
45709
87017fcbad83
clarified modules (again) -- NB: both Document and Protocol are specific to this particular prover;
wenzelm
parents:
45672
diff
changeset
|
251 |
input("Document.invoke_scala", id, tag.toString, res) |
43748 | 252 |
} |
38412
c23f3abbf42d
moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff
changeset
|
253 |
} |