author | wenzelm |
Sat, 05 Dec 2020 12:43:21 +0100 | |
changeset 72817 | 1c378ab75d48 |
parent 72816 | ea4f86914cb2 |
child 72824 | eb526f6c92b7 |
permissions | -rw-r--r-- |
36676 | 1 |
/* Title: Pure/PIDE/command.scala |
2 |
Author: Fabian Immler, TU Munich |
|
3 |
Author: Makarius |
|
4 |
||
52536 | 5 |
Prover commands with accumulated results from execution. |
36676 | 6 |
*/ |
34407 | 7 |
|
34871
e596a0b71f3c
incorporate "proofdocument" part into main Isabelle/Pure.jar -- except for html_panel.scala, which depends on external library (Lobo/Cobra browser);
wenzelm
parents:
34865
diff
changeset
|
8 |
package isabelle |
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
9 |
|
34451 | 10 |
|
45644 | 11 |
import scala.collection.mutable |
38872 | 12 |
import scala.collection.immutable.SortedMap |
13 |
||
14 |
||
34637 | 15 |
object Command |
16 |
{ |
|
72814 | 17 |
/* blobs */ |
59702
58dfaa369c11
hybrid use of command blobs: inlined errors and auxiliary files;
wenzelm
parents:
59699
diff
changeset
|
18 |
|
72817
1c378ab75d48
clarified signature, notably access to blob files;
wenzelm
parents:
72816
diff
changeset
|
19 |
object Blob |
1c378ab75d48
clarified signature, notably access to blob files;
wenzelm
parents:
72816
diff
changeset
|
20 |
{ |
1c378ab75d48
clarified signature, notably access to blob files;
wenzelm
parents:
72816
diff
changeset
|
21 |
def read_file(name: Document.Node.Name, src_path: Path): Blob = |
1c378ab75d48
clarified signature, notably access to blob files;
wenzelm
parents:
72816
diff
changeset
|
22 |
{ |
1c378ab75d48
clarified signature, notably access to blob files;
wenzelm
parents:
72816
diff
changeset
|
23 |
val bytes = Bytes.read(name.path) |
1c378ab75d48
clarified signature, notably access to blob files;
wenzelm
parents:
72816
diff
changeset
|
24 |
val chunk = Symbol.Text_Chunk(bytes.text) |
1c378ab75d48
clarified signature, notably access to blob files;
wenzelm
parents:
72816
diff
changeset
|
25 |
Blob(name, src_path, Some((bytes.sha1_digest, chunk))) |
1c378ab75d48
clarified signature, notably access to blob files;
wenzelm
parents:
72816
diff
changeset
|
26 |
} |
1c378ab75d48
clarified signature, notably access to blob files;
wenzelm
parents:
72816
diff
changeset
|
27 |
} |
1c378ab75d48
clarified signature, notably access to blob files;
wenzelm
parents:
72816
diff
changeset
|
28 |
|
72745 | 29 |
sealed case class Blob( |
30 |
name: Document.Node.Name, |
|
72747
5f9d66155081
clarified theory keywords: loaded_files are determined statically in Scala, but ML needs to do it semantically;
wenzelm
parents:
72745
diff
changeset
|
31 |
src_path: Path, |
72745 | 32 |
content: Option[(SHA1.Digest, Symbol.Text_Chunk)]) |
72816
ea4f86914cb2
support for PIDE markup for auxiliary files ("blobs");
wenzelm
parents:
72814
diff
changeset
|
33 |
{ |
72817
1c378ab75d48
clarified signature, notably access to blob files;
wenzelm
parents:
72816
diff
changeset
|
34 |
def read_file: String = File.read(name.path) |
1c378ab75d48
clarified signature, notably access to blob files;
wenzelm
parents:
72816
diff
changeset
|
35 |
|
72816
ea4f86914cb2
support for PIDE markup for auxiliary files ("blobs");
wenzelm
parents:
72814
diff
changeset
|
36 |
def chunk_file: Symbol.Text_Chunk.File = |
ea4f86914cb2
support for PIDE markup for auxiliary files ("blobs");
wenzelm
parents:
72814
diff
changeset
|
37 |
Symbol.Text_Chunk.File(name.node) |
ea4f86914cb2
support for PIDE markup for auxiliary files ("blobs");
wenzelm
parents:
72814
diff
changeset
|
38 |
} |
72745 | 39 |
|
72814 | 40 |
object Blobs_Info |
41 |
{ |
|
42 |
val none: Blobs_Info = Blobs_Info(Nil, -1) |
|
43 |
||
44 |
def errors(msgs: List[String]): Blobs_Info = |
|
45 |
Blobs_Info(msgs.map(msg => Exn.Exn[Blob](ERROR(msg))), -1) |
|
46 |
} |
|
47 |
||
48 |
sealed case class Blobs_Info(blobs: List[Exn.Result[Blob]], index: Int) |
|
49 |
||
52849 | 50 |
|
51 |
||
38361 | 52 |
/** accumulated results from prover **/ |
53 |
||
50507 | 54 |
/* results */ |
55 |
||
56 |
object Results |
|
57 |
{ |
|
51496
cb677987b7e3
retain original tooltip range, to avoid repeated window popup when the mouse is moved over the same content;
wenzelm
parents:
51494
diff
changeset
|
58 |
type Entry = (Long, XML.Tree) |
68101 | 59 |
val empty: Results = new Results(SortedMap.empty) |
59072 | 60 |
def make(args: TraversableOnce[Results.Entry]): Results = (empty /: args)(_ + _) |
61 |
def merge(args: TraversableOnce[Results]): Results = (empty /: args)(_ ++ _) |
|
50507 | 62 |
} |
63 |
||
51494 | 64 |
final class Results private(private val rep: SortedMap[Long, XML.Tree]) |
50507 | 65 |
{ |
64802 | 66 |
def is_empty: Boolean = rep.isEmpty |
50507 | 67 |
def defined(serial: Long): Boolean = rep.isDefinedAt(serial) |
68 |
def get(serial: Long): Option[XML.Tree] = rep.get(serial) |
|
56372
fadb0fef09d7
more explicit iterator terminology, in accordance to Scala 2.8 library;
wenzelm
parents:
56359
diff
changeset
|
69 |
def iterator: Iterator[Results.Entry] = rep.iterator |
50508
5b7150395568
tuned implementation according to Library.insert/merge in ML;
wenzelm
parents:
50507
diff
changeset
|
70 |
|
51496
cb677987b7e3
retain original tooltip range, to avoid repeated window popup when the mouse is moved over the same content;
wenzelm
parents:
51494
diff
changeset
|
71 |
def + (entry: Results.Entry): Results = |
50508
5b7150395568
tuned implementation according to Library.insert/merge in ML;
wenzelm
parents:
50507
diff
changeset
|
72 |
if (defined(entry._1)) this |
5b7150395568
tuned implementation according to Library.insert/merge in ML;
wenzelm
parents:
50507
diff
changeset
|
73 |
else new Results(rep + entry) |
5b7150395568
tuned implementation according to Library.insert/merge in ML;
wenzelm
parents:
50507
diff
changeset
|
74 |
|
5b7150395568
tuned implementation according to Library.insert/merge in ML;
wenzelm
parents:
50507
diff
changeset
|
75 |
def ++ (other: Results): Results = |
5b7150395568
tuned implementation according to Library.insert/merge in ML;
wenzelm
parents:
50507
diff
changeset
|
76 |
if (this eq other) this |
5b7150395568
tuned implementation according to Library.insert/merge in ML;
wenzelm
parents:
50507
diff
changeset
|
77 |
else if (rep.isEmpty) other |
56372
fadb0fef09d7
more explicit iterator terminology, in accordance to Scala 2.8 library;
wenzelm
parents:
56359
diff
changeset
|
78 |
else (this /: other.iterator)(_ + _) |
50540 | 79 |
|
51494 | 80 |
override def hashCode: Int = rep.hashCode |
81 |
override def equals(that: Any): Boolean = |
|
82 |
that match { |
|
83 |
case other: Results => rep == other.rep |
|
84 |
case _ => false |
|
85 |
} |
|
56372
fadb0fef09d7
more explicit iterator terminology, in accordance to Scala 2.8 library;
wenzelm
parents:
56359
diff
changeset
|
86 |
override def toString: String = iterator.mkString("Results(", ", ", ")") |
50507 | 87 |
} |
88 |
||
89 |
||
68101 | 90 |
/* exports */ |
91 |
||
92 |
object Exports |
|
93 |
{ |
|
94 |
type Entry = (Long, Export.Entry) |
|
95 |
val empty: Exports = new Exports(SortedMap.empty) |
|
96 |
def merge(args: TraversableOnce[Exports]): Exports = (empty /: args)(_ ++ _) |
|
97 |
} |
|
98 |
||
99 |
final class Exports private(private val rep: SortedMap[Long, Export.Entry]) |
|
100 |
{ |
|
69634 | 101 |
def is_empty: Boolean = rep.isEmpty |
68101 | 102 |
def iterator: Iterator[Exports.Entry] = rep.iterator |
103 |
||
104 |
def + (entry: Exports.Entry): Exports = |
|
105 |
if (rep.isDefinedAt(entry._1)) this |
|
106 |
else new Exports(rep + entry) |
|
107 |
||
108 |
def ++ (other: Exports): Exports = |
|
109 |
if (this eq other) this |
|
110 |
else if (rep.isEmpty) other |
|
111 |
else (this /: other.iterator)(_ + _) |
|
112 |
||
113 |
override def hashCode: Int = rep.hashCode |
|
114 |
override def equals(that: Any): Boolean = |
|
115 |
that match { |
|
116 |
case other: Exports => rep == other.rep |
|
117 |
case _ => false |
|
118 |
} |
|
119 |
override def toString: String = iterator.mkString("Exports(", ", ", ")") |
|
120 |
} |
|
121 |
||
122 |
||
123 |
/* markups */ |
|
55649
1532ab0dc67b
more general / abstract Command.Markups, with separate index for status elements;
wenzelm
parents:
55648
diff
changeset
|
124 |
|
1532ab0dc67b
more general / abstract Command.Markups, with separate index for status elements;
wenzelm
parents:
55648
diff
changeset
|
125 |
object Markup_Index |
1532ab0dc67b
more general / abstract Command.Markups, with separate index for status elements;
wenzelm
parents:
55648
diff
changeset
|
126 |
{ |
56746 | 127 |
val markup: Markup_Index = Markup_Index(false, Symbol.Text_Chunk.Default) |
72816
ea4f86914cb2
support for PIDE markup for auxiliary files ("blobs");
wenzelm
parents:
72814
diff
changeset
|
128 |
def blob(blob: Blob): Markup_Index = Markup_Index(false, blob.chunk_file) |
55649
1532ab0dc67b
more general / abstract Command.Markups, with separate index for status elements;
wenzelm
parents:
55648
diff
changeset
|
129 |
} |
1532ab0dc67b
more general / abstract Command.Markups, with separate index for status elements;
wenzelm
parents:
55648
diff
changeset
|
130 |
|
56746 | 131 |
sealed case class Markup_Index(status: Boolean, chunk_name: Symbol.Text_Chunk.Name) |
55649
1532ab0dc67b
more general / abstract Command.Markups, with separate index for status elements;
wenzelm
parents:
55648
diff
changeset
|
132 |
|
1532ab0dc67b
more general / abstract Command.Markups, with separate index for status elements;
wenzelm
parents:
55648
diff
changeset
|
133 |
object Markups |
1532ab0dc67b
more general / abstract Command.Markups, with separate index for status elements;
wenzelm
parents:
55648
diff
changeset
|
134 |
{ |
1532ab0dc67b
more general / abstract Command.Markups, with separate index for status elements;
wenzelm
parents:
55648
diff
changeset
|
135 |
val empty: Markups = new Markups(Map.empty) |
65335 | 136 |
def init(markup: Markup_Tree): Markups = new Markups(Map(Markup_Index.markup -> markup)) |
137 |
def merge(args: TraversableOnce[Markups]): Markups = (empty /: args)(_ ++ _) |
|
55649
1532ab0dc67b
more general / abstract Command.Markups, with separate index for status elements;
wenzelm
parents:
55648
diff
changeset
|
138 |
} |
1532ab0dc67b
more general / abstract Command.Markups, with separate index for status elements;
wenzelm
parents:
55648
diff
changeset
|
139 |
|
1532ab0dc67b
more general / abstract Command.Markups, with separate index for status elements;
wenzelm
parents:
55648
diff
changeset
|
140 |
final class Markups private(private val rep: Map[Markup_Index, Markup_Tree]) |
1532ab0dc67b
more general / abstract Command.Markups, with separate index for status elements;
wenzelm
parents:
55648
diff
changeset
|
141 |
{ |
56489 | 142 |
def is_empty: Boolean = rep.isEmpty |
143 |
||
55649
1532ab0dc67b
more general / abstract Command.Markups, with separate index for status elements;
wenzelm
parents:
55648
diff
changeset
|
144 |
def apply(index: Markup_Index): Markup_Tree = |
1532ab0dc67b
more general / abstract Command.Markups, with separate index for status elements;
wenzelm
parents:
55648
diff
changeset
|
145 |
rep.getOrElse(index, Markup_Tree.empty) |
1532ab0dc67b
more general / abstract Command.Markups, with separate index for status elements;
wenzelm
parents:
55648
diff
changeset
|
146 |
|
1532ab0dc67b
more general / abstract Command.Markups, with separate index for status elements;
wenzelm
parents:
55648
diff
changeset
|
147 |
def add(index: Markup_Index, markup: Text.Markup): Markups = |
1532ab0dc67b
more general / abstract Command.Markups, with separate index for status elements;
wenzelm
parents:
55648
diff
changeset
|
148 |
new Markups(rep + (index -> (this(index) + markup))) |
1532ab0dc67b
more general / abstract Command.Markups, with separate index for status elements;
wenzelm
parents:
55648
diff
changeset
|
149 |
|
65335 | 150 |
def + (entry: (Markup_Index, Markup_Tree)): Markups = |
151 |
{ |
|
152 |
val (index, tree) = entry |
|
153 |
new Markups(rep + (index -> (this(index).merge(tree, Text.Range.full, Markup.Elements.full)))) |
|
154 |
} |
|
155 |
||
156 |
def ++ (other: Markups): Markups = |
|
157 |
if (this eq other) this |
|
158 |
else if (rep.isEmpty) other |
|
159 |
else (this /: other.rep.iterator)(_ + _) |
|
160 |
||
56475 | 161 |
def redirection_iterator: Iterator[Document_ID.Generic] = |
56746 | 162 |
for (Markup_Index(_, Symbol.Text_Chunk.Id(id)) <- rep.keysIterator) |
56475 | 163 |
yield id |
56470
8eda56033203
accumulate markup reports for "other" command ids, which are later retargeted and merged for rendering (in erratic order);
wenzelm
parents:
56469
diff
changeset
|
164 |
|
56475 | 165 |
def redirect(other_id: Document_ID.Generic): Markups = |
56489 | 166 |
{ |
167 |
val rep1 = |
|
56470
8eda56033203
accumulate markup reports for "other" command ids, which are later retargeted and merged for rendering (in erratic order);
wenzelm
parents:
56469
diff
changeset
|
168 |
(for { |
56746 | 169 |
(Markup_Index(status, Symbol.Text_Chunk.Id(id)), markup) <- rep.iterator |
56470
8eda56033203
accumulate markup reports for "other" command ids, which are later retargeted and merged for rendering (in erratic order);
wenzelm
parents:
56469
diff
changeset
|
170 |
if other_id == id |
56746 | 171 |
} yield (Markup_Index(status, Symbol.Text_Chunk.Default), markup)).toMap |
56489 | 172 |
if (rep1.isEmpty) Markups.empty else new Markups(rep1) |
173 |
} |
|
56470
8eda56033203
accumulate markup reports for "other" command ids, which are later retargeted and merged for rendering (in erratic order);
wenzelm
parents:
56469
diff
changeset
|
174 |
|
55649
1532ab0dc67b
more general / abstract Command.Markups, with separate index for status elements;
wenzelm
parents:
55648
diff
changeset
|
175 |
override def hashCode: Int = rep.hashCode |
1532ab0dc67b
more general / abstract Command.Markups, with separate index for status elements;
wenzelm
parents:
55648
diff
changeset
|
176 |
override def equals(that: Any): Boolean = |
1532ab0dc67b
more general / abstract Command.Markups, with separate index for status elements;
wenzelm
parents:
55648
diff
changeset
|
177 |
that match { |
1532ab0dc67b
more general / abstract Command.Markups, with separate index for status elements;
wenzelm
parents:
55648
diff
changeset
|
178 |
case other: Markups => rep == other.rep |
1532ab0dc67b
more general / abstract Command.Markups, with separate index for status elements;
wenzelm
parents:
55648
diff
changeset
|
179 |
case _ => false |
1532ab0dc67b
more general / abstract Command.Markups, with separate index for status elements;
wenzelm
parents:
55648
diff
changeset
|
180 |
} |
1532ab0dc67b
more general / abstract Command.Markups, with separate index for status elements;
wenzelm
parents:
55648
diff
changeset
|
181 |
override def toString: String = rep.iterator.mkString("Markups(", ", ", ")") |
1532ab0dc67b
more general / abstract Command.Markups, with separate index for status elements;
wenzelm
parents:
55648
diff
changeset
|
182 |
} |
1532ab0dc67b
more general / abstract Command.Markups, with separate index for status elements;
wenzelm
parents:
55648
diff
changeset
|
183 |
|
1532ab0dc67b
more general / abstract Command.Markups, with separate index for status elements;
wenzelm
parents:
55648
diff
changeset
|
184 |
|
50507 | 185 |
/* state */ |
50501
6f41f1646617
more careful handling of Dialog_Result, with active area and color feedback;
wenzelm
parents:
50500
diff
changeset
|
186 |
|
56299
8201790fdeb9
more careful treatment of multiple command states (eval + prints): merge content that is actually required;
wenzelm
parents:
56295
diff
changeset
|
187 |
object State |
8201790fdeb9
more careful treatment of multiple command states (eval + prints): merge content that is actually required;
wenzelm
parents:
56295
diff
changeset
|
188 |
{ |
67824
661cd25304ae
more compact markup tree: output messages are already stored in command results (e.g. relevant for XML data representation);
wenzelm
parents:
67446
diff
changeset
|
189 |
def get_result(states: List[State], serial: Long): Option[XML.Tree] = |
661cd25304ae
more compact markup tree: output messages are already stored in command results (e.g. relevant for XML data representation);
wenzelm
parents:
67446
diff
changeset
|
190 |
states.find(st => st.results.defined(serial)).map(st => st.results.get(serial).get) |
661cd25304ae
more compact markup tree: output messages are already stored in command results (e.g. relevant for XML data representation);
wenzelm
parents:
67446
diff
changeset
|
191 |
|
661cd25304ae
more compact markup tree: output messages are already stored in command results (e.g. relevant for XML data representation);
wenzelm
parents:
67446
diff
changeset
|
192 |
def get_result_proper(states: List[State], props: Properties.T): Option[Results.Entry] = |
661cd25304ae
more compact markup tree: output messages are already stored in command results (e.g. relevant for XML data representation);
wenzelm
parents:
67446
diff
changeset
|
193 |
for { |
661cd25304ae
more compact markup tree: output messages are already stored in command results (e.g. relevant for XML data representation);
wenzelm
parents:
67446
diff
changeset
|
194 |
serial <- Markup.Serial.unapply(props) |
661cd25304ae
more compact markup tree: output messages are already stored in command results (e.g. relevant for XML data representation);
wenzelm
parents:
67446
diff
changeset
|
195 |
tree @ XML.Elem(_, body) <- get_result(states, serial) |
661cd25304ae
more compact markup tree: output messages are already stored in command results (e.g. relevant for XML data representation);
wenzelm
parents:
67446
diff
changeset
|
196 |
if body.nonEmpty |
661cd25304ae
more compact markup tree: output messages are already stored in command results (e.g. relevant for XML data representation);
wenzelm
parents:
67446
diff
changeset
|
197 |
} yield (serial -> tree) |
661cd25304ae
more compact markup tree: output messages are already stored in command results (e.g. relevant for XML data representation);
wenzelm
parents:
67446
diff
changeset
|
198 |
|
65335 | 199 |
def merge_results(states: List[State]): Results = |
56299
8201790fdeb9
more careful treatment of multiple command states (eval + prints): merge content that is actually required;
wenzelm
parents:
56295
diff
changeset
|
200 |
Results.merge(states.map(_.results)) |
8201790fdeb9
more careful treatment of multiple command states (eval + prints): merge content that is actually required;
wenzelm
parents:
56295
diff
changeset
|
201 |
|
68101 | 202 |
def merge_exports(states: List[State]): Exports = |
203 |
Exports.merge(states.map(_.exports)) |
|
204 |
||
65335 | 205 |
def merge_markups(states: List[State]): Markups = |
206 |
Markups.merge(states.map(_.markups)) |
|
207 |
||
56301
1da7b4c33db9
more frugal merge of markup trees: filter wrt. subsequent query;
wenzelm
parents:
56299
diff
changeset
|
208 |
def merge_markup(states: List[State], index: Markup_Index, |
56743 | 209 |
range: Text.Range, elements: Markup.Elements): Markup_Tree = |
56301
1da7b4c33db9
more frugal merge of markup trees: filter wrt. subsequent query;
wenzelm
parents:
56299
diff
changeset
|
210 |
Markup_Tree.merge(states.map(_.markup(index)), range, elements) |
65335 | 211 |
|
212 |
def merge(command: Command, states: List[State]): State = |
|
68101 | 213 |
State(command, states.flatMap(_.status), merge_results(states), |
214 |
merge_exports(states), merge_markups(states)) |
|
56299
8201790fdeb9
more careful treatment of multiple command states (eval + prints): merge content that is actually required;
wenzelm
parents:
56295
diff
changeset
|
215 |
} |
8201790fdeb9
more careful treatment of multiple command states (eval + prints): merge content that is actually required;
wenzelm
parents:
56295
diff
changeset
|
216 |
|
43714 | 217 |
sealed case class State( |
50501
6f41f1646617
more careful handling of Dialog_Result, with active area and color feedback;
wenzelm
parents:
50500
diff
changeset
|
218 |
command: Command, |
6f41f1646617
more careful handling of Dialog_Result, with active area and color feedback;
wenzelm
parents:
50500
diff
changeset
|
219 |
status: List[Markup] = Nil, |
50507 | 220 |
results: Results = Results.empty, |
68101 | 221 |
exports: Exports = Exports.empty, |
55649
1532ab0dc67b
more general / abstract Command.Markups, with separate index for status elements;
wenzelm
parents:
55648
diff
changeset
|
222 |
markups: Markups = Markups.empty) |
38361 | 223 |
{ |
68323 | 224 |
def initialized: Boolean = status.exists(markup => markup.name == Markup.INITIALIZED) |
70780
034742453594
more robust: avoid update/interrupt of long-running print_consolidation;
wenzelm
parents:
70713
diff
changeset
|
225 |
def consolidating: Boolean = status.exists(markup => markup.name == Markup.CONSOLIDATING) |
68335 | 226 |
def consolidated: Boolean = status.exists(markup => markup.name == Markup.CONSOLIDATED) |
66379
6392766f3c25
maintain "consolidated" status of theory nodes, which means all evals are finished (but not necessarily prints nor imports);
wenzelm
parents:
65522
diff
changeset
|
227 |
|
68758 | 228 |
lazy val maybe_consolidated: Boolean = |
229 |
{ |
|
230 |
var touched = false |
|
231 |
var forks = 0 |
|
232 |
var runs = 0 |
|
233 |
for (markup <- status) { |
|
234 |
markup.name match { |
|
235 |
case Markup.FORKED => touched = true; forks += 1 |
|
236 |
case Markup.JOINED => forks -= 1 |
|
237 |
case Markup.RUNNING => touched = true; runs += 1 |
|
238 |
case Markup.FINISHED => runs -= 1 |
|
239 |
case _ => |
|
240 |
} |
|
241 |
} |
|
242 |
touched && forks == 0 && runs == 0 |
|
243 |
} |
|
68381
2fd3a6d6ba2e
less wasteful consolidation, based on PIDE front-end state and recent changes;
wenzelm
parents:
68335
diff
changeset
|
244 |
|
68758 | 245 |
lazy val document_status: Document_Status.Command_Status = |
56395
0546e036d1c0
more direct warning within persistent Protocol.Status;
wenzelm
parents:
56372
diff
changeset
|
246 |
{ |
0546e036d1c0
more direct warning within persistent Protocol.Status;
wenzelm
parents:
56372
diff
changeset
|
247 |
val warnings = |
59203
5f0bd5afc16d
explicit message channel for "legacy", which is nonetheless a variant of "warning";
wenzelm
parents:
59072
diff
changeset
|
248 |
if (results.iterator.exists(p => Protocol.is_warning(p._2) || Protocol.is_legacy(p._2))) |
56395
0546e036d1c0
more direct warning within persistent Protocol.Status;
wenzelm
parents:
56372
diff
changeset
|
249 |
List(Markup(Markup.WARNING, Nil)) |
0546e036d1c0
more direct warning within persistent Protocol.Status;
wenzelm
parents:
56372
diff
changeset
|
250 |
else Nil |
0546e036d1c0
more direct warning within persistent Protocol.Status;
wenzelm
parents:
56372
diff
changeset
|
251 |
val errors = |
0546e036d1c0
more direct warning within persistent Protocol.Status;
wenzelm
parents:
56372
diff
changeset
|
252 |
if (results.iterator.exists(p => Protocol.is_error(p._2))) |
0546e036d1c0
more direct warning within persistent Protocol.Status;
wenzelm
parents:
56372
diff
changeset
|
253 |
List(Markup(Markup.ERROR, Nil)) |
0546e036d1c0
more direct warning within persistent Protocol.Status;
wenzelm
parents:
56372
diff
changeset
|
254 |
else Nil |
68758 | 255 |
Document_Status.Command_Status.make((warnings ::: errors ::: status).iterator) |
56395
0546e036d1c0
more direct warning within persistent Protocol.Status;
wenzelm
parents:
56372
diff
changeset
|
256 |
} |
55432
9c53198dbb1c
maintain multiple command chunks and markup trees: for main chunk and loaded files;
wenzelm
parents:
55431
diff
changeset
|
257 |
|
55650 | 258 |
def markup(index: Markup_Index): Markup_Tree = markups(index) |
55432
9c53198dbb1c
maintain multiple command chunks and markup trees: for main chunk and loaded files;
wenzelm
parents:
55431
diff
changeset
|
259 |
|
56489 | 260 |
def redirect(other_command: Command): Option[State] = |
261 |
{ |
|
262 |
val markups1 = markups.redirect(other_command.id) |
|
263 |
if (markups1.is_empty) None |
|
68101 | 264 |
else Some(new State(other_command, markups = markups1)) |
56489 | 265 |
} |
49614 | 266 |
|
55649
1532ab0dc67b
more general / abstract Command.Markups, with separate index for status elements;
wenzelm
parents:
55648
diff
changeset
|
267 |
private def add_status(st: Markup): State = |
1532ab0dc67b
more general / abstract Command.Markups, with separate index for status elements;
wenzelm
parents:
55648
diff
changeset
|
268 |
copy(status = st :: status) |
55432
9c53198dbb1c
maintain multiple command chunks and markup trees: for main chunk and loaded files;
wenzelm
parents:
55431
diff
changeset
|
269 |
|
67826 | 270 |
private def add_result(entry: Results.Entry): State = |
271 |
copy(results = results + entry) |
|
272 |
||
68114 | 273 |
def add_export(entry: Exports.Entry): Option[State] = |
274 |
if (command.node_name.theory == entry._2.theory_name) Some(copy(exports = exports + entry)) |
|
275 |
else None |
|
68101 | 276 |
|
56746 | 277 |
private def add_markup( |
278 |
status: Boolean, chunk_name: Symbol.Text_Chunk.Name, m: Text.Markup): State = |
|
55649
1532ab0dc67b
more general / abstract Command.Markups, with separate index for status elements;
wenzelm
parents:
55648
diff
changeset
|
279 |
{ |
1532ab0dc67b
more general / abstract Command.Markups, with separate index for status elements;
wenzelm
parents:
55648
diff
changeset
|
280 |
val markups1 = |
68758 | 281 |
if (status || Document_Status.Command_Status.liberal_elements(m.info.name)) |
56462
b64b0cb845fe
more explicit Command.Chunk types, less ooddities;
wenzelm
parents:
56395
diff
changeset
|
282 |
markups.add(Markup_Index(true, chunk_name), m) |
55649
1532ab0dc67b
more general / abstract Command.Markups, with separate index for status elements;
wenzelm
parents:
55648
diff
changeset
|
283 |
else markups |
56462
b64b0cb845fe
more explicit Command.Chunk types, less ooddities;
wenzelm
parents:
56395
diff
changeset
|
284 |
copy(markups = markups1.add(Markup_Index(false, chunk_name), m)) |
55649
1532ab0dc67b
more general / abstract Command.Markups, with separate index for status elements;
wenzelm
parents:
55648
diff
changeset
|
285 |
} |
38361 | 286 |
|
56470
8eda56033203
accumulate markup reports for "other" command ids, which are later retargeted and merged for rendering (in erratic order);
wenzelm
parents:
56469
diff
changeset
|
287 |
def accumulate( |
8eda56033203
accumulate markup reports for "other" command ids, which are later retargeted and merged for rendering (in erratic order);
wenzelm
parents:
56469
diff
changeset
|
288 |
self_id: Document_ID.Generic => Boolean, |
72780 | 289 |
other_id: (Document.Node.Name, Document_ID.Generic) => |
290 |
Option[(Symbol.Text_Chunk.Id, Symbol.Text_Chunk)], |
|
67825 | 291 |
message: XML.Elem, |
292 |
xml_cache: XML.Cache): State = |
|
38361 | 293 |
message match { |
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
50163
diff
changeset
|
294 |
case XML.Elem(Markup(Markup.STATUS, _), msgs) => |
72692
22aeec526ffd
support for PIDE markup in batch build (inactive due to pide_reports=false);
wenzelm
parents:
70780
diff
changeset
|
295 |
if (command.span.is_theory) this |
22aeec526ffd
support for PIDE markup in batch build (inactive due to pide_reports=false);
wenzelm
parents:
70780
diff
changeset
|
296 |
else { |
22aeec526ffd
support for PIDE markup in batch build (inactive due to pide_reports=false);
wenzelm
parents:
70780
diff
changeset
|
297 |
(this /: msgs)((state, msg) => |
22aeec526ffd
support for PIDE markup in batch build (inactive due to pide_reports=false);
wenzelm
parents:
70780
diff
changeset
|
298 |
msg match { |
22aeec526ffd
support for PIDE markup in batch build (inactive due to pide_reports=false);
wenzelm
parents:
70780
diff
changeset
|
299 |
case elem @ XML.Elem(markup, Nil) => |
22aeec526ffd
support for PIDE markup in batch build (inactive due to pide_reports=false);
wenzelm
parents:
70780
diff
changeset
|
300 |
state. |
22aeec526ffd
support for PIDE markup in batch build (inactive due to pide_reports=false);
wenzelm
parents:
70780
diff
changeset
|
301 |
add_status(markup). |
22aeec526ffd
support for PIDE markup in batch build (inactive due to pide_reports=false);
wenzelm
parents:
70780
diff
changeset
|
302 |
add_markup(true, Symbol.Text_Chunk.Default, Text.Info(command.core_range, elem)) |
22aeec526ffd
support for PIDE markup in batch build (inactive due to pide_reports=false);
wenzelm
parents:
70780
diff
changeset
|
303 |
case _ => |
22aeec526ffd
support for PIDE markup in batch build (inactive due to pide_reports=false);
wenzelm
parents:
70780
diff
changeset
|
304 |
Output.warning("Ignored status message: " + msg) |
22aeec526ffd
support for PIDE markup in batch build (inactive due to pide_reports=false);
wenzelm
parents:
70780
diff
changeset
|
305 |
state |
22aeec526ffd
support for PIDE markup in batch build (inactive due to pide_reports=false);
wenzelm
parents:
70780
diff
changeset
|
306 |
}) |
22aeec526ffd
support for PIDE markup in batch build (inactive due to pide_reports=false);
wenzelm
parents:
70780
diff
changeset
|
307 |
} |
38581
d503a0912e14
simplified Command.status again, reverting most of e5eed57913d0 (note that more complex information can be represented with full markup reports);
wenzelm
parents:
38579
diff
changeset
|
308 |
|
72709
cb9d5af781b4
more complete report positions, notably for command 'back' (amending eca176f773e0);
wenzelm
parents:
72708
diff
changeset
|
309 |
case XML.Elem(Markup(Markup.REPORT, atts0), msgs) => |
38572
0fe2c01ef7da
Command.State: accumulate markup reports uniformly;
wenzelm
parents:
38564
diff
changeset
|
310 |
(this /: msgs)((state, msg) => |
55432
9c53198dbb1c
maintain multiple command chunks and markup trees: for main chunk and loaded files;
wenzelm
parents:
55431
diff
changeset
|
311 |
{ |
56782
433cf57550fa
more systematic Isabelle output, like in classic Isabelle/ML (without markup);
wenzelm
parents:
56746
diff
changeset
|
312 |
def bad(): Unit = Output.warning("Ignored report message: " + msg) |
55432
9c53198dbb1c
maintain multiple command chunks and markup trees: for main chunk and loaded files;
wenzelm
parents:
55431
diff
changeset
|
313 |
|
9c53198dbb1c
maintain multiple command chunks and markup trees: for main chunk and loaded files;
wenzelm
parents:
55431
diff
changeset
|
314 |
msg match { |
72709
cb9d5af781b4
more complete report positions, notably for command 'back' (amending eca176f773e0);
wenzelm
parents:
72708
diff
changeset
|
315 |
case XML.Elem(Markup(name, atts1), args) => |
cb9d5af781b4
more complete report positions, notably for command 'back' (amending eca176f773e0);
wenzelm
parents:
72708
diff
changeset
|
316 |
val atts = atts1 ::: atts0 |
72692
22aeec526ffd
support for PIDE markup in batch build (inactive due to pide_reports=false);
wenzelm
parents:
70780
diff
changeset
|
317 |
command.reported_position(atts) match { |
22aeec526ffd
support for PIDE markup in batch build (inactive due to pide_reports=false);
wenzelm
parents:
70780
diff
changeset
|
318 |
case Some((id, chunk_name)) => |
22aeec526ffd
support for PIDE markup in batch build (inactive due to pide_reports=false);
wenzelm
parents:
70780
diff
changeset
|
319 |
val target = |
22aeec526ffd
support for PIDE markup in batch build (inactive due to pide_reports=false);
wenzelm
parents:
70780
diff
changeset
|
320 |
if (self_id(id) && command.chunks.isDefinedAt(chunk_name)) |
22aeec526ffd
support for PIDE markup in batch build (inactive due to pide_reports=false);
wenzelm
parents:
70780
diff
changeset
|
321 |
Some((chunk_name, command.chunks(chunk_name))) |
72780 | 322 |
else if (chunk_name == Symbol.Text_Chunk.Default) |
323 |
other_id(command.node_name, id) |
|
72692
22aeec526ffd
support for PIDE markup in batch build (inactive due to pide_reports=false);
wenzelm
parents:
70780
diff
changeset
|
324 |
else None |
56470
8eda56033203
accumulate markup reports for "other" command ids, which are later retargeted and merged for rendering (in erratic order);
wenzelm
parents:
56469
diff
changeset
|
325 |
|
72692
22aeec526ffd
support for PIDE markup in batch build (inactive due to pide_reports=false);
wenzelm
parents:
70780
diff
changeset
|
326 |
(target, atts) match { |
22aeec526ffd
support for PIDE markup in batch build (inactive due to pide_reports=false);
wenzelm
parents:
70780
diff
changeset
|
327 |
case (Some((target_name, target_chunk)), Position.Range(symbol_range)) => |
22aeec526ffd
support for PIDE markup in batch build (inactive due to pide_reports=false);
wenzelm
parents:
70780
diff
changeset
|
328 |
target_chunk.incorporate(symbol_range) match { |
22aeec526ffd
support for PIDE markup in batch build (inactive due to pide_reports=false);
wenzelm
parents:
70780
diff
changeset
|
329 |
case Some(range) => |
72708 | 330 |
val props = atts.filterNot(Markup.position_property) |
72692
22aeec526ffd
support for PIDE markup in batch build (inactive due to pide_reports=false);
wenzelm
parents:
70780
diff
changeset
|
331 |
val elem = xml_cache.elem(XML.Elem(Markup(name, props), args)) |
22aeec526ffd
support for PIDE markup in batch build (inactive due to pide_reports=false);
wenzelm
parents:
70780
diff
changeset
|
332 |
state.add_markup(false, target_name, Text.Info(range, elem)) |
22aeec526ffd
support for PIDE markup in batch build (inactive due to pide_reports=false);
wenzelm
parents:
70780
diff
changeset
|
333 |
case None => bad(); state |
22aeec526ffd
support for PIDE markup in batch build (inactive due to pide_reports=false);
wenzelm
parents:
70780
diff
changeset
|
334 |
} |
22aeec526ffd
support for PIDE markup in batch build (inactive due to pide_reports=false);
wenzelm
parents:
70780
diff
changeset
|
335 |
case _ => |
22aeec526ffd
support for PIDE markup in batch build (inactive due to pide_reports=false);
wenzelm
parents:
70780
diff
changeset
|
336 |
// silently ignore excessive reports |
22aeec526ffd
support for PIDE markup in batch build (inactive due to pide_reports=false);
wenzelm
parents:
70780
diff
changeset
|
337 |
state |
55432
9c53198dbb1c
maintain multiple command chunks and markup trees: for main chunk and loaded files;
wenzelm
parents:
55431
diff
changeset
|
338 |
} |
9c53198dbb1c
maintain multiple command chunks and markup trees: for main chunk and loaded files;
wenzelm
parents:
55431
diff
changeset
|
339 |
|
72692
22aeec526ffd
support for PIDE markup in batch build (inactive due to pide_reports=false);
wenzelm
parents:
70780
diff
changeset
|
340 |
case _ => bad(); state |
22aeec526ffd
support for PIDE markup in batch build (inactive due to pide_reports=false);
wenzelm
parents:
70780
diff
changeset
|
341 |
} |
56470
8eda56033203
accumulate markup reports for "other" command ids, which are later retargeted and merged for rendering (in erratic order);
wenzelm
parents:
56469
diff
changeset
|
342 |
case _ => bad(); state |
55432
9c53198dbb1c
maintain multiple command chunks and markup trees: for main chunk and loaded files;
wenzelm
parents:
55431
diff
changeset
|
343 |
} |
38361 | 344 |
}) |
72692
22aeec526ffd
support for PIDE markup in batch build (inactive due to pide_reports=false);
wenzelm
parents:
70780
diff
changeset
|
345 |
|
52930
5fab62ae3532
retain original messages properties, e.g. for retrieval via Command.Results;
wenzelm
parents:
52849
diff
changeset
|
346 |
case XML.Elem(Markup(name, props), body) => |
5fab62ae3532
retain original messages properties, e.g. for retrieval via Command.Results;
wenzelm
parents:
52849
diff
changeset
|
347 |
props match { |
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
50163
diff
changeset
|
348 |
case Markup.Serial(i) => |
67825 | 349 |
val markup_message = |
350 |
xml_cache.elem(XML.Elem(Markup(Markup.message(name), props), body)) |
|
351 |
val message_markup = |
|
352 |
xml_cache.elem(XML.elem(Markup(name, props.filter(p => p._1 == Markup.SERIAL)))) |
|
50163
c62ce309dc26
more abstract Sendback operations, with explicit id/exec_id properties;
wenzelm
parents:
50158
diff
changeset
|
353 |
|
67826 | 354 |
var st = add_result(i -> markup_message) |
55433
d2960d67f163
clarified message_positions: cover alt_id as well;
wenzelm
parents:
55432
diff
changeset
|
355 |
if (Protocol.is_inlined(message)) { |
d2960d67f163
clarified message_positions: cover alt_id as well;
wenzelm
parents:
55432
diff
changeset
|
356 |
for { |
56469 | 357 |
(chunk_name, chunk) <- command.chunks.iterator |
72692
22aeec526ffd
support for PIDE markup in batch build (inactive due to pide_reports=false);
wenzelm
parents:
70780
diff
changeset
|
358 |
range <- command.message_positions(self_id, chunk_name, chunk, message) |
67824
661cd25304ae
more compact markup tree: output messages are already stored in command results (e.g. relevant for XML data representation);
wenzelm
parents:
67446
diff
changeset
|
359 |
} st = st.add_markup(false, chunk_name, Text.Info(range, message_markup)) |
55433
d2960d67f163
clarified message_positions: cover alt_id as well;
wenzelm
parents:
55432
diff
changeset
|
360 |
} |
d2960d67f163
clarified message_positions: cover alt_id as well;
wenzelm
parents:
55432
diff
changeset
|
361 |
st |
55432
9c53198dbb1c
maintain multiple command chunks and markup trees: for main chunk and loaded files;
wenzelm
parents:
55431
diff
changeset
|
362 |
|
52536 | 363 |
case _ => |
56782
433cf57550fa
more systematic Isabelle output, like in classic Isabelle/ML (without markup);
wenzelm
parents:
56746
diff
changeset
|
364 |
Output.warning("Ignored message without serial number: " + message) |
52536 | 365 |
this |
38872 | 366 |
} |
68101 | 367 |
} |
38361 | 368 |
} |
38367 | 369 |
|
370 |
||
55431
e0f20a44ff9d
common Command.Chunk for command source and auxiliary files (static Symbol.Index without actual String content);
wenzelm
parents:
55430
diff
changeset
|
371 |
|
e0f20a44ff9d
common Command.Chunk for command source and auxiliary files (static Symbol.Index without actual String content);
wenzelm
parents:
55430
diff
changeset
|
372 |
/** static content **/ |
e0f20a44ff9d
common Command.Chunk for command source and auxiliary files (static Symbol.Index without actual String content);
wenzelm
parents:
55430
diff
changeset
|
373 |
|
45644 | 374 |
/* make commands */ |
375 |
||
55648
38f264741609
tuned signature -- avoid obscure default arguments;
wenzelm
parents:
55622
diff
changeset
|
376 |
def apply( |
38f264741609
tuned signature -- avoid obscure default arguments;
wenzelm
parents:
55622
diff
changeset
|
377 |
id: Document_ID.Command, |
38f264741609
tuned signature -- avoid obscure default arguments;
wenzelm
parents:
55622
diff
changeset
|
378 |
node_name: Document.Node.Name, |
59702
58dfaa369c11
hybrid use of command blobs: inlined errors and auxiliary files;
wenzelm
parents:
59699
diff
changeset
|
379 |
blobs_info: Blobs_Info, |
57905
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
57904
diff
changeset
|
380 |
span: Command_Span.Span): Command = |
55648
38f264741609
tuned signature -- avoid obscure default arguments;
wenzelm
parents:
55622
diff
changeset
|
381 |
{ |
57901
e1abca2527da
more explicit type Span in Scala, according to ML version;
wenzelm
parents:
57842
diff
changeset
|
382 |
val (source, span1) = span.compact_source |
72722
ade53fbc6f03
clarified signature: initial markup is_empty, not init_markup;
wenzelm
parents:
72709
diff
changeset
|
383 |
new Command(id, node_name, blobs_info, span1, source, Results.empty, Markups.empty) |
55648
38f264741609
tuned signature -- avoid obscure default arguments;
wenzelm
parents:
55622
diff
changeset
|
384 |
} |
49414 | 385 |
|
57901
e1abca2527da
more explicit type Span in Scala, according to ML version;
wenzelm
parents:
57842
diff
changeset
|
386 |
val empty: Command = |
72814 | 387 |
Command(Document_ID.none, Document.Node.Name.empty, Blobs_Info.none, Command_Span.empty) |
55648
38f264741609
tuned signature -- avoid obscure default arguments;
wenzelm
parents:
55622
diff
changeset
|
388 |
|
38f264741609
tuned signature -- avoid obscure default arguments;
wenzelm
parents:
55622
diff
changeset
|
389 |
def unparsed( |
38f264741609
tuned signature -- avoid obscure default arguments;
wenzelm
parents:
55622
diff
changeset
|
390 |
source: String, |
72692
22aeec526ffd
support for PIDE markup in batch build (inactive due to pide_reports=false);
wenzelm
parents:
70780
diff
changeset
|
391 |
theory: Boolean = false, |
22aeec526ffd
support for PIDE markup in batch build (inactive due to pide_reports=false);
wenzelm
parents:
70780
diff
changeset
|
392 |
id: Document_ID.Command = Document_ID.none, |
22aeec526ffd
support for PIDE markup in batch build (inactive due to pide_reports=false);
wenzelm
parents:
70780
diff
changeset
|
393 |
node_name: Document.Node.Name = Document.Node.Name.empty, |
72816
ea4f86914cb2
support for PIDE markup for auxiliary files ("blobs");
wenzelm
parents:
72814
diff
changeset
|
394 |
blobs_info: Blobs_Info = Blobs_Info.none, |
72692
22aeec526ffd
support for PIDE markup in batch build (inactive due to pide_reports=false);
wenzelm
parents:
70780
diff
changeset
|
395 |
results: Results = Results.empty, |
72722
ade53fbc6f03
clarified signature: initial markup is_empty, not init_markup;
wenzelm
parents:
72709
diff
changeset
|
396 |
markups: Markups = Markups.empty): Command = |
55648
38f264741609
tuned signature -- avoid obscure default arguments;
wenzelm
parents:
55622
diff
changeset
|
397 |
{ |
72692
22aeec526ffd
support for PIDE markup in batch build (inactive due to pide_reports=false);
wenzelm
parents:
70780
diff
changeset
|
398 |
val (source1, span1) = Command_Span.unparsed(source, theory).compact_source |
72816
ea4f86914cb2
support for PIDE markup for auxiliary files ("blobs");
wenzelm
parents:
72814
diff
changeset
|
399 |
new Command(id, node_name, blobs_info, span1, source1, results, markups) |
55648
38f264741609
tuned signature -- avoid obscure default arguments;
wenzelm
parents:
55622
diff
changeset
|
400 |
} |
49414 | 401 |
|
72692
22aeec526ffd
support for PIDE markup in batch build (inactive due to pide_reports=false);
wenzelm
parents:
70780
diff
changeset
|
402 |
def text(source: String): Command = unparsed(source) |
44384 | 403 |
|
52530
99dd8b4ef3fe
explicit module Document_ID as source of globally unique identifiers across ML/Scala;
wenzelm
parents:
52527
diff
changeset
|
404 |
def rich_text(id: Document_ID.Command, results: Results, body: XML.Body): Command = |
72722
ade53fbc6f03
clarified signature: initial markup is_empty, not init_markup;
wenzelm
parents:
72709
diff
changeset
|
405 |
unparsed(XML.content(body), id = id, results = results, |
ade53fbc6f03
clarified signature: initial markup is_empty, not init_markup;
wenzelm
parents:
72709
diff
changeset
|
406 |
markups = Markups.init(Markup_Tree.from_XML(body))) |
49359
c1262d7389fb
refined output panel: more value-oriented approach to update and caret focus;
wenzelm
parents:
49037
diff
changeset
|
407 |
|
44384 | 408 |
|
72814 | 409 |
/* edits and perspective */ |
410 |
||
411 |
type Edit = (Option[Command], Option[Command]) |
|
44384 | 412 |
|
44474 | 413 |
object Perspective |
414 |
{ |
|
415 |
val empty: Perspective = Perspective(Nil) |
|
416 |
} |
|
44385
e7fdb008aa7d
propagate editor perspective through document model;
wenzelm
parents:
44384
diff
changeset
|
417 |
|
44474 | 418 |
sealed case class Perspective(commands: List[Command]) // visible commands in canonical order |
44385
e7fdb008aa7d
propagate editor perspective through document model;
wenzelm
parents:
44384
diff
changeset
|
419 |
{ |
57615
df1b3452d71c
more explicit discrimination of empty nodes -- suppress from Theories panel;
wenzelm
parents:
56782
diff
changeset
|
420 |
def is_empty: Boolean = commands.isEmpty |
df1b3452d71c
more explicit discrimination of empty nodes -- suppress from Theories panel;
wenzelm
parents:
56782
diff
changeset
|
421 |
|
44474 | 422 |
def same(that: Perspective): Boolean = |
423 |
{ |
|
424 |
val cmds1 = this.commands |
|
425 |
val cmds2 = that.commands |
|
48754
c2c1e5944536
clarified undefined, unparsed, unfinished command spans;
wenzelm
parents:
48745
diff
changeset
|
426 |
require(!cmds1.exists(_.is_undefined)) |
c2c1e5944536
clarified undefined, unparsed, unfinished command spans;
wenzelm
parents:
48745
diff
changeset
|
427 |
require(!cmds2.exists(_.is_undefined)) |
44474 | 428 |
cmds1.length == cmds2.length && |
429 |
(cmds1.iterator zip cmds2.iterator).forall({ case (c1, c2) => c1.id == c2.id }) |
|
430 |
} |
|
44385
e7fdb008aa7d
propagate editor perspective through document model;
wenzelm
parents:
44384
diff
changeset
|
431 |
} |
59689
7968c57ea240
simplified Command.resolve_files in ML, using blobs_index from Scala;
wenzelm
parents:
59684
diff
changeset
|
432 |
|
7968c57ea240
simplified Command.resolve_files in ML, using blobs_index from Scala;
wenzelm
parents:
59684
diff
changeset
|
433 |
|
59702
58dfaa369c11
hybrid use of command blobs: inlined errors and auxiliary files;
wenzelm
parents:
59699
diff
changeset
|
434 |
/* blobs: inlined errors and auxiliary files */ |
59689
7968c57ea240
simplified Command.resolve_files in ML, using blobs_index from Scala;
wenzelm
parents:
59684
diff
changeset
|
435 |
|
59702
58dfaa369c11
hybrid use of command blobs: inlined errors and auxiliary files;
wenzelm
parents:
59699
diff
changeset
|
436 |
def blobs_info( |
59699 | 437 |
resources: Resources, |
63584
68751fe1c036
tuned signature -- prover-independence is presently theoretical;
wenzelm
parents:
62969
diff
changeset
|
438 |
syntax: Outer_Syntax, |
59699 | 439 |
get_blob: Document.Node.Name => Option[Document.Blob], |
59702
58dfaa369c11
hybrid use of command blobs: inlined errors and auxiliary files;
wenzelm
parents:
59699
diff
changeset
|
440 |
can_import: Document.Node.Name => Boolean, |
59699 | 441 |
node_name: Document.Node.Name, |
59702
58dfaa369c11
hybrid use of command blobs: inlined errors and auxiliary files;
wenzelm
parents:
59699
diff
changeset
|
442 |
span: Command_Span.Span): Blobs_Info = |
59689
7968c57ea240
simplified Command.resolve_files in ML, using blobs_index from Scala;
wenzelm
parents:
59684
diff
changeset
|
443 |
{ |
59735 | 444 |
span.name match { |
59702
58dfaa369c11
hybrid use of command blobs: inlined errors and auxiliary files;
wenzelm
parents:
59699
diff
changeset
|
445 |
// inlined errors |
59735 | 446 |
case Thy_Header.THEORY => |
64825 | 447 |
val reader = Scan.char_reader(Token.implode(span.content)) |
72772 | 448 |
val header = resources.check_thy(node_name, reader) |
72748
04d5f6d769a7
more flexible syntax for theory load commands via Isabelle/Scala;
wenzelm
parents:
72747
diff
changeset
|
449 |
val imports_pos = header.imports_pos |
66768 | 450 |
val raw_imports = |
451 |
try { |
|
72778 | 452 |
val read_imports = Thy_Header.read(node_name, reader).imports.map(_._1) |
70638
f164cec7ac22
clarified signature: prefer operations without position;
wenzelm
parents:
69891
diff
changeset
|
453 |
if (imports_pos.length == read_imports.length) read_imports else error("") |
66768 | 454 |
} |
72778 | 455 |
catch { case _: Throwable => List.fill(header.imports.length)("") } |
66768 | 456 |
|
72765 | 457 |
val errors = |
70638
f164cec7ac22
clarified signature: prefer operations without position;
wenzelm
parents:
69891
diff
changeset
|
458 |
for { ((import_name, pos), s) <- imports_pos zip raw_imports if !can_import(import_name) } |
66768 | 459 |
yield { |
460 |
val completion = |
|
70713
fd188463066e
clarified theory imports completion, based on session directories and current master directory (no support for local session-subdirectories);
wenzelm
parents:
70638
diff
changeset
|
461 |
if (Thy_Header.is_base_name(s)) resources.complete_import_name(node_name, s) else Nil |
72814 | 462 |
"Bad theory import " + |
463 |
Markup.Path(import_name.node).markup(quote(import_name.toString)) + |
|
464 |
Position.here(pos) + Completion.report_theories(pos, completion) |
|
59708
aed304412e43
more markup, which helps to create missing imports;
wenzelm
parents:
59706
diff
changeset
|
465 |
} |
72814 | 466 |
Blobs_Info.errors(errors) |
59702
58dfaa369c11
hybrid use of command blobs: inlined errors and auxiliary files;
wenzelm
parents:
59699
diff
changeset
|
467 |
|
58dfaa369c11
hybrid use of command blobs: inlined errors and auxiliary files;
wenzelm
parents:
59699
diff
changeset
|
468 |
// auxiliary files |
58dfaa369c11
hybrid use of command blobs: inlined errors and auxiliary files;
wenzelm
parents:
59699
diff
changeset
|
469 |
case _ => |
72757 | 470 |
val loaded_files = span.loaded_files(syntax) |
59702
58dfaa369c11
hybrid use of command blobs: inlined errors and auxiliary files;
wenzelm
parents:
59699
diff
changeset
|
471 |
val blobs = |
72757 | 472 |
loaded_files.files.map(file => |
59702
58dfaa369c11
hybrid use of command blobs: inlined errors and auxiliary files;
wenzelm
parents:
59699
diff
changeset
|
473 |
(Exn.capture { |
72747
5f9d66155081
clarified theory keywords: loaded_files are determined statically in Scala, but ML needs to do it semantically;
wenzelm
parents:
72745
diff
changeset
|
474 |
val src_path = Path.explode(file) |
5f9d66155081
clarified theory keywords: loaded_files are determined statically in Scala, but ML needs to do it semantically;
wenzelm
parents:
72745
diff
changeset
|
475 |
val name = Document.Node.Name(resources.append(node_name, src_path)) |
72745 | 476 |
val content = get_blob(name).map(blob => (blob.bytes.sha1_digest, blob.chunk)) |
72747
5f9d66155081
clarified theory keywords: loaded_files are determined statically in Scala, but ML needs to do it semantically;
wenzelm
parents:
72745
diff
changeset
|
477 |
Blob(name, src_path, content) |
59702
58dfaa369c11
hybrid use of command blobs: inlined errors and auxiliary files;
wenzelm
parents:
59699
diff
changeset
|
478 |
}).user_error) |
72814 | 479 |
Blobs_Info(blobs, loaded_files.index) |
59702
58dfaa369c11
hybrid use of command blobs: inlined errors and auxiliary files;
wenzelm
parents:
59699
diff
changeset
|
480 |
} |
59689
7968c57ea240
simplified Command.resolve_files in ML, using blobs_index from Scala;
wenzelm
parents:
59684
diff
changeset
|
481 |
} |
72816
ea4f86914cb2
support for PIDE markup for auxiliary files ("blobs");
wenzelm
parents:
72814
diff
changeset
|
482 |
|
ea4f86914cb2
support for PIDE markup for auxiliary files ("blobs");
wenzelm
parents:
72814
diff
changeset
|
483 |
def build_blobs_info( |
ea4f86914cb2
support for PIDE markup for auxiliary files ("blobs");
wenzelm
parents:
72814
diff
changeset
|
484 |
syntax: Outer_Syntax, |
ea4f86914cb2
support for PIDE markup for auxiliary files ("blobs");
wenzelm
parents:
72814
diff
changeset
|
485 |
node_name: Document.Node.Name, |
ea4f86914cb2
support for PIDE markup for auxiliary files ("blobs");
wenzelm
parents:
72814
diff
changeset
|
486 |
load_commands: List[Command_Span.Span]): Blobs_Info = |
ea4f86914cb2
support for PIDE markup for auxiliary files ("blobs");
wenzelm
parents:
72814
diff
changeset
|
487 |
{ |
ea4f86914cb2
support for PIDE markup for auxiliary files ("blobs");
wenzelm
parents:
72814
diff
changeset
|
488 |
val blobs = |
ea4f86914cb2
support for PIDE markup for auxiliary files ("blobs");
wenzelm
parents:
72814
diff
changeset
|
489 |
for { |
ea4f86914cb2
support for PIDE markup for auxiliary files ("blobs");
wenzelm
parents:
72814
diff
changeset
|
490 |
span <- load_commands |
ea4f86914cb2
support for PIDE markup for auxiliary files ("blobs");
wenzelm
parents:
72814
diff
changeset
|
491 |
file <- span.loaded_files(syntax).files |
ea4f86914cb2
support for PIDE markup for auxiliary files ("blobs");
wenzelm
parents:
72814
diff
changeset
|
492 |
} yield { |
ea4f86914cb2
support for PIDE markup for auxiliary files ("blobs");
wenzelm
parents:
72814
diff
changeset
|
493 |
(Exn.capture { |
72817
1c378ab75d48
clarified signature, notably access to blob files;
wenzelm
parents:
72816
diff
changeset
|
494 |
val dir = node_name.master_dir_path |
72816
ea4f86914cb2
support for PIDE markup for auxiliary files ("blobs");
wenzelm
parents:
72814
diff
changeset
|
495 |
val src_path = Path.explode(file) |
ea4f86914cb2
support for PIDE markup for auxiliary files ("blobs");
wenzelm
parents:
72814
diff
changeset
|
496 |
val name = Document.Node.Name((dir + src_path).expand.implode_symbolic) |
72817
1c378ab75d48
clarified signature, notably access to blob files;
wenzelm
parents:
72816
diff
changeset
|
497 |
Blob.read_file(name, src_path) |
72816
ea4f86914cb2
support for PIDE markup for auxiliary files ("blobs");
wenzelm
parents:
72814
diff
changeset
|
498 |
}).user_error |
ea4f86914cb2
support for PIDE markup for auxiliary files ("blobs");
wenzelm
parents:
72814
diff
changeset
|
499 |
} |
ea4f86914cb2
support for PIDE markup for auxiliary files ("blobs");
wenzelm
parents:
72814
diff
changeset
|
500 |
Blobs_Info(blobs, -1) |
ea4f86914cb2
support for PIDE markup for auxiliary files ("blobs");
wenzelm
parents:
72814
diff
changeset
|
501 |
} |
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
502 |
} |
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
503 |
|
38361 | 504 |
|
46712 | 505 |
final class Command private( |
52530
99dd8b4ef3fe
explicit module Document_ID as source of globally unique identifiers across ML/Scala;
wenzelm
parents:
52527
diff
changeset
|
506 |
val id: Document_ID.Command, |
44615 | 507 |
val node_name: Document.Node.Name, |
59702
58dfaa369c11
hybrid use of command blobs: inlined errors and auxiliary files;
wenzelm
parents:
59699
diff
changeset
|
508 |
val blobs_info: Command.Blobs_Info, |
57905
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
57904
diff
changeset
|
509 |
val span: Command_Span.Span, |
49414 | 510 |
val source: String, |
50501
6f41f1646617
more careful handling of Dialog_Result, with active area and color feedback;
wenzelm
parents:
50500
diff
changeset
|
511 |
val init_results: Command.Results, |
72722
ade53fbc6f03
clarified signature: initial markup is_empty, not init_markup;
wenzelm
parents:
72709
diff
changeset
|
512 |
val init_markups: Command.Markups) |
34451 | 513 |
{ |
57912 | 514 |
override def toString: String = id + "/" + span.kind.toString |
34495 | 515 |
|
57910 | 516 |
|
517 |
/* classification */ |
|
518 |
||
57905
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
57904
diff
changeset
|
519 |
def is_proper: Boolean = span.kind.isInstanceOf[Command_Span.Command_Span] |
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
57904
diff
changeset
|
520 |
def is_ignored: Boolean = span.kind == Command_Span.Ignored_Span |
57904 | 521 |
|
522 |
def is_undefined: Boolean = id == Document_ID.none |
|
523 |
val is_unparsed: Boolean = span.content.exists(_.is_unparsed) |
|
524 |
val is_unfinished: Boolean = span.content.exists(_.is_unfinished) |
|
525 |
||
68323 | 526 |
def potentially_initialized: Boolean = span.name == Thy_Header.THEORY |
527 |
||
34859 | 528 |
|
54519
5fed81762406
maintain blobs within document state: digest + text in ML, digest-only in Scala;
wenzelm
parents:
54517
diff
changeset
|
529 |
/* blobs */ |
5fed81762406
maintain blobs within document state: digest + text in ML, digest-only in Scala;
wenzelm
parents:
54517
diff
changeset
|
530 |
|
72814 | 531 |
def blobs: List[Exn.Result[Command.Blob]] = blobs_info.blobs |
532 |
def blobs_index: Int = blobs_info.index |
|
59702
58dfaa369c11
hybrid use of command blobs: inlined errors and auxiliary files;
wenzelm
parents:
59699
diff
changeset
|
533 |
|
65335 | 534 |
def blobs_ok: Boolean = |
535 |
blobs.forall({ case Exn.Res(_) => true case _ => false }) |
|
536 |
||
54530
2c1440f70028
ranges of thy_load commands count as visible within perspective;
wenzelm
parents:
54524
diff
changeset
|
537 |
def blobs_names: List[Document.Node.Name] = |
72745 | 538 |
for (Exn.Res(blob) <- blobs) yield blob.name |
54530
2c1440f70028
ranges of thy_load commands count as visible within perspective;
wenzelm
parents:
54524
diff
changeset
|
539 |
|
60916
a6e2a667b0a8
resolve undefined blobs by default, e.g. relevant for ML debugger to avoid reset of breakpoints after reload;
wenzelm
parents:
60215
diff
changeset
|
540 |
def blobs_undefined: List[Document.Node.Name] = |
72745 | 541 |
for (Exn.Res(blob) <- blobs if blob.content.isEmpty) yield blob.name |
60916
a6e2a667b0a8
resolve undefined blobs by default, e.g. relevant for ML debugger to avoid reset of breakpoints after reload;
wenzelm
parents:
60215
diff
changeset
|
542 |
|
57842
8e4ae2db1849
more direct access to persistent blobs (see also 8953d4cc060a), avoiding fragile digest lookup from later version (which might have removed unused blobs already);
wenzelm
parents:
57615
diff
changeset
|
543 |
def blobs_defined: List[(Document.Node.Name, SHA1.Digest)] = |
72745 | 544 |
for (Exn.Res(blob) <- blobs; (digest, _) <- blob.content) yield (blob.name, digest) |
57842
8e4ae2db1849
more direct access to persistent blobs (see also 8953d4cc060a), avoiding fragile digest lookup from later version (which might have removed unused blobs already);
wenzelm
parents:
57615
diff
changeset
|
545 |
|
8e4ae2db1849
more direct access to persistent blobs (see also 8953d4cc060a), avoiding fragile digest lookup from later version (which might have removed unused blobs already);
wenzelm
parents:
57615
diff
changeset
|
546 |
def blobs_changed(doc_blobs: Document.Blobs): Boolean = |
72745 | 547 |
blobs.exists({ case Exn.Res(blob) => doc_blobs.changed(blob.name) case _ => false }) |
54519
5fed81762406
maintain blobs within document state: digest + text in ML, digest-only in Scala;
wenzelm
parents:
54517
diff
changeset
|
548 |
|
55432
9c53198dbb1c
maintain multiple command chunks and markup trees: for main chunk and loaded files;
wenzelm
parents:
55431
diff
changeset
|
549 |
|
56462
b64b0cb845fe
more explicit Command.Chunk types, less ooddities;
wenzelm
parents:
56395
diff
changeset
|
550 |
/* source chunks */ |
55431
e0f20a44ff9d
common Command.Chunk for command source and auxiliary files (static Symbol.Index without actual String content);
wenzelm
parents:
55430
diff
changeset
|
551 |
|
56746 | 552 |
val chunk: Symbol.Text_Chunk = Symbol.Text_Chunk(source) |
56473 | 553 |
|
56746 | 554 |
val chunks: Map[Symbol.Text_Chunk.Name, Symbol.Text_Chunk] = |
555 |
((Symbol.Text_Chunk.Default -> chunk) :: |
|
72745 | 556 |
(for (Exn.Res(blob) <- blobs; (_, file) <- blob.content) |
72816
ea4f86914cb2
support for PIDE markup for auxiliary files ("blobs");
wenzelm
parents:
72814
diff
changeset
|
557 |
yield blob.chunk_file -> file)).toMap |
56473 | 558 |
|
46813 | 559 |
def length: Int = source.length |
56473 | 560 |
def range: Text.Range = chunk.range |
46813 | 561 |
|
68728 | 562 |
val core_range: Text.Range = |
57901
e1abca2527da
more explicit type Span in Scala, according to ML version;
wenzelm
parents:
57842
diff
changeset
|
563 |
Text.Range(0, |
68729
3a02b424d5fb
clarified ignored span / core range: include formal comments, e.g. relevant for error messages from antiquotations;
wenzelm
parents:
68728
diff
changeset
|
564 |
(length /: span.content.reverse.iterator.takeWhile(_.is_ignored))(_ - _.source.length)) |
46813 | 565 |
|
65522 | 566 |
def source(range: Text.Range): String = range.substring(source) |
38572
0fe2c01ef7da
Command.State: accumulate markup reports uniformly;
wenzelm
parents:
38564
diff
changeset
|
567 |
|
38370
8b15d0f98962
explicit Document.State value, instead of individual state variables in Session, Command, Document;
wenzelm
parents:
38367
diff
changeset
|
568 |
|
72692
22aeec526ffd
support for PIDE markup in batch build (inactive due to pide_reports=false);
wenzelm
parents:
70780
diff
changeset
|
569 |
/* reported positions */ |
22aeec526ffd
support for PIDE markup in batch build (inactive due to pide_reports=false);
wenzelm
parents:
70780
diff
changeset
|
570 |
|
22aeec526ffd
support for PIDE markup in batch build (inactive due to pide_reports=false);
wenzelm
parents:
70780
diff
changeset
|
571 |
def reported_position(pos: Position.T): Option[(Document_ID.Generic, Symbol.Text_Chunk.Name)] = |
22aeec526ffd
support for PIDE markup in batch build (inactive due to pide_reports=false);
wenzelm
parents:
70780
diff
changeset
|
572 |
pos match { |
22aeec526ffd
support for PIDE markup in batch build (inactive due to pide_reports=false);
wenzelm
parents:
70780
diff
changeset
|
573 |
case Position.Id(id) => |
22aeec526ffd
support for PIDE markup in batch build (inactive due to pide_reports=false);
wenzelm
parents:
70780
diff
changeset
|
574 |
val chunk_name = |
22aeec526ffd
support for PIDE markup in batch build (inactive due to pide_reports=false);
wenzelm
parents:
70780
diff
changeset
|
575 |
pos match { |
22aeec526ffd
support for PIDE markup in batch build (inactive due to pide_reports=false);
wenzelm
parents:
70780
diff
changeset
|
576 |
case Position.File(name) if name != node_name.node => |
22aeec526ffd
support for PIDE markup in batch build (inactive due to pide_reports=false);
wenzelm
parents:
70780
diff
changeset
|
577 |
Symbol.Text_Chunk.File(name) |
22aeec526ffd
support for PIDE markup in batch build (inactive due to pide_reports=false);
wenzelm
parents:
70780
diff
changeset
|
578 |
case _ => Symbol.Text_Chunk.Default |
22aeec526ffd
support for PIDE markup in batch build (inactive due to pide_reports=false);
wenzelm
parents:
70780
diff
changeset
|
579 |
} |
22aeec526ffd
support for PIDE markup in batch build (inactive due to pide_reports=false);
wenzelm
parents:
70780
diff
changeset
|
580 |
Some((id, chunk_name)) |
22aeec526ffd
support for PIDE markup in batch build (inactive due to pide_reports=false);
wenzelm
parents:
70780
diff
changeset
|
581 |
case _ => None |
22aeec526ffd
support for PIDE markup in batch build (inactive due to pide_reports=false);
wenzelm
parents:
70780
diff
changeset
|
582 |
} |
22aeec526ffd
support for PIDE markup in batch build (inactive due to pide_reports=false);
wenzelm
parents:
70780
diff
changeset
|
583 |
|
22aeec526ffd
support for PIDE markup in batch build (inactive due to pide_reports=false);
wenzelm
parents:
70780
diff
changeset
|
584 |
def message_positions( |
22aeec526ffd
support for PIDE markup in batch build (inactive due to pide_reports=false);
wenzelm
parents:
70780
diff
changeset
|
585 |
self_id: Document_ID.Generic => Boolean, |
22aeec526ffd
support for PIDE markup in batch build (inactive due to pide_reports=false);
wenzelm
parents:
70780
diff
changeset
|
586 |
chunk_name: Symbol.Text_Chunk.Name, |
22aeec526ffd
support for PIDE markup in batch build (inactive due to pide_reports=false);
wenzelm
parents:
70780
diff
changeset
|
587 |
chunk: Symbol.Text_Chunk, |
22aeec526ffd
support for PIDE markup in batch build (inactive due to pide_reports=false);
wenzelm
parents:
70780
diff
changeset
|
588 |
message: XML.Elem): Set[Text.Range] = |
22aeec526ffd
support for PIDE markup in batch build (inactive due to pide_reports=false);
wenzelm
parents:
70780
diff
changeset
|
589 |
{ |
22aeec526ffd
support for PIDE markup in batch build (inactive due to pide_reports=false);
wenzelm
parents:
70780
diff
changeset
|
590 |
def elem(props: Properties.T, set: Set[Text.Range]): Set[Text.Range] = |
22aeec526ffd
support for PIDE markup in batch build (inactive due to pide_reports=false);
wenzelm
parents:
70780
diff
changeset
|
591 |
reported_position(props) match { |
22aeec526ffd
support for PIDE markup in batch build (inactive due to pide_reports=false);
wenzelm
parents:
70780
diff
changeset
|
592 |
case Some((id, name)) if self_id(id) && name == chunk_name => |
22aeec526ffd
support for PIDE markup in batch build (inactive due to pide_reports=false);
wenzelm
parents:
70780
diff
changeset
|
593 |
val opt_range = |
22aeec526ffd
support for PIDE markup in batch build (inactive due to pide_reports=false);
wenzelm
parents:
70780
diff
changeset
|
594 |
Position.Range.unapply(props) orElse { |
22aeec526ffd
support for PIDE markup in batch build (inactive due to pide_reports=false);
wenzelm
parents:
70780
diff
changeset
|
595 |
if (name == Symbol.Text_Chunk.Default) |
22aeec526ffd
support for PIDE markup in batch build (inactive due to pide_reports=false);
wenzelm
parents:
70780
diff
changeset
|
596 |
Position.Range.unapply(span.position) |
22aeec526ffd
support for PIDE markup in batch build (inactive due to pide_reports=false);
wenzelm
parents:
70780
diff
changeset
|
597 |
else None |
22aeec526ffd
support for PIDE markup in batch build (inactive due to pide_reports=false);
wenzelm
parents:
70780
diff
changeset
|
598 |
} |
22aeec526ffd
support for PIDE markup in batch build (inactive due to pide_reports=false);
wenzelm
parents:
70780
diff
changeset
|
599 |
opt_range match { |
22aeec526ffd
support for PIDE markup in batch build (inactive due to pide_reports=false);
wenzelm
parents:
70780
diff
changeset
|
600 |
case Some(symbol_range) => |
22aeec526ffd
support for PIDE markup in batch build (inactive due to pide_reports=false);
wenzelm
parents:
70780
diff
changeset
|
601 |
chunk.incorporate(symbol_range) match { |
22aeec526ffd
support for PIDE markup in batch build (inactive due to pide_reports=false);
wenzelm
parents:
70780
diff
changeset
|
602 |
case Some(range) => set + range |
22aeec526ffd
support for PIDE markup in batch build (inactive due to pide_reports=false);
wenzelm
parents:
70780
diff
changeset
|
603 |
case _ => set |
22aeec526ffd
support for PIDE markup in batch build (inactive due to pide_reports=false);
wenzelm
parents:
70780
diff
changeset
|
604 |
} |
22aeec526ffd
support for PIDE markup in batch build (inactive due to pide_reports=false);
wenzelm
parents:
70780
diff
changeset
|
605 |
case None => set |
22aeec526ffd
support for PIDE markup in batch build (inactive due to pide_reports=false);
wenzelm
parents:
70780
diff
changeset
|
606 |
} |
22aeec526ffd
support for PIDE markup in batch build (inactive due to pide_reports=false);
wenzelm
parents:
70780
diff
changeset
|
607 |
case _ => set |
22aeec526ffd
support for PIDE markup in batch build (inactive due to pide_reports=false);
wenzelm
parents:
70780
diff
changeset
|
608 |
} |
22aeec526ffd
support for PIDE markup in batch build (inactive due to pide_reports=false);
wenzelm
parents:
70780
diff
changeset
|
609 |
def tree(set: Set[Text.Range], t: XML.Tree): Set[Text.Range] = |
22aeec526ffd
support for PIDE markup in batch build (inactive due to pide_reports=false);
wenzelm
parents:
70780
diff
changeset
|
610 |
t match { |
22aeec526ffd
support for PIDE markup in batch build (inactive due to pide_reports=false);
wenzelm
parents:
70780
diff
changeset
|
611 |
case XML.Wrapped_Elem(Markup(name, props), _, body) => |
22aeec526ffd
support for PIDE markup in batch build (inactive due to pide_reports=false);
wenzelm
parents:
70780
diff
changeset
|
612 |
body.foldLeft(if (Rendering.position_elements(name)) elem(props, set) else set)(tree) |
22aeec526ffd
support for PIDE markup in batch build (inactive due to pide_reports=false);
wenzelm
parents:
70780
diff
changeset
|
613 |
case XML.Elem(Markup(name, props), body) => |
22aeec526ffd
support for PIDE markup in batch build (inactive due to pide_reports=false);
wenzelm
parents:
70780
diff
changeset
|
614 |
body.foldLeft(if (Rendering.position_elements(name)) elem(props, set) else set)(tree) |
22aeec526ffd
support for PIDE markup in batch build (inactive due to pide_reports=false);
wenzelm
parents:
70780
diff
changeset
|
615 |
case XML.Text(_) => set |
22aeec526ffd
support for PIDE markup in batch build (inactive due to pide_reports=false);
wenzelm
parents:
70780
diff
changeset
|
616 |
} |
22aeec526ffd
support for PIDE markup in batch build (inactive due to pide_reports=false);
wenzelm
parents:
70780
diff
changeset
|
617 |
|
22aeec526ffd
support for PIDE markup in batch build (inactive due to pide_reports=false);
wenzelm
parents:
70780
diff
changeset
|
618 |
val set = tree(Set.empty, message) |
22aeec526ffd
support for PIDE markup in batch build (inactive due to pide_reports=false);
wenzelm
parents:
70780
diff
changeset
|
619 |
if (set.isEmpty) elem(message.markup.properties, set) |
22aeec526ffd
support for PIDE markup in batch build (inactive due to pide_reports=false);
wenzelm
parents:
70780
diff
changeset
|
620 |
else set |
22aeec526ffd
support for PIDE markup in batch build (inactive due to pide_reports=false);
wenzelm
parents:
70780
diff
changeset
|
621 |
} |
22aeec526ffd
support for PIDE markup in batch build (inactive due to pide_reports=false);
wenzelm
parents:
70780
diff
changeset
|
622 |
|
22aeec526ffd
support for PIDE markup in batch build (inactive due to pide_reports=false);
wenzelm
parents:
70780
diff
changeset
|
623 |
|
38370
8b15d0f98962
explicit Document.State value, instead of individual state variables in Session, Command, Document;
wenzelm
parents:
38367
diff
changeset
|
624 |
/* accumulated results */ |
8b15d0f98962
explicit Document.State value, instead of individual state variables in Session, Command, Document;
wenzelm
parents:
38367
diff
changeset
|
625 |
|
50501
6f41f1646617
more careful handling of Dialog_Result, with active area and color feedback;
wenzelm
parents:
50500
diff
changeset
|
626 |
val init_state: Command.State = |
72722
ade53fbc6f03
clarified signature: initial markup is_empty, not init_markup;
wenzelm
parents:
72709
diff
changeset
|
627 |
Command.State(this, results = init_results, markups = init_markups) |
52527
dbac84eab3bc
separate exec_id assignment for Command.print states, without affecting result of eval;
wenzelm
parents:
52524
diff
changeset
|
628 |
|
dbac84eab3bc
separate exec_id assignment for Command.print states, without affecting result of eval;
wenzelm
parents:
52524
diff
changeset
|
629 |
val empty_state: Command.State = Command.State(this) |
34676
9e725d34df7b
Command and Command_State handle results from prover as Accumulator
immler@in.tum.de
parents:
34675
diff
changeset
|
630 |
} |