author | wenzelm |
Tue, 05 Jun 2018 16:12:26 +0200 | |
changeset 68381 | 2fd3a6d6ba2e |
parent 68336 | 09ac56914b29 |
child 68758 | a110e7e24e55 |
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._ |
65345
2fdd4431b30e
clarified YXML vs. symbol encoding: operate on whole message;
wenzelm
parents:
65313
diff
changeset
|
19 |
Some(pair(long, list(pair(long, list(long))))(Symbol.decode_yxml(text))) |
44661
383c9d758a56
raw message function "assign_execs" avoids full overhead of decoding and caching message body;
wenzelm
parents:
44644
diff
changeset
|
20 |
} |
383c9d758a56
raw message function "assign_execs" avoids full overhead of decoding and caching message body;
wenzelm
parents:
44644
diff
changeset
|
21 |
catch { |
383c9d758a56
raw message function "assign_execs" avoids full overhead of decoding and caching message body;
wenzelm
parents:
44644
diff
changeset
|
22 |
case ERROR(_) => None |
51987 | 23 |
case _: XML.Error => None |
38412
c23f3abbf42d
moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff
changeset
|
24 |
} |
c23f3abbf42d
moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff
changeset
|
25 |
} |
38567
b670faa807c9
concentrate protocol message formats in Isar_Document;
wenzelm
parents:
38483
diff
changeset
|
26 |
|
44676 | 27 |
object Removed |
28 |
{ |
|
52530
99dd8b4ef3fe
explicit module Document_ID as source of globally unique identifiers across ML/Scala;
wenzelm
parents:
52527
diff
changeset
|
29 |
def unapply(text: String): Option[List[Document_ID.Version]] = |
44676 | 30 |
try { |
31 |
import XML.Decode._ |
|
65345
2fdd4431b30e
clarified YXML vs. symbol encoding: operate on whole message;
wenzelm
parents:
65313
diff
changeset
|
32 |
Some(list(long)(Symbol.decode_yxml(text))) |
44676 | 33 |
} |
34 |
catch { |
|
35 |
case ERROR(_) => None |
|
51987 | 36 |
case _: XML.Error => None |
44676 | 37 |
} |
38 |
} |
|
39 |
||
38567
b670faa807c9
concentrate protocol message formats in Isar_Document;
wenzelm
parents:
38483
diff
changeset
|
40 |
|
68381
2fd3a6d6ba2e
less wasteful consolidation, based on PIDE front-end state and recent changes;
wenzelm
parents:
68336
diff
changeset
|
41 |
/* consolidation status */ |
2fd3a6d6ba2e
less wasteful consolidation, based on PIDE front-end state and recent changes;
wenzelm
parents:
68336
diff
changeset
|
42 |
|
2fd3a6d6ba2e
less wasteful consolidation, based on PIDE front-end state and recent changes;
wenzelm
parents:
68336
diff
changeset
|
43 |
def maybe_consolidated(markups: List[Markup]): Boolean = |
2fd3a6d6ba2e
less wasteful consolidation, based on PIDE front-end state and recent changes;
wenzelm
parents:
68336
diff
changeset
|
44 |
{ |
2fd3a6d6ba2e
less wasteful consolidation, based on PIDE front-end state and recent changes;
wenzelm
parents:
68336
diff
changeset
|
45 |
var touched = false |
2fd3a6d6ba2e
less wasteful consolidation, based on PIDE front-end state and recent changes;
wenzelm
parents:
68336
diff
changeset
|
46 |
var forks = 0 |
2fd3a6d6ba2e
less wasteful consolidation, based on PIDE front-end state and recent changes;
wenzelm
parents:
68336
diff
changeset
|
47 |
var runs = 0 |
2fd3a6d6ba2e
less wasteful consolidation, based on PIDE front-end state and recent changes;
wenzelm
parents:
68336
diff
changeset
|
48 |
for (markup <- markups) { |
2fd3a6d6ba2e
less wasteful consolidation, based on PIDE front-end state and recent changes;
wenzelm
parents:
68336
diff
changeset
|
49 |
markup.name match { |
2fd3a6d6ba2e
less wasteful consolidation, based on PIDE front-end state and recent changes;
wenzelm
parents:
68336
diff
changeset
|
50 |
case Markup.FORKED => touched = true; forks += 1 |
2fd3a6d6ba2e
less wasteful consolidation, based on PIDE front-end state and recent changes;
wenzelm
parents:
68336
diff
changeset
|
51 |
case Markup.JOINED => forks -= 1 |
2fd3a6d6ba2e
less wasteful consolidation, based on PIDE front-end state and recent changes;
wenzelm
parents:
68336
diff
changeset
|
52 |
case Markup.RUNNING => touched = true; runs += 1 |
2fd3a6d6ba2e
less wasteful consolidation, based on PIDE front-end state and recent changes;
wenzelm
parents:
68336
diff
changeset
|
53 |
case Markup.FINISHED => runs -= 1 |
2fd3a6d6ba2e
less wasteful consolidation, based on PIDE front-end state and recent changes;
wenzelm
parents:
68336
diff
changeset
|
54 |
case _ => |
2fd3a6d6ba2e
less wasteful consolidation, based on PIDE front-end state and recent changes;
wenzelm
parents:
68336
diff
changeset
|
55 |
} |
2fd3a6d6ba2e
less wasteful consolidation, based on PIDE front-end state and recent changes;
wenzelm
parents:
68336
diff
changeset
|
56 |
} |
2fd3a6d6ba2e
less wasteful consolidation, based on PIDE front-end state and recent changes;
wenzelm
parents:
68336
diff
changeset
|
57 |
touched && forks == 0 && runs == 0 |
2fd3a6d6ba2e
less wasteful consolidation, based on PIDE front-end state and recent changes;
wenzelm
parents:
68336
diff
changeset
|
58 |
} |
2fd3a6d6ba2e
less wasteful consolidation, based on PIDE front-end state and recent changes;
wenzelm
parents:
68336
diff
changeset
|
59 |
|
2fd3a6d6ba2e
less wasteful consolidation, based on PIDE front-end state and recent changes;
wenzelm
parents:
68336
diff
changeset
|
60 |
|
46209 | 61 |
/* command status */ |
38567
b670faa807c9
concentrate protocol message formats in Isar_Document;
wenzelm
parents:
38483
diff
changeset
|
62 |
|
56359
bca016a9a18d
persistent protocol_status, to improve performance of node_status a little;
wenzelm
parents:
56356
diff
changeset
|
63 |
object Status |
bca016a9a18d
persistent protocol_status, to improve performance of node_status a little;
wenzelm
parents:
56356
diff
changeset
|
64 |
{ |
bca016a9a18d
persistent protocol_status, to improve performance of node_status a little;
wenzelm
parents:
56356
diff
changeset
|
65 |
def make(markup_iterator: Iterator[Markup]): Status = |
bca016a9a18d
persistent protocol_status, to improve performance of node_status a little;
wenzelm
parents:
56356
diff
changeset
|
66 |
{ |
bca016a9a18d
persistent protocol_status, to improve performance of node_status a little;
wenzelm
parents:
56356
diff
changeset
|
67 |
var touched = false |
bca016a9a18d
persistent protocol_status, to improve performance of node_status a little;
wenzelm
parents:
56356
diff
changeset
|
68 |
var accepted = false |
56395
0546e036d1c0
more direct warning within persistent Protocol.Status;
wenzelm
parents:
56387
diff
changeset
|
69 |
var warned = false |
56359
bca016a9a18d
persistent protocol_status, to improve performance of node_status a little;
wenzelm
parents:
56356
diff
changeset
|
70 |
var failed = false |
bca016a9a18d
persistent protocol_status, to improve performance of node_status a little;
wenzelm
parents:
56356
diff
changeset
|
71 |
var forks = 0 |
bca016a9a18d
persistent protocol_status, to improve performance of node_status a little;
wenzelm
parents:
56356
diff
changeset
|
72 |
var runs = 0 |
bca016a9a18d
persistent protocol_status, to improve performance of node_status a little;
wenzelm
parents:
56356
diff
changeset
|
73 |
for (markup <- markup_iterator) { |
bca016a9a18d
persistent protocol_status, to improve performance of node_status a little;
wenzelm
parents:
56356
diff
changeset
|
74 |
markup.name match { |
bca016a9a18d
persistent protocol_status, to improve performance of node_status a little;
wenzelm
parents:
56356
diff
changeset
|
75 |
case Markup.ACCEPTED => accepted = true |
bca016a9a18d
persistent protocol_status, to improve performance of node_status a little;
wenzelm
parents:
56356
diff
changeset
|
76 |
case Markup.FORKED => touched = true; forks += 1 |
bca016a9a18d
persistent protocol_status, to improve performance of node_status a little;
wenzelm
parents:
56356
diff
changeset
|
77 |
case Markup.JOINED => forks -= 1 |
bca016a9a18d
persistent protocol_status, to improve performance of node_status a little;
wenzelm
parents:
56356
diff
changeset
|
78 |
case Markup.RUNNING => touched = true; runs += 1 |
bca016a9a18d
persistent protocol_status, to improve performance of node_status a little;
wenzelm
parents:
56356
diff
changeset
|
79 |
case Markup.FINISHED => runs -= 1 |
59203
5f0bd5afc16d
explicit message channel for "legacy", which is nonetheless a variant of "warning";
wenzelm
parents:
59184
diff
changeset
|
80 |
case Markup.WARNING | Markup.LEGACY => warned = true |
56395
0546e036d1c0
more direct warning within persistent Protocol.Status;
wenzelm
parents:
56387
diff
changeset
|
81 |
case Markup.FAILED | Markup.ERROR => failed = true |
56359
bca016a9a18d
persistent protocol_status, to improve performance of node_status a little;
wenzelm
parents:
56356
diff
changeset
|
82 |
case _ => |
bca016a9a18d
persistent protocol_status, to improve performance of node_status a little;
wenzelm
parents:
56356
diff
changeset
|
83 |
} |
bca016a9a18d
persistent protocol_status, to improve performance of node_status a little;
wenzelm
parents:
56356
diff
changeset
|
84 |
} |
56395
0546e036d1c0
more direct warning within persistent Protocol.Status;
wenzelm
parents:
56387
diff
changeset
|
85 |
Status(touched, accepted, warned, failed, forks, runs) |
56359
bca016a9a18d
persistent protocol_status, to improve performance of node_status a little;
wenzelm
parents:
56356
diff
changeset
|
86 |
} |
bca016a9a18d
persistent protocol_status, to improve performance of node_status a little;
wenzelm
parents:
56356
diff
changeset
|
87 |
|
bca016a9a18d
persistent protocol_status, to improve performance of node_status a little;
wenzelm
parents:
56356
diff
changeset
|
88 |
val empty = make(Iterator.empty) |
bca016a9a18d
persistent protocol_status, to improve performance of node_status a little;
wenzelm
parents:
56356
diff
changeset
|
89 |
|
bca016a9a18d
persistent protocol_status, to improve performance of node_status a little;
wenzelm
parents:
56356
diff
changeset
|
90 |
def merge(status_iterator: Iterator[Status]): Status = |
bca016a9a18d
persistent protocol_status, to improve performance of node_status a little;
wenzelm
parents:
56356
diff
changeset
|
91 |
if (status_iterator.hasNext) { |
bca016a9a18d
persistent protocol_status, to improve performance of node_status a little;
wenzelm
parents:
56356
diff
changeset
|
92 |
val status0 = status_iterator.next |
bca016a9a18d
persistent protocol_status, to improve performance of node_status a little;
wenzelm
parents:
56356
diff
changeset
|
93 |
(status0 /: status_iterator)(_ + _) |
bca016a9a18d
persistent protocol_status, to improve performance of node_status a little;
wenzelm
parents:
56356
diff
changeset
|
94 |
} |
bca016a9a18d
persistent protocol_status, to improve performance of node_status a little;
wenzelm
parents:
56356
diff
changeset
|
95 |
else empty |
bca016a9a18d
persistent protocol_status, to improve performance of node_status a little;
wenzelm
parents:
56356
diff
changeset
|
96 |
} |
bca016a9a18d
persistent protocol_status, to improve performance of node_status a little;
wenzelm
parents:
56356
diff
changeset
|
97 |
|
46166 | 98 |
sealed case class Status( |
56352
abdc524db8b4
more frugal command_status, which is often used in a tight loop;
wenzelm
parents:
56335
diff
changeset
|
99 |
private val touched: Boolean, |
abdc524db8b4
more frugal command_status, which is often used in a tight loop;
wenzelm
parents:
56335
diff
changeset
|
100 |
private val accepted: Boolean, |
56395
0546e036d1c0
more direct warning within persistent Protocol.Status;
wenzelm
parents:
56387
diff
changeset
|
101 |
private val warned: Boolean, |
56352
abdc524db8b4
more frugal command_status, which is often used in a tight loop;
wenzelm
parents:
56335
diff
changeset
|
102 |
private val failed: Boolean, |
abdc524db8b4
more frugal command_status, which is often used in a tight loop;
wenzelm
parents:
56335
diff
changeset
|
103 |
forks: Int, |
abdc524db8b4
more frugal command_status, which is often used in a tight loop;
wenzelm
parents:
56335
diff
changeset
|
104 |
runs: Int) |
38567
b670faa807c9
concentrate protocol message formats in Isar_Document;
wenzelm
parents:
38483
diff
changeset
|
105 |
{ |
56359
bca016a9a18d
persistent protocol_status, to improve performance of node_status a little;
wenzelm
parents:
56356
diff
changeset
|
106 |
def + (that: Status): Status = |
56395
0546e036d1c0
more direct warning within persistent Protocol.Status;
wenzelm
parents:
56387
diff
changeset
|
107 |
Status( |
0546e036d1c0
more direct warning within persistent Protocol.Status;
wenzelm
parents:
56387
diff
changeset
|
108 |
touched || that.touched, |
0546e036d1c0
more direct warning within persistent Protocol.Status;
wenzelm
parents:
56387
diff
changeset
|
109 |
accepted || that.accepted, |
0546e036d1c0
more direct warning within persistent Protocol.Status;
wenzelm
parents:
56387
diff
changeset
|
110 |
warned || that.warned, |
0546e036d1c0
more direct warning within persistent Protocol.Status;
wenzelm
parents:
56387
diff
changeset
|
111 |
failed || that.failed, |
0546e036d1c0
more direct warning within persistent Protocol.Status;
wenzelm
parents:
56387
diff
changeset
|
112 |
forks + that.forks, |
0546e036d1c0
more direct warning within persistent Protocol.Status;
wenzelm
parents:
56387
diff
changeset
|
113 |
runs + that.runs) |
56359
bca016a9a18d
persistent protocol_status, to improve performance of node_status a little;
wenzelm
parents:
56356
diff
changeset
|
114 |
|
49036
4680c4046814
further refinement of command status, to accomodate forked proofs;
wenzelm
parents:
49009
diff
changeset
|
115 |
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
|
116 |
def is_running: Boolean = runs != 0 |
56474
4df2727a0b5f
more direct interpretation of "warned" status, like "failed" and independently of "finished", e.g. relevant for Rendering.overview_color of aux. files where main command status is unavailable (amending 0546e036d1c0);
wenzelm
parents:
56470
diff
changeset
|
117 |
def is_warned: Boolean = warned |
4df2727a0b5f
more direct interpretation of "warned" status, like "failed" and independently of "finished", e.g. relevant for Rendering.overview_color of aux. files where main command status is unavailable (amending 0546e036d1c0);
wenzelm
parents:
56470
diff
changeset
|
118 |
def is_failed: Boolean = failed |
49039 | 119 |
def is_finished: Boolean = !failed && touched && forks == 0 && runs == 0 |
46166 | 120 |
} |
121 |
||
56395
0546e036d1c0
more direct warning within persistent Protocol.Status;
wenzelm
parents:
56387
diff
changeset
|
122 |
val proper_status_elements = |
56743 | 123 |
Markup.Elements(Markup.ACCEPTED, Markup.FORKED, Markup.JOINED, Markup.RUNNING, |
55646 | 124 |
Markup.FINISHED, Markup.FAILED) |
125 |
||
56395
0546e036d1c0
more direct warning within persistent Protocol.Status;
wenzelm
parents:
56387
diff
changeset
|
126 |
val liberal_status_elements = |
59203
5f0bd5afc16d
explicit message channel for "legacy", which is nonetheless a variant of "warning";
wenzelm
parents:
59184
diff
changeset
|
127 |
proper_status_elements + Markup.WARNING + Markup.LEGACY + Markup.ERROR |
55646 | 128 |
|
46209 | 129 |
|
51818
517f232e867d
clarified module dependencies: avoid Properties and Document introding minimal "PIDE";
wenzelm
parents:
51533
diff
changeset
|
130 |
/* command timing */ |
517f232e867d
clarified module dependencies: avoid Properties and Document introding minimal "PIDE";
wenzelm
parents:
51533
diff
changeset
|
131 |
|
517f232e867d
clarified module dependencies: avoid Properties and Document introding minimal "PIDE";
wenzelm
parents:
51533
diff
changeset
|
132 |
object Command_Timing |
517f232e867d
clarified module dependencies: avoid Properties and Document introding minimal "PIDE";
wenzelm
parents:
51533
diff
changeset
|
133 |
{ |
52531 | 134 |
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
|
135 |
props match { |
66873
9953ae603a23
provide theory timing information, similar to command timing but always considered relevant;
wenzelm
parents:
66717
diff
changeset
|
136 |
case Markup.COMMAND_TIMING :: args => |
51818
517f232e867d
clarified module dependencies: avoid Properties and Document introding minimal "PIDE";
wenzelm
parents:
51533
diff
changeset
|
137 |
(args, args) match { |
517f232e867d
clarified module dependencies: avoid Properties and Document introding minimal "PIDE";
wenzelm
parents:
51533
diff
changeset
|
138 |
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
|
139 |
case _ => None |
517f232e867d
clarified module dependencies: avoid Properties and Document introding minimal "PIDE";
wenzelm
parents:
51533
diff
changeset
|
140 |
} |
517f232e867d
clarified module dependencies: avoid Properties and Document introding minimal "PIDE";
wenzelm
parents:
51533
diff
changeset
|
141 |
case _ => None |
517f232e867d
clarified module dependencies: avoid Properties and Document introding minimal "PIDE";
wenzelm
parents:
51533
diff
changeset
|
142 |
} |
517f232e867d
clarified module dependencies: avoid Properties and Document introding minimal "PIDE";
wenzelm
parents:
51533
diff
changeset
|
143 |
} |
517f232e867d
clarified module dependencies: avoid Properties and Document introding minimal "PIDE";
wenzelm
parents:
51533
diff
changeset
|
144 |
|
517f232e867d
clarified module dependencies: avoid Properties and Document introding minimal "PIDE";
wenzelm
parents:
51533
diff
changeset
|
145 |
|
66873
9953ae603a23
provide theory timing information, similar to command timing but always considered relevant;
wenzelm
parents:
66717
diff
changeset
|
146 |
/* theory timing */ |
9953ae603a23
provide theory timing information, similar to command timing but always considered relevant;
wenzelm
parents:
66717
diff
changeset
|
147 |
|
9953ae603a23
provide theory timing information, similar to command timing but always considered relevant;
wenzelm
parents:
66717
diff
changeset
|
148 |
object Theory_Timing |
9953ae603a23
provide theory timing information, similar to command timing but always considered relevant;
wenzelm
parents:
66717
diff
changeset
|
149 |
{ |
9953ae603a23
provide theory timing information, similar to command timing but always considered relevant;
wenzelm
parents:
66717
diff
changeset
|
150 |
def unapply(props: Properties.T): Option[(String, isabelle.Timing)] = |
9953ae603a23
provide theory timing information, similar to command timing but always considered relevant;
wenzelm
parents:
66717
diff
changeset
|
151 |
props match { |
9953ae603a23
provide theory timing information, similar to command timing but always considered relevant;
wenzelm
parents:
66717
diff
changeset
|
152 |
case Markup.THEORY_TIMING :: args => |
9953ae603a23
provide theory timing information, similar to command timing but always considered relevant;
wenzelm
parents:
66717
diff
changeset
|
153 |
(args, args) match { |
9953ae603a23
provide theory timing information, similar to command timing but always considered relevant;
wenzelm
parents:
66717
diff
changeset
|
154 |
case (Markup.Name(name), Markup.Timing_Properties(timing)) => Some((name, timing)) |
9953ae603a23
provide theory timing information, similar to command timing but always considered relevant;
wenzelm
parents:
66717
diff
changeset
|
155 |
case _ => None |
9953ae603a23
provide theory timing information, similar to command timing but always considered relevant;
wenzelm
parents:
66717
diff
changeset
|
156 |
} |
9953ae603a23
provide theory timing information, similar to command timing but always considered relevant;
wenzelm
parents:
66717
diff
changeset
|
157 |
case _ => None |
9953ae603a23
provide theory timing information, similar to command timing but always considered relevant;
wenzelm
parents:
66717
diff
changeset
|
158 |
} |
9953ae603a23
provide theory timing information, similar to command timing but always considered relevant;
wenzelm
parents:
66717
diff
changeset
|
159 |
} |
9953ae603a23
provide theory timing information, similar to command timing but always considered relevant;
wenzelm
parents:
66717
diff
changeset
|
160 |
|
9953ae603a23
provide theory timing information, similar to command timing but always considered relevant;
wenzelm
parents:
66717
diff
changeset
|
161 |
|
46209 | 162 |
/* node status */ |
163 |
||
46688 | 164 |
sealed case class Node_Status( |
68323 | 165 |
unprocessed: Int, running: Int, warned: Int, failed: Int, finished: Int, |
166 |
initialized: Boolean, consolidated: Boolean) |
|
44866 | 167 |
{ |
67915 | 168 |
def ok: Boolean = failed == 0 |
56474
4df2727a0b5f
more direct interpretation of "warned" status, like "failed" and independently of "finished", e.g. relevant for Rendering.overview_color of aux. files where main command status is unavailable (amending 0546e036d1c0);
wenzelm
parents:
56470
diff
changeset
|
169 |
def total: Int = unprocessed + running + warned + failed + finished |
67883 | 170 |
|
171 |
def json: JSON.Object.T = |
|
67915 | 172 |
JSON.Object("ok" -> ok, "total" -> total, "unprocessed" -> unprocessed, |
173 |
"running" -> running, "warned" -> warned, "failed" -> failed, "finished" -> finished, |
|
68323 | 174 |
"initialized" -> initialized, "consolidated" -> consolidated) |
44866 | 175 |
} |
44613 | 176 |
|
177 |
def node_status( |
|
66410 | 178 |
state: Document.State, |
179 |
version: Document.Version, |
|
68321 | 180 |
name: Document.Node.Name): Node_Status = |
44613 | 181 |
{ |
68321 | 182 |
val node = version.nodes(name) |
183 |
||
44613 | 184 |
var unprocessed = 0 |
185 |
var running = 0 |
|
46688 | 186 |
var warned = 0 |
44613 | 187 |
var failed = 0 |
56474
4df2727a0b5f
more direct interpretation of "warned" status, like "failed" and independently of "finished", e.g. relevant for Rendering.overview_color of aux. files where main command status is unavailable (amending 0546e036d1c0);
wenzelm
parents:
56470
diff
changeset
|
188 |
var finished = 0 |
56356
c3dbaa155ece
tuned for-comprehensions -- less structure mapping;
wenzelm
parents:
56355
diff
changeset
|
189 |
for (command <- node.commands.iterator) { |
56355
1a9f569b5b7e
some rephrasing to ensure that this becomes cheap "foreach" and not expensive "map" (cf. 0fc032898b05);
wenzelm
parents:
56353
diff
changeset
|
190 |
val states = state.command_states(version, command) |
56359
bca016a9a18d
persistent protocol_status, to improve performance of node_status a little;
wenzelm
parents:
56356
diff
changeset
|
191 |
val status = Status.merge(states.iterator.map(_.protocol_status)) |
56355
1a9f569b5b7e
some rephrasing to ensure that this becomes cheap "foreach" and not expensive "map" (cf. 0fc032898b05);
wenzelm
parents:
56353
diff
changeset
|
192 |
|
56299
8201790fdeb9
more careful treatment of multiple command states (eval + prints): merge content that is actually required;
wenzelm
parents:
56295
diff
changeset
|
193 |
if (status.is_running) running += 1 |
57843
d8966c09025c
proper priority for error over warning also for node_status (see 9c5220e05e04);
wenzelm
parents:
56801
diff
changeset
|
194 |
else if (status.is_failed) failed += 1 |
56395
0546e036d1c0
more direct warning within persistent Protocol.Status;
wenzelm
parents:
56387
diff
changeset
|
195 |
else if (status.is_warned) warned += 1 |
0546e036d1c0
more direct warning within persistent Protocol.Status;
wenzelm
parents:
56387
diff
changeset
|
196 |
else if (status.is_finished) finished += 1 |
56299
8201790fdeb9
more careful treatment of multiple command states (eval + prints): merge content that is actually required;
wenzelm
parents:
56295
diff
changeset
|
197 |
else unprocessed += 1 |
8201790fdeb9
more careful treatment of multiple command states (eval + prints): merge content that is actually required;
wenzelm
parents:
56295
diff
changeset
|
198 |
} |
68323 | 199 |
val initialized = state.node_initialized(version, name) |
66410 | 200 |
val consolidated = state.node_consolidated(version, name) |
201 |
||
68323 | 202 |
Node_Status(unprocessed, running, warned, failed, finished, initialized, consolidated) |
44613 | 203 |
} |
204 |
||
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
|
205 |
|
51533 | 206 |
/* node timing */ |
207 |
||
208 |
sealed case class Node_Timing(total: Double, commands: Map[Command, Double]) |
|
209 |
||
210 |
val empty_node_timing = Node_Timing(0.0, Map.empty) |
|
211 |
||
212 |
def node_timing( |
|
213 |
state: Document.State, |
|
214 |
version: Document.Version, |
|
215 |
node: Document.Node, |
|
216 |
threshold: Double): Node_Timing = |
|
217 |
{ |
|
218 |
var total = 0.0 |
|
219 |
var commands = Map.empty[Command, Double] |
|
220 |
for { |
|
221 |
command <- node.commands.iterator |
|
56299
8201790fdeb9
more careful treatment of multiple command states (eval + prints): merge content that is actually required;
wenzelm
parents:
56295
diff
changeset
|
222 |
st <- state.command_states(version, command) |
56356
c3dbaa155ece
tuned for-comprehensions -- less structure mapping;
wenzelm
parents:
56355
diff
changeset
|
223 |
} { |
c3dbaa155ece
tuned for-comprehensions -- less structure mapping;
wenzelm
parents:
56355
diff
changeset
|
224 |
val command_timing = |
51533 | 225 |
(0.0 /: st.status)({ |
226 |
case (timing, Markup.Timing(t)) => timing + t.elapsed.seconds |
|
227 |
case (timing, _) => timing |
|
228 |
}) |
|
229 |
total += command_timing |
|
230 |
if (command_timing >= threshold) commands += (command -> command_timing) |
|
231 |
} |
|
232 |
Node_Timing(total, commands) |
|
233 |
} |
|
234 |
||
235 |
||
39441
4110cc1b8f9f
allow embedded reports in regular prover messages, to avoid side-effects for errors for example;
wenzelm
parents:
39439
diff
changeset
|
236 |
/* 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
|
237 |
|
50500
c94bba7906d2
identify dialogs via official serial and maintain as result message;
wenzelm
parents:
50498
diff
changeset
|
238 |
def is_result(msg: XML.Tree): Boolean = |
c94bba7906d2
identify dialogs via official serial and maintain as result message;
wenzelm
parents:
50498
diff
changeset
|
239 |
msg match { |
c94bba7906d2
identify dialogs via official serial and maintain as result message;
wenzelm
parents:
50498
diff
changeset
|
240 |
case XML.Elem(Markup(Markup.RESULT, _), _) => true |
c94bba7906d2
identify dialogs via official serial and maintain as result message;
wenzelm
parents:
50498
diff
changeset
|
241 |
case _ => false |
c94bba7906d2
identify dialogs via official serial and maintain as result message;
wenzelm
parents:
50498
diff
changeset
|
242 |
} |
c94bba7906d2
identify dialogs via official serial and maintain as result message;
wenzelm
parents:
50498
diff
changeset
|
243 |
|
50157 | 244 |
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
|
245 |
msg match { |
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
50157
diff
changeset
|
246 |
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
|
247 |
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
|
248 |
case _ => false |
53365ba766ac
Command.accumulate: refrain from adding tracing messages to markup tree -- potential scalability problem;
wenzelm
parents:
39511
diff
changeset
|
249 |
} |
53365ba766ac
Command.accumulate: refrain from adding tracing messages to markup tree -- potential scalability problem;
wenzelm
parents:
39511
diff
changeset
|
250 |
|
59184
830bb7ddb3ab
explicit message channels for "state", "information";
wenzelm
parents:
59085
diff
changeset
|
251 |
def is_state(msg: XML.Tree): Boolean = |
50500
c94bba7906d2
identify dialogs via official serial and maintain as result message;
wenzelm
parents:
50498
diff
changeset
|
252 |
msg match { |
59184
830bb7ddb3ab
explicit message channels for "state", "information";
wenzelm
parents:
59085
diff
changeset
|
253 |
case XML.Elem(Markup(Markup.STATE, _), _) => true |
830bb7ddb3ab
explicit message channels for "state", "information";
wenzelm
parents:
59085
diff
changeset
|
254 |
case XML.Elem(Markup(Markup.STATE_MESSAGE, _), _) => true |
830bb7ddb3ab
explicit message channels for "state", "information";
wenzelm
parents:
59085
diff
changeset
|
255 |
case _ => false |
830bb7ddb3ab
explicit message channels for "state", "information";
wenzelm
parents:
59085
diff
changeset
|
256 |
} |
830bb7ddb3ab
explicit message channels for "state", "information";
wenzelm
parents:
59085
diff
changeset
|
257 |
|
830bb7ddb3ab
explicit message channels for "state", "information";
wenzelm
parents:
59085
diff
changeset
|
258 |
def is_information(msg: XML.Tree): Boolean = |
830bb7ddb3ab
explicit message channels for "state", "information";
wenzelm
parents:
59085
diff
changeset
|
259 |
msg match { |
830bb7ddb3ab
explicit message channels for "state", "information";
wenzelm
parents:
59085
diff
changeset
|
260 |
case XML.Elem(Markup(Markup.INFORMATION, _), _) => true |
830bb7ddb3ab
explicit message channels for "state", "information";
wenzelm
parents:
59085
diff
changeset
|
261 |
case XML.Elem(Markup(Markup.INFORMATION_MESSAGE, _), _) => true |
50500
c94bba7906d2
identify dialogs via official serial and maintain as result message;
wenzelm
parents:
50498
diff
changeset
|
262 |
case _ => false |
c94bba7906d2
identify dialogs via official serial and maintain as result message;
wenzelm
parents:
50498
diff
changeset
|
263 |
} |
c94bba7906d2
identify dialogs via official serial and maintain as result message;
wenzelm
parents:
50498
diff
changeset
|
264 |
|
67923
3e072441c96a
clarified exported messages, e.g. suppress "information", "tracing";
wenzelm
parents:
67915
diff
changeset
|
265 |
def is_writeln(msg: XML.Tree): Boolean = |
3e072441c96a
clarified exported messages, e.g. suppress "information", "tracing";
wenzelm
parents:
67915
diff
changeset
|
266 |
msg match { |
3e072441c96a
clarified exported messages, e.g. suppress "information", "tracing";
wenzelm
parents:
67915
diff
changeset
|
267 |
case XML.Elem(Markup(Markup.WRITELN, _), _) => true |
3e072441c96a
clarified exported messages, e.g. suppress "information", "tracing";
wenzelm
parents:
67915
diff
changeset
|
268 |
case XML.Elem(Markup(Markup.WRITELN_MESSAGE, _), _) => true |
3e072441c96a
clarified exported messages, e.g. suppress "information", "tracing";
wenzelm
parents:
67915
diff
changeset
|
269 |
case _ => false |
3e072441c96a
clarified exported messages, e.g. suppress "information", "tracing";
wenzelm
parents:
67915
diff
changeset
|
270 |
} |
3e072441c96a
clarified exported messages, e.g. suppress "information", "tracing";
wenzelm
parents:
67915
diff
changeset
|
271 |
|
39511 | 272 |
def is_warning(msg: XML.Tree): Boolean = |
273 |
msg match { |
|
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
50157
diff
changeset
|
274 |
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
|
275 |
case XML.Elem(Markup(Markup.WARNING_MESSAGE, _), _) => true |
39511 | 276 |
case _ => false |
277 |
} |
|
278 |
||
59203
5f0bd5afc16d
explicit message channel for "legacy", which is nonetheless a variant of "warning";
wenzelm
parents:
59184
diff
changeset
|
279 |
def is_legacy(msg: XML.Tree): Boolean = |
5f0bd5afc16d
explicit message channel for "legacy", which is nonetheless a variant of "warning";
wenzelm
parents:
59184
diff
changeset
|
280 |
msg match { |
5f0bd5afc16d
explicit message channel for "legacy", which is nonetheless a variant of "warning";
wenzelm
parents:
59184
diff
changeset
|
281 |
case XML.Elem(Markup(Markup.LEGACY, _), _) => true |
5f0bd5afc16d
explicit message channel for "legacy", which is nonetheless a variant of "warning";
wenzelm
parents:
59184
diff
changeset
|
282 |
case XML.Elem(Markup(Markup.LEGACY_MESSAGE, _), _) => true |
5f0bd5afc16d
explicit message channel for "legacy", which is nonetheless a variant of "warning";
wenzelm
parents:
59184
diff
changeset
|
283 |
case _ => false |
5f0bd5afc16d
explicit message channel for "legacy", which is nonetheless a variant of "warning";
wenzelm
parents:
59184
diff
changeset
|
284 |
} |
5f0bd5afc16d
explicit message channel for "legacy", which is nonetheless a variant of "warning";
wenzelm
parents:
59184
diff
changeset
|
285 |
|
39511 | 286 |
def is_error(msg: XML.Tree): Boolean = |
287 |
msg match { |
|
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
50157
diff
changeset
|
288 |
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
|
289 |
case XML.Elem(Markup(Markup.ERROR_MESSAGE, _), _) => true |
39511 | 290 |
case _ => false |
291 |
} |
|
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
|
292 |
|
56495 | 293 |
def is_inlined(msg: XML.Tree): Boolean = |
294 |
!(is_result(msg) || is_tracing(msg) || is_state(msg)) |
|
295 |
||
67923
3e072441c96a
clarified exported messages, e.g. suppress "information", "tracing";
wenzelm
parents:
67915
diff
changeset
|
296 |
def is_exported(msg: XML.Tree): Boolean = |
3e072441c96a
clarified exported messages, e.g. suppress "information", "tracing";
wenzelm
parents:
67915
diff
changeset
|
297 |
is_writeln(msg) || is_warning(msg) || is_legacy(msg) || is_error(msg) |
3e072441c96a
clarified exported messages, e.g. suppress "information", "tracing";
wenzelm
parents:
67915
diff
changeset
|
298 |
|
50500
c94bba7906d2
identify dialogs via official serial and maintain as result message;
wenzelm
parents:
50498
diff
changeset
|
299 |
|
60882 | 300 |
/* breakpoints */ |
301 |
||
302 |
object ML_Breakpoint |
|
303 |
{ |
|
304 |
def unapply(tree: XML.Tree): Option[Long] = |
|
305 |
tree match { |
|
306 |
case XML.Elem(Markup(Markup.ML_BREAKPOINT, Markup.Serial(breakpoint)), _) => Some(breakpoint) |
|
307 |
case _ => None |
|
308 |
} |
|
309 |
} |
|
310 |
||
311 |
||
50500
c94bba7906d2
identify dialogs via official serial and maintain as result message;
wenzelm
parents:
50498
diff
changeset
|
312 |
/* dialogs */ |
c94bba7906d2
identify dialogs via official serial and maintain as result message;
wenzelm
parents:
50498
diff
changeset
|
313 |
|
c94bba7906d2
identify dialogs via official serial and maintain as result message;
wenzelm
parents:
50498
diff
changeset
|
314 |
object Dialog_Args |
c94bba7906d2
identify dialogs via official serial and maintain as result message;
wenzelm
parents:
50498
diff
changeset
|
315 |
{ |
52531 | 316 |
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
|
317 |
(props, props, props) match { |
c94bba7906d2
identify dialogs via official serial and maintain as result message;
wenzelm
parents:
50498
diff
changeset
|
318 |
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
|
319 |
Some((id, serial, result)) |
c94bba7906d2
identify dialogs via official serial and maintain as result message;
wenzelm
parents:
50498
diff
changeset
|
320 |
case _ => None |
c94bba7906d2
identify dialogs via official serial and maintain as result message;
wenzelm
parents:
50498
diff
changeset
|
321 |
} |
c94bba7906d2
identify dialogs via official serial and maintain as result message;
wenzelm
parents:
50498
diff
changeset
|
322 |
} |
c94bba7906d2
identify dialogs via official serial and maintain as result message;
wenzelm
parents:
50498
diff
changeset
|
323 |
|
c94bba7906d2
identify dialogs via official serial and maintain as result message;
wenzelm
parents:
50498
diff
changeset
|
324 |
object Dialog |
c94bba7906d2
identify dialogs via official serial and maintain as result message;
wenzelm
parents:
50498
diff
changeset
|
325 |
{ |
52531 | 326 |
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
|
327 |
tree match { |
c94bba7906d2
identify dialogs via official serial and maintain as result message;
wenzelm
parents:
50498
diff
changeset
|
328 |
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
|
329 |
Some((id, serial, result)) |
c94bba7906d2
identify dialogs via official serial and maintain as result message;
wenzelm
parents:
50498
diff
changeset
|
330 |
case _ => None |
c94bba7906d2
identify dialogs via official serial and maintain as result message;
wenzelm
parents:
50498
diff
changeset
|
331 |
} |
c94bba7906d2
identify dialogs via official serial and maintain as result message;
wenzelm
parents:
50498
diff
changeset
|
332 |
} |
c94bba7906d2
identify dialogs via official serial and maintain as result message;
wenzelm
parents:
50498
diff
changeset
|
333 |
|
c94bba7906d2
identify dialogs via official serial and maintain as result message;
wenzelm
parents:
50498
diff
changeset
|
334 |
object Dialog_Result |
c94bba7906d2
identify dialogs via official serial and maintain as result message;
wenzelm
parents:
50498
diff
changeset
|
335 |
{ |
52531 | 336 |
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
|
337 |
{ |
6f41f1646617
more careful handling of Dialog_Result, with active area and color feedback;
wenzelm
parents:
50500
diff
changeset
|
338 |
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
|
339 |
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
|
340 |
} |
50500
c94bba7906d2
identify dialogs via official serial and maintain as result message;
wenzelm
parents:
50498
diff
changeset
|
341 |
|
50501
6f41f1646617
more careful handling of Dialog_Result, with active area and color feedback;
wenzelm
parents:
50500
diff
changeset
|
342 |
def unapply(tree: XML.Tree): Option[String] = |
50500
c94bba7906d2
identify dialogs via official serial and maintain as result message;
wenzelm
parents:
50498
diff
changeset
|
343 |
tree match { |
50501
6f41f1646617
more careful handling of Dialog_Result, with active area and color feedback;
wenzelm
parents:
50500
diff
changeset
|
344 |
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
|
345 |
case _ => None |
c94bba7906d2
identify dialogs via official serial and maintain as result message;
wenzelm
parents:
50498
diff
changeset
|
346 |
} |
c94bba7906d2
identify dialogs via official serial and maintain as result message;
wenzelm
parents:
50498
diff
changeset
|
347 |
} |
38412
c23f3abbf42d
moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff
changeset
|
348 |
} |
c23f3abbf42d
moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff
changeset
|
349 |
|
c23f3abbf42d
moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff
changeset
|
350 |
|
57916 | 351 |
trait Protocol |
38412
c23f3abbf42d
moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff
changeset
|
352 |
{ |
57916 | 353 |
/* protocol commands */ |
354 |
||
355 |
def protocol_command_bytes(name: String, args: Bytes*): Unit |
|
356 |
def protocol_command(name: String, args: String*): Unit |
|
357 |
||
358 |
||
56387 | 359 |
/* options */ |
360 |
||
361 |
def options(opts: Options): Unit = |
|
65345
2fdd4431b30e
clarified YXML vs. symbol encoding: operate on whole message;
wenzelm
parents:
65313
diff
changeset
|
362 |
protocol_command("Prover.options", Symbol.encode_yxml(opts.encode)) |
56387 | 363 |
|
364 |
||
65470 | 365 |
/* session base */ |
366 |
||
367 |
private def encode_table(table: List[(String, String)]): String = |
|
368 |
{ |
|
369 |
import XML.Encode._ |
|
370 |
Symbol.encode_yxml(list(pair(string, string))(table)) |
|
371 |
} |
|
372 |
||
66712 | 373 |
private def encode_list(lst: List[String]): String = |
374 |
{ |
|
375 |
import XML.Encode._ |
|
376 |
Symbol.encode_yxml(list(string)(lst)) |
|
377 |
} |
|
378 |
||
67493
c4e9e0c50487
treat sessions as entities with defining position;
wenzelm
parents:
67471
diff
changeset
|
379 |
private def encode_sessions(lst: List[(String, Position.T)]): String = |
c4e9e0c50487
treat sessions as entities with defining position;
wenzelm
parents:
67471
diff
changeset
|
380 |
{ |
c4e9e0c50487
treat sessions as entities with defining position;
wenzelm
parents:
67471
diff
changeset
|
381 |
import XML.Encode._ |
c4e9e0c50487
treat sessions as entities with defining position;
wenzelm
parents:
67471
diff
changeset
|
382 |
Symbol.encode_yxml(list(pair(string, properties))(lst)) |
c4e9e0c50487
treat sessions as entities with defining position;
wenzelm
parents:
67471
diff
changeset
|
383 |
} |
c4e9e0c50487
treat sessions as entities with defining position;
wenzelm
parents:
67471
diff
changeset
|
384 |
|
66668
6019cfb8256c
proper standard_path to revert platform_path in JEdit_Sessions.session_base;
wenzelm
parents:
66411
diff
changeset
|
385 |
def session_base(resources: Resources) |
6019cfb8256c
proper standard_path to revert platform_path in JEdit_Sessions.session_base;
wenzelm
parents:
66411
diff
changeset
|
386 |
{ |
6019cfb8256c
proper standard_path to revert platform_path in JEdit_Sessions.session_base;
wenzelm
parents:
66411
diff
changeset
|
387 |
val base = resources.session_base.standard_path |
67219 | 388 |
protocol_command("Prover.init_session_base", |
67493
c4e9e0c50487
treat sessions as entities with defining position;
wenzelm
parents:
67471
diff
changeset
|
389 |
encode_sessions(base.known.sessions.toList), |
67471 | 390 |
encode_list(base.doc_names), |
66668
6019cfb8256c
proper standard_path to revert platform_path in JEdit_Sessions.session_base;
wenzelm
parents:
66411
diff
changeset
|
391 |
encode_table(base.global_theories.toList), |
66717
67dbf5cdc056
more informative loaded_theories: dependencies and syntax;
wenzelm
parents:
66712
diff
changeset
|
392 |
encode_list(base.loaded_theories.keys), |
66668
6019cfb8256c
proper standard_path to revert platform_path in JEdit_Sessions.session_base;
wenzelm
parents:
66411
diff
changeset
|
393 |
encode_table(base.dest_known_theories)) |
6019cfb8256c
proper standard_path to revert platform_path in JEdit_Sessions.session_base;
wenzelm
parents:
66411
diff
changeset
|
394 |
} |
65470 | 395 |
|
396 |
||
56387 | 397 |
/* interned items */ |
54519
5fed81762406
maintain blobs within document state: digest + text in ML, digest-only in Scala;
wenzelm
parents:
54515
diff
changeset
|
398 |
|
56335
8953d4cc060a
store blob content within document node: aux. files that were once open are made persistent;
wenzelm
parents:
56306
diff
changeset
|
399 |
def define_blob(digest: SHA1.Digest, bytes: Bytes): Unit = |
56387 | 400 |
protocol_command_bytes("Document.define_blob", Bytes(digest.toString), bytes) |
38412
c23f3abbf42d
moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff
changeset
|
401 |
|
59671
9715eb8e9408
more precise position information in Isabelle/Scala, with YXML markup as in Isabelle/ML;
wenzelm
parents:
59364
diff
changeset
|
402 |
def define_command(command: Command) |
54519
5fed81762406
maintain blobs within document state: digest + text in ML, digest-only in Scala;
wenzelm
parents:
54515
diff
changeset
|
403 |
{ |
5fed81762406
maintain blobs within document state: digest + text in ML, digest-only in Scala;
wenzelm
parents:
54515
diff
changeset
|
404 |
val blobs_yxml = |
61376
93224745477f
output HTML text according to Isabelle/Scala Symbol.Interpretation;
wenzelm
parents:
60992
diff
changeset
|
405 |
{ |
93224745477f
output HTML text according to Isabelle/Scala Symbol.Interpretation;
wenzelm
parents:
60992
diff
changeset
|
406 |
import XML.Encode._ |
54519
5fed81762406
maintain blobs within document state: digest + text in ML, digest-only in Scala;
wenzelm
parents:
54515
diff
changeset
|
407 |
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
|
408 |
variant(List( |
54526 | 409 |
{ case Exn.Res((a, b)) => |
65345
2fdd4431b30e
clarified YXML vs. symbol encoding: operate on whole message;
wenzelm
parents:
65313
diff
changeset
|
410 |
(Nil, pair(string, option(string))((a.node, b.map(p => p._1.toString)))) }, |
2fdd4431b30e
clarified YXML vs. symbol encoding: operate on whole message;
wenzelm
parents:
65313
diff
changeset
|
411 |
{ case Exn.Exn(e) => (Nil, string(Exn.message(e))) })) |
59085
08a6901eb035
clarified define_command: send tokens more directly, without requiring keywords in ML;
wenzelm
parents:
58015
diff
changeset
|
412 |
|
65345
2fdd4431b30e
clarified YXML vs. symbol encoding: operate on whole message;
wenzelm
parents:
65313
diff
changeset
|
413 |
Symbol.encode_yxml(pair(list(encode_blob), int)(command.blobs, command.blobs_index)) |
54519
5fed81762406
maintain blobs within document state: digest + text in ML, digest-only in Scala;
wenzelm
parents:
54515
diff
changeset
|
414 |
} |
59085
08a6901eb035
clarified define_command: send tokens more directly, without requiring keywords in ML;
wenzelm
parents:
58015
diff
changeset
|
415 |
|
08a6901eb035
clarified define_command: send tokens more directly, without requiring keywords in ML;
wenzelm
parents:
58015
diff
changeset
|
416 |
val toks = command.span.content |
08a6901eb035
clarified define_command: send tokens more directly, without requiring keywords in ML;
wenzelm
parents:
58015
diff
changeset
|
417 |
val toks_yxml = |
61376
93224745477f
output HTML text according to Isabelle/Scala Symbol.Interpretation;
wenzelm
parents:
60992
diff
changeset
|
418 |
{ |
93224745477f
output HTML text according to Isabelle/Scala Symbol.Interpretation;
wenzelm
parents:
60992
diff
changeset
|
419 |
import XML.Encode._ |
64616 | 420 |
val encode_tok: T[Token] = (tok => pair(int, int)((tok.kind.id, Symbol.length(tok.source)))) |
65345
2fdd4431b30e
clarified YXML vs. symbol encoding: operate on whole message;
wenzelm
parents:
65313
diff
changeset
|
421 |
Symbol.encode_yxml(list(encode_tok)(toks)) |
59085
08a6901eb035
clarified define_command: send tokens more directly, without requiring keywords in ML;
wenzelm
parents:
58015
diff
changeset
|
422 |
} |
08a6901eb035
clarified define_command: send tokens more directly, without requiring keywords in ML;
wenzelm
parents:
58015
diff
changeset
|
423 |
|
52582 | 424 |
protocol_command("Document.define_command", |
65345
2fdd4431b30e
clarified YXML vs. symbol encoding: operate on whole message;
wenzelm
parents:
65313
diff
changeset
|
425 |
(Document_ID(command.id) :: Symbol.encode(command.span.name) :: blobs_yxml :: toks_yxml :: |
2fdd4431b30e
clarified YXML vs. symbol encoding: operate on whole message;
wenzelm
parents:
65313
diff
changeset
|
426 |
toks.map(tok => Symbol.encode(tok.source))): _*) |
54519
5fed81762406
maintain blobs within document state: digest + text in ML, digest-only in Scala;
wenzelm
parents:
54515
diff
changeset
|
427 |
} |
38412
c23f3abbf42d
moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff
changeset
|
428 |
|
c23f3abbf42d
moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff
changeset
|
429 |
|
52931
ac6648c0c0fb
cancel_query via direct access to the exec_id of the running query process;
wenzelm
parents:
52862
diff
changeset
|
430 |
/* execution */ |
ac6648c0c0fb
cancel_query via direct access to the exec_id of the running query process;
wenzelm
parents:
52862
diff
changeset
|
431 |
|
ac6648c0c0fb
cancel_query via direct access to the exec_id of the running query process;
wenzelm
parents:
52862
diff
changeset
|
432 |
def discontinue_execution(): Unit = |
ac6648c0c0fb
cancel_query via direct access to the exec_id of the running query process;
wenzelm
parents:
52862
diff
changeset
|
433 |
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
|
434 |
|
52931
ac6648c0c0fb
cancel_query via direct access to the exec_id of the running query process;
wenzelm
parents:
52862
diff
changeset
|
435 |
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
|
436 |
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
|
437 |
|
ac6648c0c0fb
cancel_query via direct access to the exec_id of the running query process;
wenzelm
parents:
52862
diff
changeset
|
438 |
|
ac6648c0c0fb
cancel_query via direct access to the exec_id of the running query process;
wenzelm
parents:
52862
diff
changeset
|
439 |
/* 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
|
440 |
|
52530
99dd8b4ef3fe
explicit module Document_ID as source of globally unique identifiers across ML/Scala;
wenzelm
parents:
52527
diff
changeset
|
441 |
def update(old_id: Document_ID.Version, new_id: Document_ID.Version, |
68381
2fd3a6d6ba2e
less wasteful consolidation, based on PIDE front-end state and recent changes;
wenzelm
parents:
68336
diff
changeset
|
442 |
edits: List[Document.Edit_Command], consolidate: List[Document.Node.Name]) |
38412
c23f3abbf42d
moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff
changeset
|
443 |
{ |
44157
a21d3e1e64fd
uniform treatment of header edits as document edits;
wenzelm
parents:
44156
diff
changeset
|
444 |
val edits_yxml = |
61376
93224745477f
output HTML text according to Isabelle/Scala Symbol.Interpretation;
wenzelm
parents:
60992
diff
changeset
|
445 |
{ |
93224745477f
output HTML text according to Isabelle/Scala Symbol.Interpretation;
wenzelm
parents:
60992
diff
changeset
|
446 |
import XML.Encode._ |
44383 | 447 |
def id: T[Command] = (cmd => long(cmd.id)) |
46737 | 448 |
def encode_edit(name: Document.Node.Name) |
52849 | 449 |
: 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
|
450 |
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
|
451 |
{ 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
|
452 |
{ case Document.Node.Deps(header) => |
60992 | 453 |
val master_dir = File.standard_url(name.master_dir) |
59695 | 454 |
val imports = header.imports.map({ case (a, _) => a.node }) |
65384 | 455 |
val keywords = |
456 |
header.keywords.map({ case (a, Keyword.Spec(b, c, d)) => (a, ((b, c), d)) }) |
|
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
|
457 |
(Nil, |
65345
2fdd4431b30e
clarified YXML vs. symbol encoding: operate on whole message;
wenzelm
parents:
65313
diff
changeset
|
458 |
pair(string, pair(string, pair(list(string), pair(list(pair(string, |
2fdd4431b30e
clarified YXML vs. symbol encoding: operate on whole message;
wenzelm
parents:
65313
diff
changeset
|
459 |
pair(pair(string, list(string)), list(string)))), list(string)))))( |
65445
e9e7f5f5794c
more qualifier treatment, but in the end it is still ignored;
wenzelm
parents:
65439
diff
changeset
|
460 |
(master_dir, (name.theory, (imports, (keywords, header.errors)))))) }, |
52849 | 461 |
{ case Document.Node.Perspective(a, b, c) => |
462 |
(bool_atom(a) :: b.commands.map(cmd => long_atom(cmd.id)), |
|
65345
2fdd4431b30e
clarified YXML vs. symbol encoding: operate on whole message;
wenzelm
parents:
65313
diff
changeset
|
463 |
list(pair(id, pair(string, list(string))))(c.dest)) })) |
48705
dd32321d6eef
tuned signature -- slightly more abstract text representation of prover process;
wenzelm
parents:
47542
diff
changeset
|
464 |
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
|
465 |
{ |
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
|
466 |
val (name, edit) = node_edit |
65345
2fdd4431b30e
clarified YXML vs. symbol encoding: operate on whole message;
wenzelm
parents:
65313
diff
changeset
|
467 |
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
|
468 |
}) |
68381
2fd3a6d6ba2e
less wasteful consolidation, based on PIDE front-end state and recent changes;
wenzelm
parents:
68336
diff
changeset
|
469 |
Symbol.encode_yxml(encode_edits(edits)) |
2fd3a6d6ba2e
less wasteful consolidation, based on PIDE front-end state and recent changes;
wenzelm
parents:
68336
diff
changeset
|
470 |
} |
2fd3a6d6ba2e
less wasteful consolidation, based on PIDE front-end state and recent changes;
wenzelm
parents:
68336
diff
changeset
|
471 |
|
2fd3a6d6ba2e
less wasteful consolidation, based on PIDE front-end state and recent changes;
wenzelm
parents:
68336
diff
changeset
|
472 |
val consolidate_yxml = |
2fd3a6d6ba2e
less wasteful consolidation, based on PIDE front-end state and recent changes;
wenzelm
parents:
68336
diff
changeset
|
473 |
{ |
2fd3a6d6ba2e
less wasteful consolidation, based on PIDE front-end state and recent changes;
wenzelm
parents:
68336
diff
changeset
|
474 |
import XML.Encode._ |
2fd3a6d6ba2e
less wasteful consolidation, based on PIDE front-end state and recent changes;
wenzelm
parents:
68336
diff
changeset
|
475 |
Symbol.encode_yxml(list(string)(consolidate.map(_.node))) |
2fd3a6d6ba2e
less wasteful consolidation, based on PIDE front-end state and recent changes;
wenzelm
parents:
68336
diff
changeset
|
476 |
} |
2fd3a6d6ba2e
less wasteful consolidation, based on PIDE front-end state and recent changes;
wenzelm
parents:
68336
diff
changeset
|
477 |
|
68336
09ac56914b29
Document.update includes node consolidation / presentation as regular print operation: avoid user operations on protocol thread;
wenzelm
parents:
68323
diff
changeset
|
478 |
protocol_command( |
68381
2fd3a6d6ba2e
less wasteful consolidation, based on PIDE front-end state and recent changes;
wenzelm
parents:
68336
diff
changeset
|
479 |
"Document.update", Document_ID(old_id), Document_ID(new_id), edits_yxml, consolidate_yxml) |
38412
c23f3abbf42d
moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff
changeset
|
480 |
} |
43748 | 481 |
|
44673 | 482 |
def remove_versions(versions: List[Document.Version]) |
483 |
{ |
|
484 |
val versions_yxml = |
|
59364 | 485 |
{ import XML.Encode._ |
65345
2fdd4431b30e
clarified YXML vs. symbol encoding: operate on whole message;
wenzelm
parents:
65313
diff
changeset
|
486 |
Symbol.encode_yxml(list(long)(versions.map(_.id))) } |
52582 | 487 |
protocol_command("Document.remove_versions", versions_yxml) |
44673 | 488 |
} |
489 |
||
43748 | 490 |
|
50498 | 491 |
/* dialog via document content */ |
492 |
||
52931
ac6648c0c0fb
cancel_query via direct access to the exec_id of the running query process;
wenzelm
parents:
52862
diff
changeset
|
493 |
def dialog_result(serial: Long, result: String): Unit = |
63805 | 494 |
protocol_command("Document.dialog_result", Value.Long(serial), result) |
38412
c23f3abbf42d
moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff
changeset
|
495 |
} |