author | wenzelm |
Fri, 08 Jan 2021 16:36:20 +0100 | |
changeset 73105 | 578a33042aa6 |
parent 72929 | 776198313227 |
child 73359 | d8a0e996614b |
permissions | -rw-r--r-- |
64622
529bbb8977c7
more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
diff
changeset
|
1 |
/* Title: Pure/PIDE/rendering.scala |
529bbb8977c7
more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
diff
changeset
|
2 |
Author: Makarius |
529bbb8977c7
more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
diff
changeset
|
3 |
|
529bbb8977c7
more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
diff
changeset
|
4 |
Isabelle-specific implementation of quasi-abstract rendering and |
529bbb8977c7
more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
diff
changeset
|
5 |
markup interpretation. |
529bbb8977c7
more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
diff
changeset
|
6 |
*/ |
529bbb8977c7
more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
diff
changeset
|
7 |
|
529bbb8977c7
more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
diff
changeset
|
8 |
package isabelle |
529bbb8977c7
more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
diff
changeset
|
9 |
|
529bbb8977c7
more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
diff
changeset
|
10 |
|
66158 | 11 |
import java.io.{File => JFile} |
12 |
import java.nio.file.FileSystems |
|
13 |
||
72869 | 14 |
import scala.collection.immutable.SortedMap |
15 |
||
16 |
||
66158 | 17 |
|
64622
529bbb8977c7
more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
diff
changeset
|
18 |
object Rendering |
529bbb8977c7
more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
diff
changeset
|
19 |
{ |
65101 | 20 |
/* color */ |
21 |
||
22 |
object Color extends Enumeration |
|
23 |
{ |
|
65104
66b19d05dcee
decorations for background and foreground colors;
wenzelm
parents:
65101
diff
changeset
|
24 |
// background |
68871
f5c76072db55
more explicit status for "canceled" command within theory node;
wenzelm
parents:
68822
diff
changeset
|
25 |
val unprocessed1, running1, canceled, bad, intensify, entity, active, active_result, |
67322 | 26 |
markdown_bullet1, markdown_bullet2, markdown_bullet3, markdown_bullet4 = Value |
71601 | 27 |
val background_colors: ValueSet = values |
65104
66b19d05dcee
decorations for background and foreground colors;
wenzelm
parents:
65101
diff
changeset
|
28 |
|
66b19d05dcee
decorations for background and foreground colors;
wenzelm
parents:
65101
diff
changeset
|
29 |
// foreground |
65637 | 30 |
val quoted, antiquoted = Value |
71601 | 31 |
val foreground_colors: ValueSet = values -- background_colors |
65121 | 32 |
|
65124 | 33 |
// message underline |
65637 | 34 |
val writeln, information, warning, legacy, error = Value |
71601 | 35 |
val message_underline_colors: ValueSet = values -- background_colors -- foreground_colors |
65124 | 36 |
|
37 |
// message background |
|
65637 | 38 |
val writeln_message, information_message, tracing_message, |
39 |
warning_message, legacy_message, error_message = Value |
|
71601 | 40 |
val message_background_colors: ValueSet = |
65143 | 41 |
values -- background_colors -- foreground_colors -- message_underline_colors |
65144 | 42 |
|
43 |
// text |
|
65637 | 44 |
val main, keyword1, keyword2, keyword3, quasi_keyword, improper, operator, |
45 |
tfree, tvar, free, skolem, bound, `var`, inner_numeral, inner_quoted, |
|
69965
da5e7278286b
more markup for various text kinds, notably for nested formal comments;
wenzelm
parents:
69916
diff
changeset
|
46 |
inner_cartouche, comment1, comment2, comment3, dynamic, class_parameter, |
da5e7278286b
more markup for various text kinds, notably for nested formal comments;
wenzelm
parents:
69916
diff
changeset
|
47 |
antiquote, raw_text, plain_text = Value |
71601 | 48 |
val text_colors: ValueSet = |
65144 | 49 |
values -- background_colors -- foreground_colors -- message_underline_colors -- |
50 |
message_background_colors |
|
65911 | 51 |
|
65913 | 52 |
// text overview |
65911 | 53 |
val unprocessed, running = Value |
65913 | 54 |
val text_overview_colors = Set(unprocessed, running, error, warning) |
65101 | 55 |
} |
56 |
||
57 |
||
65190 | 58 |
/* output messages */ |
64676 | 59 |
|
60 |
val state_pri = 1 |
|
61 |
val writeln_pri = 2 |
|
62 |
val information_pri = 3 |
|
63 |
val tracing_pri = 4 |
|
64 |
val warning_pri = 5 |
|
65 |
val legacy_pri = 6 |
|
66 |
val error_pri = 7 |
|
67 |
||
68 |
val message_pri = Map( |
|
69 |
Markup.STATE -> state_pri, |
|
70 |
Markup.STATE_MESSAGE -> state_pri, |
|
71 |
Markup.WRITELN -> writeln_pri, |
|
72 |
Markup.WRITELN_MESSAGE -> writeln_pri, |
|
73 |
Markup.INFORMATION -> information_pri, |
|
74 |
Markup.INFORMATION_MESSAGE -> information_pri, |
|
75 |
Markup.TRACING -> tracing_pri, |
|
76 |
Markup.TRACING_MESSAGE -> tracing_pri, |
|
77 |
Markup.WARNING -> warning_pri, |
|
78 |
Markup.WARNING_MESSAGE -> warning_pri, |
|
79 |
Markup.LEGACY -> legacy_pri, |
|
80 |
Markup.LEGACY_MESSAGE -> legacy_pri, |
|
81 |
Markup.ERROR -> error_pri, |
|
65133 | 82 |
Markup.ERROR_MESSAGE -> error_pri |
83 |
).withDefaultValue(0) |
|
64676 | 84 |
|
65121 | 85 |
val message_underline_color = Map( |
86 |
writeln_pri -> Color.writeln, |
|
87 |
information_pri -> Color.information, |
|
88 |
warning_pri -> Color.warning, |
|
89 |
legacy_pri -> Color.legacy, |
|
90 |
error_pri -> Color.error) |
|
91 |
||
65124 | 92 |
val message_background_color = Map( |
93 |
writeln_pri -> Color.writeln_message, |
|
94 |
information_pri -> Color.information_message, |
|
95 |
tracing_pri -> Color.tracing_message, |
|
96 |
warning_pri -> Color.warning_message, |
|
97 |
legacy_pri -> Color.legacy_message, |
|
98 |
error_pri -> Color.error_message) |
|
99 |
||
72869 | 100 |
def output_messages(results: Command.Results): List[XML.Elem] = |
65190 | 101 |
{ |
102 |
val (states, other) = |
|
72727 | 103 |
results.iterator.map(_._2).filterNot(Protocol.is_result).toList |
104 |
.partition(Protocol.is_state) |
|
65190 | 105 |
states ::: other |
106 |
} |
|
107 |
||
64676 | 108 |
|
65144 | 109 |
/* text color */ |
110 |
||
111 |
val text_color = Map( |
|
112 |
Markup.KEYWORD1 -> Color.keyword1, |
|
113 |
Markup.KEYWORD2 -> Color.keyword2, |
|
114 |
Markup.KEYWORD3 -> Color.keyword3, |
|
115 |
Markup.QUASI_KEYWORD -> Color.quasi_keyword, |
|
116 |
Markup.IMPROPER -> Color.improper, |
|
117 |
Markup.OPERATOR -> Color.operator, |
|
65145 | 118 |
Markup.STRING -> Color.main, |
119 |
Markup.ALT_STRING -> Color.main, |
|
120 |
Markup.VERBATIM -> Color.main, |
|
121 |
Markup.CARTOUCHE -> Color.main, |
|
65144 | 122 |
Markup.LITERAL -> Color.keyword1, |
65145 | 123 |
Markup.DELIMITER -> Color.main, |
65144 | 124 |
Markup.TFREE -> Color.tfree, |
125 |
Markup.TVAR -> Color.tvar, |
|
126 |
Markup.FREE -> Color.free, |
|
127 |
Markup.SKOLEM -> Color.skolem, |
|
128 |
Markup.BOUND -> Color.bound, |
|
65637 | 129 |
Markup.VAR -> Color.`var`, |
65144 | 130 |
Markup.INNER_STRING -> Color.inner_quoted, |
131 |
Markup.INNER_CARTOUCHE -> Color.inner_cartouche, |
|
132 |
Markup.DYNAMIC_FACT -> Color.dynamic, |
|
133 |
Markup.CLASS_PARAMETER -> Color.class_parameter, |
|
134 |
Markup.ANTIQUOTE -> Color.antiquote, |
|
69965
da5e7278286b
more markup for various text kinds, notably for nested formal comments;
wenzelm
parents:
69916
diff
changeset
|
135 |
Markup.RAW_TEXT -> Color.raw_text, |
da5e7278286b
more markup for various text kinds, notably for nested formal comments;
wenzelm
parents:
69916
diff
changeset
|
136 |
Markup.PLAIN_TEXT -> Color.plain_text, |
65144 | 137 |
Markup.ML_KEYWORD1 -> Color.keyword1, |
138 |
Markup.ML_KEYWORD2 -> Color.keyword2, |
|
139 |
Markup.ML_KEYWORD3 -> Color.keyword3, |
|
65145 | 140 |
Markup.ML_DELIMITER -> Color.main, |
65144 | 141 |
Markup.ML_NUMERAL -> Color.inner_numeral, |
142 |
Markup.ML_CHAR -> Color.inner_quoted, |
|
143 |
Markup.ML_STRING -> Color.inner_quoted, |
|
69320 | 144 |
Markup.ML_COMMENT -> Color.comment1, |
69970
b5a47478897a
clarified rendering, notably of \<^latex>CARTOUCHE in outer syntax;
wenzelm
parents:
69965
diff
changeset
|
145 |
Markup.COMMENT -> Color.comment1, |
69320 | 146 |
Markup.COMMENT1 -> Color.comment1, |
147 |
Markup.COMMENT2 -> Color.comment2, |
|
148 |
Markup.COMMENT3 -> Color.comment3) |
|
65144 | 149 |
|
66074 | 150 |
val foreground = |
151 |
Map( |
|
152 |
Markup.STRING -> Color.quoted, |
|
153 |
Markup.ALT_STRING -> Color.quoted, |
|
154 |
Markup.VERBATIM -> Color.quoted, |
|
155 |
Markup.CARTOUCHE -> Color.quoted, |
|
156 |
Markup.ANTIQUOTED -> Color.antiquoted) |
|
157 |
||
65144 | 158 |
|
65149 | 159 |
/* tooltips */ |
65101 | 160 |
|
65149 | 161 |
val tooltip_descriptions = |
64622
529bbb8977c7
more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
diff
changeset
|
162 |
Map( |
529bbb8977c7
more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
diff
changeset
|
163 |
Markup.CITATION -> "citation", |
529bbb8977c7
more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
diff
changeset
|
164 |
Markup.TOKEN_RANGE -> "inner syntax token", |
529bbb8977c7
more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
diff
changeset
|
165 |
Markup.FREE -> "free variable", |
529bbb8977c7
more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
diff
changeset
|
166 |
Markup.SKOLEM -> "skolem variable", |
529bbb8977c7
more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
diff
changeset
|
167 |
Markup.BOUND -> "bound variable", |
529bbb8977c7
more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
diff
changeset
|
168 |
Markup.VAR -> "schematic variable", |
529bbb8977c7
more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
diff
changeset
|
169 |
Markup.TFREE -> "free type variable", |
529bbb8977c7
more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
diff
changeset
|
170 |
Markup.TVAR -> "schematic type variable") |
529bbb8977c7
more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
diff
changeset
|
171 |
|
65149 | 172 |
|
72900 | 173 |
/* entity focus */ |
174 |
||
175 |
object Focus |
|
176 |
{ |
|
177 |
def apply(ids: Set[Long]): Focus = new Focus(ids) |
|
178 |
val empty: Focus = apply(Set.empty) |
|
72905 | 179 |
def make(args: List[Text.Info[Focus]]): Focus = |
180 |
(empty /: args)({ case (focus1, Text.Info(_, focus2)) => focus1 ++ focus2 }) |
|
72927
69f768aff611
clarified caret focus modifier, depending on option "jedit_focus_modifier";
wenzelm
parents:
72926
diff
changeset
|
181 |
|
69f768aff611
clarified caret focus modifier, depending on option "jedit_focus_modifier";
wenzelm
parents:
72926
diff
changeset
|
182 |
val full: Focus = |
69f768aff611
clarified caret focus modifier, depending on option "jedit_focus_modifier";
wenzelm
parents:
72926
diff
changeset
|
183 |
new Focus(Set.empty) |
69f768aff611
clarified caret focus modifier, depending on option "jedit_focus_modifier";
wenzelm
parents:
72926
diff
changeset
|
184 |
{ |
69f768aff611
clarified caret focus modifier, depending on option "jedit_focus_modifier";
wenzelm
parents:
72926
diff
changeset
|
185 |
override def apply(id: Long): Boolean = true |
69f768aff611
clarified caret focus modifier, depending on option "jedit_focus_modifier";
wenzelm
parents:
72926
diff
changeset
|
186 |
override def toString: String = "Focus.full" |
69f768aff611
clarified caret focus modifier, depending on option "jedit_focus_modifier";
wenzelm
parents:
72926
diff
changeset
|
187 |
} |
72900 | 188 |
} |
189 |
||
190 |
sealed class Focus private[Rendering](protected val rep: Set[Long]) |
|
191 |
{ |
|
192 |
def defined: Boolean = rep.nonEmpty |
|
193 |
def apply(id: Long): Boolean = rep.contains(id) |
|
194 |
def + (id: Long): Focus = if (rep.contains(id)) this else new Focus(rep + id) |
|
195 |
def ++ (other: Focus): Focus = |
|
196 |
if (this eq other) this |
|
197 |
else if (rep.isEmpty) other |
|
198 |
else (this /: other.rep.iterator)(_ + _) |
|
199 |
override def toString: String = rep.mkString("Focus(", ",", ")") |
|
200 |
} |
|
201 |
||
202 |
||
65149 | 203 |
/* markup elements */ |
204 |
||
72692
22aeec526ffd
support for PIDE markup in batch build (inactive due to pide_reports=false);
wenzelm
parents:
71601
diff
changeset
|
205 |
val position_elements = |
22aeec526ffd
support for PIDE markup in batch build (inactive due to pide_reports=false);
wenzelm
parents:
71601
diff
changeset
|
206 |
Markup.Elements(Markup.BINDING, Markup.ENTITY, Markup.REPORT, Markup.POSITION) |
22aeec526ffd
support for PIDE markup in batch build (inactive due to pide_reports=false);
wenzelm
parents:
71601
diff
changeset
|
207 |
|
66053 | 208 |
val semantic_completion_elements = |
209 |
Markup.Elements(Markup.COMPLETION, Markup.NO_COMPLETION) |
|
210 |
||
211 |
val language_context_elements = |
|
212 |
Markup.Elements(Markup.STRING, Markup.ALT_STRING, Markup.VERBATIM, |
|
213 |
Markup.CARTOUCHE, Markup.COMMENT, Markup.LANGUAGE, |
|
214 |
Markup.ML_STRING, Markup.ML_COMMENT) |
|
215 |
||
216 |
val language_elements = Markup.Elements(Markup.LANGUAGE) |
|
217 |
||
218 |
val citation_elements = Markup.Elements(Markup.CITATION) |
|
219 |
||
65149 | 220 |
val active_elements = |
69650 | 221 |
Markup.Elements(Markup.DIALOG, Markup.BROWSER, Markup.GRAPHVIEW, Markup.THEORY_EXPORTS, |
65149 | 222 |
Markup.SENDBACK, Markup.JEDIT_ACTION, Markup.SIMP_TRACE_PANEL) |
223 |
||
224 |
val background_elements = |
|
68758 | 225 |
Document_Status.Command_Status.proper_elements + Markup.WRITELN_MESSAGE + |
65149 | 226 |
Markup.STATE_MESSAGE + Markup.INFORMATION_MESSAGE + |
227 |
Markup.TRACING_MESSAGE + Markup.WARNING_MESSAGE + |
|
228 |
Markup.LEGACY_MESSAGE + Markup.ERROR_MESSAGE + |
|
229 |
Markup.BAD + Markup.INTENSIFY + Markup.ENTITY + |
|
67322 | 230 |
Markup.Markdown_Bullet.name ++ active_elements |
65149 | 231 |
|
66074 | 232 |
val foreground_elements = Markup.Elements(foreground.keySet) |
233 |
||
234 |
val text_color_elements = Markup.Elements(text_color.keySet) |
|
65149 | 235 |
|
65129
06a7c2d316cf
more general tooltips, with uniform info range handling;
wenzelm
parents:
65126
diff
changeset
|
236 |
val tooltip_elements = |
64622
529bbb8977c7
more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
diff
changeset
|
237 |
Markup.Elements(Markup.LANGUAGE, Markup.EXPRESSION, Markup.TIMING, Markup.ENTITY, |
529bbb8977c7
more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
diff
changeset
|
238 |
Markup.SORTING, Markup.TYPING, Markup.CLASS_PARAMETER, Markup.ML_TYPING, |
69650 | 239 |
Markup.ML_BREAKPOINT, Markup.PATH, Markup.DOC, Markup.URL, |
69648 | 240 |
Markup.MARKDOWN_PARAGRAPH, Markup.MARKDOWN_ITEM, Markup.Markdown_List.name) ++ |
67323
d02208cefbdb
PIDE markup for Markdown items (which may consist of multiple paragraphs or lists);
wenzelm
parents:
67322
diff
changeset
|
241 |
Markup.Elements(tooltip_descriptions.keySet) |
64622
529bbb8977c7
more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
diff
changeset
|
242 |
|
65129
06a7c2d316cf
more general tooltips, with uniform info range handling;
wenzelm
parents:
65126
diff
changeset
|
243 |
val tooltip_message_elements = |
06a7c2d316cf
more general tooltips, with uniform info range handling;
wenzelm
parents:
65126
diff
changeset
|
244 |
Markup.Elements(Markup.WRITELN, Markup.INFORMATION, Markup.WARNING, Markup.LEGACY, Markup.ERROR, |
06a7c2d316cf
more general tooltips, with uniform info range handling;
wenzelm
parents:
65126
diff
changeset
|
245 |
Markup.BAD) |
06a7c2d316cf
more general tooltips, with uniform info range handling;
wenzelm
parents:
65126
diff
changeset
|
246 |
|
72858
cb0c407fbc6e
added "isabelle log": print messages from build database;
wenzelm
parents:
72856
diff
changeset
|
247 |
val message_elements = Markup.Elements(message_pri.keySet) |
71499 | 248 |
val warning_elements = Markup.Elements(Markup.WARNING, Markup.LEGACY) |
71566
76b739c0bedd
backed out changeset 7eadccd4392c: too confusing wrt. text overview panel;
wenzelm
parents:
71555
diff
changeset
|
249 |
val error_elements = Markup.Elements(Markup.ERROR) |
71499 | 250 |
|
72901 | 251 |
val entity_elements = Markup.Elements(Markup.ENTITY) |
67132 | 252 |
|
253 |
val antiquoted_elements = Markup.Elements(Markup.ANTIQUOTED) |
|
67336 | 254 |
|
69900 | 255 |
val meta_data_elements = |
256 |
Markup.Elements(Markup.META_TITLE, Markup.META_CREATOR, Markup.META_CONTRIBUTOR, |
|
69916
3235ecdcd884
more meta data from "dcterms" (superset of "dc");
wenzelm
parents:
69900
diff
changeset
|
257 |
Markup.META_DATE, Markup.META_DESCRIPTION, Markup.META_LICENSE) |
69900 | 258 |
|
70135
ad6d4a14adb5
report document tags as seen in the text (not the active tag of Thy_Output.present_thy);
wenzelm
parents:
69970
diff
changeset
|
259 |
val document_tag_elements = |
ad6d4a14adb5
report document tags as seen in the text (not the active tag of Thy_Output.present_thy);
wenzelm
parents:
69970
diff
changeset
|
260 |
Markup.Elements(Markup.Document_Tag.ELEMENT) |
ad6d4a14adb5
report document tags as seen in the text (not the active tag of Thy_Output.present_thy);
wenzelm
parents:
69970
diff
changeset
|
261 |
|
67336 | 262 |
val markdown_elements = |
263 |
Markup.Elements(Markup.MARKDOWN_PARAGRAPH, Markup.MARKDOWN_ITEM, Markup.Markdown_List.name, |
|
264 |
Markup.Markdown_Bullet.name) |
|
64622
529bbb8977c7
more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
diff
changeset
|
265 |
} |
529bbb8977c7
more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
diff
changeset
|
266 |
|
72856 | 267 |
class Rendering( |
64622
529bbb8977c7
more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
diff
changeset
|
268 |
val snapshot: Document.Snapshot, |
529bbb8977c7
more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
diff
changeset
|
269 |
val options: Options, |
65213
51c0f094dc02
proper local debugger state, depending on session;
wenzelm
parents:
65190
diff
changeset
|
270 |
val session: Session) |
64622
529bbb8977c7
more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
diff
changeset
|
271 |
{ |
529bbb8977c7
more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
diff
changeset
|
272 |
override def toString: String = "Rendering(" + snapshot.toString + ")" |
529bbb8977c7
more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
diff
changeset
|
273 |
|
72856 | 274 |
def get_text(range: Text.Range): Option[String] = None |
66114 | 275 |
|
64622
529bbb8977c7
more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
diff
changeset
|
276 |
|
66117 | 277 |
/* caret */ |
278 |
||
279 |
def before_caret_range(caret: Text.Offset): Text.Range = |
|
280 |
{ |
|
281 |
val former_caret = snapshot.revert(caret) |
|
282 |
snapshot.convert(Text.Range(former_caret - 1, former_caret)) |
|
283 |
} |
|
284 |
||
285 |
||
64877 | 286 |
/* completion */ |
287 |
||
66054
fb0eea226a4d
more uniform syntax_completion + semantic_completion;
wenzelm
parents:
66053
diff
changeset
|
288 |
def semantic_completion(completed_range: Option[Text.Range], caret_range: Text.Range) |
64877 | 289 |
: Option[Text.Info[Completion.Semantic]] = |
290 |
if (snapshot.is_outdated) None |
|
291 |
else { |
|
66054
fb0eea226a4d
more uniform syntax_completion + semantic_completion;
wenzelm
parents:
66053
diff
changeset
|
292 |
snapshot.select(caret_range, Rendering.semantic_completion_elements, _ => |
64877 | 293 |
{ |
294 |
case Completion.Semantic.Info(info) => |
|
295 |
completed_range match { |
|
296 |
case Some(range0) if range0.contains(info.range) && range0 != info.range => None |
|
297 |
case _ => Some(info) |
|
298 |
} |
|
299 |
case _ => None |
|
300 |
}).headOption.map(_.info) |
|
301 |
} |
|
302 |
||
66054
fb0eea226a4d
more uniform syntax_completion + semantic_completion;
wenzelm
parents:
66053
diff
changeset
|
303 |
def semantic_completion_result( |
fb0eea226a4d
more uniform syntax_completion + semantic_completion;
wenzelm
parents:
66053
diff
changeset
|
304 |
history: Completion.History, |
66055 | 305 |
unicode: Boolean, |
66054
fb0eea226a4d
more uniform syntax_completion + semantic_completion;
wenzelm
parents:
66053
diff
changeset
|
306 |
completed_range: Option[Text.Range], |
66114 | 307 |
caret_range: Text.Range): (Boolean, Option[Completion.Result]) = |
66054
fb0eea226a4d
more uniform syntax_completion + semantic_completion;
wenzelm
parents:
66053
diff
changeset
|
308 |
{ |
fb0eea226a4d
more uniform syntax_completion + semantic_completion;
wenzelm
parents:
66053
diff
changeset
|
309 |
semantic_completion(completed_range, caret_range) match { |
fb0eea226a4d
more uniform syntax_completion + semantic_completion;
wenzelm
parents:
66053
diff
changeset
|
310 |
case Some(Text.Info(_, Completion.No_Completion)) => (true, None) |
fb0eea226a4d
more uniform syntax_completion + semantic_completion;
wenzelm
parents:
66053
diff
changeset
|
311 |
case Some(Text.Info(range, names: Completion.Names)) => |
72856 | 312 |
get_text(range) match { |
66055 | 313 |
case Some(original) => (false, names.complete(range, history, unicode, original)) |
66054
fb0eea226a4d
more uniform syntax_completion + semantic_completion;
wenzelm
parents:
66053
diff
changeset
|
314 |
case None => (false, None) |
fb0eea226a4d
more uniform syntax_completion + semantic_completion;
wenzelm
parents:
66053
diff
changeset
|
315 |
} |
fb0eea226a4d
more uniform syntax_completion + semantic_completion;
wenzelm
parents:
66053
diff
changeset
|
316 |
case None => (false, None) |
fb0eea226a4d
more uniform syntax_completion + semantic_completion;
wenzelm
parents:
66053
diff
changeset
|
317 |
} |
fb0eea226a4d
more uniform syntax_completion + semantic_completion;
wenzelm
parents:
66053
diff
changeset
|
318 |
} |
fb0eea226a4d
more uniform syntax_completion + semantic_completion;
wenzelm
parents:
66053
diff
changeset
|
319 |
|
66053 | 320 |
def language_context(range: Text.Range): Option[Completion.Language_Context] = |
321 |
snapshot.select(range, Rendering.language_context_elements, _ => |
|
322 |
{ |
|
323 |
case Text.Info(_, XML.Elem(Markup.Language(language, symbols, antiquotes, delimited), _)) => |
|
324 |
if (delimited) Some(Completion.Language_Context(language, symbols, antiquotes)) |
|
325 |
else None |
|
326 |
case Text.Info(_, elem) |
|
327 |
if elem.name == Markup.ML_STRING || elem.name == Markup.ML_COMMENT => |
|
328 |
Some(Completion.Language_Context.ML_inner) |
|
329 |
case Text.Info(_, _) => |
|
330 |
Some(Completion.Language_Context.inner) |
|
331 |
}).headOption.map(_.info) |
|
332 |
||
72729 | 333 |
def citations(range: Text.Range): List[Text.Info[String]] = |
66158 | 334 |
snapshot.select(range, Rendering.citation_elements, _ => |
335 |
{ |
|
336 |
case Text.Info(info_range, XML.Elem(Markup.Citation(name), _)) => |
|
337 |
Some(Text.Info(snapshot.convert(info_range), name)) |
|
338 |
case _ => None |
|
72729 | 339 |
}).map(_.info) |
66158 | 340 |
|
341 |
||
342 |
/* file-system path completion */ |
|
343 |
||
72842
6aae62f55c2b
clarified markup: support more completion, e.g. within ROOTS;
wenzelm
parents:
72729
diff
changeset
|
344 |
def language_path(range: Text.Range): Option[Text.Info[Boolean]] = |
66053 | 345 |
snapshot.select(range, Rendering.language_elements, _ => |
346 |
{ |
|
72842
6aae62f55c2b
clarified markup: support more completion, e.g. within ROOTS;
wenzelm
parents:
72729
diff
changeset
|
347 |
case Text.Info(info_range, XML.Elem(Markup.Language.Path(delimited), _)) => |
6aae62f55c2b
clarified markup: support more completion, e.g. within ROOTS;
wenzelm
parents:
72729
diff
changeset
|
348 |
Some((delimited, snapshot.convert(info_range))) |
66053 | 349 |
case _ => None |
72842
6aae62f55c2b
clarified markup: support more completion, e.g. within ROOTS;
wenzelm
parents:
72729
diff
changeset
|
350 |
}).headOption.map({ case Text.Info(_, (delimited, range)) => Text.Info(range, delimited) }) |
66053 | 351 |
|
66158 | 352 |
def path_completion(caret: Text.Offset): Option[Completion.Result] = |
353 |
{ |
|
354 |
def complete(text: String): List[(String, List[String])] = |
|
355 |
{ |
|
356 |
try { |
|
357 |
val path = Path.explode(text) |
|
358 |
val (dir, base_name) = |
|
359 |
if (text == "" || text.endsWith("/")) (path, "") |
|
69366 | 360 |
else (path.dir, path.file_name) |
66158 | 361 |
|
362 |
val directory = new JFile(session.resources.append(snapshot.node_name, dir)) |
|
363 |
val files = directory.listFiles |
|
364 |
if (files == null) Nil |
|
365 |
else { |
|
366 |
val ignore = |
|
66923 | 367 |
space_explode(':', options.string("completion_path_ignore")). |
66158 | 368 |
map(s => FileSystems.getDefault.getPathMatcher("glob:" + s)) |
369 |
(for { |
|
370 |
file <- files.iterator |
|
371 |
||
372 |
name = file.getName |
|
373 |
if name.startsWith(base_name) |
|
374 |
path_name = new JFile(name).toPath |
|
375 |
if !ignore.exists(matcher => matcher.matches(path_name)) |
|
376 |
||
377 |
text1 = (dir + Path.basic(name)).implode_short |
|
378 |
if text != text1 |
|
379 |
||
380 |
is_dir = new JFile(directory, name).isDirectory |
|
381 |
replacement = text1 + (if (is_dir) "/" else "") |
|
382 |
descr = List(text1, if (is_dir) "(directory)" else "(file)") |
|
383 |
} yield (replacement, descr)).take(options.int("completion_limit")).toList |
|
384 |
} |
|
385 |
} |
|
386 |
catch { case ERROR(_) => Nil } |
|
387 |
} |
|
388 |
||
389 |
def is_wrapped(s: String): Boolean = |
|
390 |
s.startsWith("\"") && s.endsWith("\"") || |
|
391 |
s.startsWith(Symbol.open_decoded) && s.endsWith(Symbol.close_decoded) |
|
392 |
||
393 |
for { |
|
72842
6aae62f55c2b
clarified markup: support more completion, e.g. within ROOTS;
wenzelm
parents:
72729
diff
changeset
|
394 |
Text.Info(r1, delimited) <- language_path(before_caret_range(caret)) |
72856 | 395 |
s1 <- get_text(r1) |
72842
6aae62f55c2b
clarified markup: support more completion, e.g. within ROOTS;
wenzelm
parents:
72729
diff
changeset
|
396 |
(r2, s2) <- |
6aae62f55c2b
clarified markup: support more completion, e.g. within ROOTS;
wenzelm
parents:
72729
diff
changeset
|
397 |
if (is_wrapped(s1)) { |
6aae62f55c2b
clarified markup: support more completion, e.g. within ROOTS;
wenzelm
parents:
72729
diff
changeset
|
398 |
Some((Text.Range(r1.start + 1, r1.stop - 1), s1.substring(1, s1.length - 1))) |
6aae62f55c2b
clarified markup: support more completion, e.g. within ROOTS;
wenzelm
parents:
72729
diff
changeset
|
399 |
} |
6aae62f55c2b
clarified markup: support more completion, e.g. within ROOTS;
wenzelm
parents:
72729
diff
changeset
|
400 |
else if (delimited) Some((r1, s1)) |
6aae62f55c2b
clarified markup: support more completion, e.g. within ROOTS;
wenzelm
parents:
72729
diff
changeset
|
401 |
else None |
66158 | 402 |
if Path.is_valid(s2) |
403 |
paths = complete(s2) |
|
404 |
if paths.nonEmpty |
|
405 |
items = paths.map(p => Completion.Item(r2, s2, "", p._2, p._1, 0, false)) |
|
406 |
} yield Completion.Result(r2, s2, false, items) |
|
407 |
} |
|
66053 | 408 |
|
64877 | 409 |
|
65139 | 410 |
/* spell checker */ |
411 |
||
67395
b39d596b77ce
more accurate spell-checking for nested quotations / antiquotations, notably in formal comments;
wenzelm
parents:
67336
diff
changeset
|
412 |
private lazy val spell_checker_include = |
b39d596b77ce
more accurate spell-checking for nested quotations / antiquotations, notably in formal comments;
wenzelm
parents:
67336
diff
changeset
|
413 |
Markup.Elements(space_explode(',', options.string("spell_checker_include")): _*) |
b39d596b77ce
more accurate spell-checking for nested quotations / antiquotations, notably in formal comments;
wenzelm
parents:
67336
diff
changeset
|
414 |
|
65139 | 415 |
private lazy val spell_checker_elements = |
67395
b39d596b77ce
more accurate spell-checking for nested quotations / antiquotations, notably in formal comments;
wenzelm
parents:
67336
diff
changeset
|
416 |
spell_checker_include ++ |
b39d596b77ce
more accurate spell-checking for nested quotations / antiquotations, notably in formal comments;
wenzelm
parents:
67336
diff
changeset
|
417 |
Markup.Elements(space_explode(',', options.string("spell_checker_exclude")): _*) |
65139 | 418 |
|
67395
b39d596b77ce
more accurate spell-checking for nested quotations / antiquotations, notably in formal comments;
wenzelm
parents:
67336
diff
changeset
|
419 |
def spell_checker(range: Text.Range): List[Text.Info[Text.Range]] = |
b39d596b77ce
more accurate spell-checking for nested quotations / antiquotations, notably in formal comments;
wenzelm
parents:
67336
diff
changeset
|
420 |
{ |
b39d596b77ce
more accurate spell-checking for nested quotations / antiquotations, notably in formal comments;
wenzelm
parents:
67336
diff
changeset
|
421 |
val result = |
b39d596b77ce
more accurate spell-checking for nested quotations / antiquotations, notably in formal comments;
wenzelm
parents:
67336
diff
changeset
|
422 |
snapshot.select(range, spell_checker_elements, _ => |
b39d596b77ce
more accurate spell-checking for nested quotations / antiquotations, notably in formal comments;
wenzelm
parents:
67336
diff
changeset
|
423 |
{ |
b39d596b77ce
more accurate spell-checking for nested quotations / antiquotations, notably in formal comments;
wenzelm
parents:
67336
diff
changeset
|
424 |
case info => |
b39d596b77ce
more accurate spell-checking for nested quotations / antiquotations, notably in formal comments;
wenzelm
parents:
67336
diff
changeset
|
425 |
Some( |
b39d596b77ce
more accurate spell-checking for nested quotations / antiquotations, notably in formal comments;
wenzelm
parents:
67336
diff
changeset
|
426 |
if (spell_checker_include(info.info.name)) |
b39d596b77ce
more accurate spell-checking for nested quotations / antiquotations, notably in formal comments;
wenzelm
parents:
67336
diff
changeset
|
427 |
Some(snapshot.convert(info.range)) |
b39d596b77ce
more accurate spell-checking for nested quotations / antiquotations, notably in formal comments;
wenzelm
parents:
67336
diff
changeset
|
428 |
else None) |
b39d596b77ce
more accurate spell-checking for nested quotations / antiquotations, notably in formal comments;
wenzelm
parents:
67336
diff
changeset
|
429 |
}) |
b39d596b77ce
more accurate spell-checking for nested quotations / antiquotations, notably in formal comments;
wenzelm
parents:
67336
diff
changeset
|
430 |
for (Text.Info(range, Some(range1)) <- result) |
b39d596b77ce
more accurate spell-checking for nested quotations / antiquotations, notably in formal comments;
wenzelm
parents:
67336
diff
changeset
|
431 |
yield Text.Info(range, range1) |
b39d596b77ce
more accurate spell-checking for nested quotations / antiquotations, notably in formal comments;
wenzelm
parents:
67336
diff
changeset
|
432 |
} |
65139 | 433 |
|
434 |
def spell_checker_point(range: Text.Range): Option[Text.Range] = |
|
67395
b39d596b77ce
more accurate spell-checking for nested quotations / antiquotations, notably in formal comments;
wenzelm
parents:
67336
diff
changeset
|
435 |
spell_checker(range).headOption.map(_.info) |
65139 | 436 |
|
437 |
||
65101 | 438 |
/* text background */ |
439 |
||
72900 | 440 |
def background(elements: Markup.Elements, range: Text.Range, focus: Rendering.Focus) |
65176 | 441 |
: List[Text.Info[Rendering.Color.Value]] = |
65101 | 442 |
{ |
443 |
for { |
|
444 |
Text.Info(r, result) <- |
|
445 |
snapshot.cumulate[(List[Markup], Option[Rendering.Color.Value])]( |
|
72906 | 446 |
range, (List(Markup.Empty), None), elements, |
65101 | 447 |
command_states => |
448 |
{ |
|
72925 | 449 |
case ((markups, color), Text.Info(_, XML.Elem(markup, _))) |
68758 | 450 |
if markups.nonEmpty && Document_Status.Command_Status.proper_elements(markup.name) => |
65101 | 451 |
Some((markup :: markups, color)) |
452 |
case (_, Text.Info(_, XML.Elem(Markup(Markup.BAD, _), _))) => |
|
453 |
Some((Nil, Some(Rendering.Color.bad))) |
|
454 |
case (_, Text.Info(_, XML.Elem(Markup(Markup.INTENSIFY, _), _))) => |
|
455 |
Some((Nil, Some(Rendering.Color.intensify))) |
|
72929 | 456 |
case (_, Text.Info(_, XML.Elem(Markup.Entity.Occ(i), _))) if focus(i) => |
72903 | 457 |
Some((Nil, Some(Rendering.Color.entity))) |
67322 | 458 |
case (_, Text.Info(_, XML.Elem(Markup.Markdown_Bullet(depth), _))) => |
65101 | 459 |
val color = |
65150 | 460 |
depth % 4 match { |
67322 | 461 |
case 1 => Rendering.Color.markdown_bullet1 |
462 |
case 2 => Rendering.Color.markdown_bullet2 |
|
463 |
case 3 => Rendering.Color.markdown_bullet3 |
|
464 |
case _ => Rendering.Color.markdown_bullet4 |
|
65101 | 465 |
} |
466 |
Some((Nil, Some(color))) |
|
72907 | 467 |
case (_, Text.Info(_, Protocol.Dialog(_, serial, result))) => |
65101 | 468 |
command_states.collectFirst( |
469 |
{ case st if st.results.defined(serial) => st.results.get(serial).get }) match |
|
470 |
{ |
|
471 |
case Some(Protocol.Dialog_Result(res)) if res == result => |
|
472 |
Some((Nil, Some(Rendering.Color.active_result))) |
|
473 |
case _ => |
|
474 |
Some((Nil, Some(Rendering.Color.active))) |
|
475 |
} |
|
476 |
case (_, Text.Info(_, elem)) => |
|
477 |
if (Rendering.active_elements(elem.name)) |
|
478 |
Some((Nil, Some(Rendering.Color.active))) |
|
479 |
else None |
|
480 |
}) |
|
481 |
color <- |
|
72925 | 482 |
result match { |
65101 | 483 |
case (markups, opt_color) if markups.nonEmpty => |
68758 | 484 |
val status = Document_Status.Command_Status.make(markups.iterator) |
65101 | 485 |
if (status.is_unprocessed) Some(Rendering.Color.unprocessed1) |
486 |
else if (status.is_running) Some(Rendering.Color.running1) |
|
68871
f5c76072db55
more explicit status for "canceled" command within theory node;
wenzelm
parents:
68822
diff
changeset
|
487 |
else if (status.is_canceled) Some(Rendering.Color.canceled) |
65101 | 488 |
else opt_color |
489 |
case (_, opt_color) => opt_color |
|
72925 | 490 |
} |
65101 | 491 |
} yield Text.Info(r, color) |
492 |
} |
|
493 |
||
494 |
||
495 |
/* text foreground */ |
|
496 |
||
497 |
def foreground(range: Text.Range): List[Text.Info[Rendering.Color.Value]] = |
|
498 |
snapshot.select(range, Rendering.foreground_elements, _ => |
|
499 |
{ |
|
66074 | 500 |
case info => Some(Rendering.foreground(info.info.name)) |
65101 | 501 |
}) |
502 |
||
503 |
||
72904 | 504 |
/* entity focus */ |
64767 | 505 |
|
72904 | 506 |
def entity_focus_defs(range: Text.Range): Rendering.Focus = |
72905 | 507 |
Rendering.Focus.make( |
508 |
snapshot.cumulate(range, Rendering.Focus.empty, Rendering.entity_elements, _ => |
|
72904 | 509 |
{ |
510 |
case (focus, Text.Info(_, XML.Elem(Markup.Entity.Def(i), _))) => Some(focus + i) |
|
511 |
case _ => None |
|
72905 | 512 |
})) |
72904 | 513 |
|
72927
69f768aff611
clarified caret focus modifier, depending on option "jedit_focus_modifier";
wenzelm
parents:
72926
diff
changeset
|
514 |
def entity_focus(range: Text.Range, defs_focus: Rendering.Focus): Rendering.Focus = |
72905 | 515 |
Rendering.Focus.make( |
516 |
snapshot.cumulate(range, Rendering.Focus.empty, Rendering.entity_elements, _ => |
|
72904 | 517 |
{ |
518 |
case (focus, Text.Info(_, XML.Elem(Markup.Entity.Ref(i), _))) |
|
72927
69f768aff611
clarified caret focus modifier, depending on option "jedit_focus_modifier";
wenzelm
parents:
72926
diff
changeset
|
519 |
if defs_focus(i) => Some(focus + i) |
72904 | 520 |
case _ => None |
72905 | 521 |
})) |
72904 | 522 |
|
523 |
||
524 |
/* caret focus */ |
|
64767 | 525 |
|
72927
69f768aff611
clarified caret focus modifier, depending on option "jedit_focus_modifier";
wenzelm
parents:
72926
diff
changeset
|
526 |
def caret_focus(caret_range: Text.Range, defs_range: Text.Range): Rendering.Focus = |
64767 | 527 |
{ |
72904 | 528 |
val focus = entity_focus_defs(caret_range) |
529 |
if (focus.defined) focus |
|
72927
69f768aff611
clarified caret focus modifier, depending on option "jedit_focus_modifier";
wenzelm
parents:
72926
diff
changeset
|
530 |
else if (defs_range == Text.Range.offside) Rendering.Focus.empty |
69f768aff611
clarified caret focus modifier, depending on option "jedit_focus_modifier";
wenzelm
parents:
72926
diff
changeset
|
531 |
else { |
69f768aff611
clarified caret focus modifier, depending on option "jedit_focus_modifier";
wenzelm
parents:
72926
diff
changeset
|
532 |
val defs_focus = |
69f768aff611
clarified caret focus modifier, depending on option "jedit_focus_modifier";
wenzelm
parents:
72926
diff
changeset
|
533 |
if (defs_range == Text.Range.full) Rendering.Focus.full |
69f768aff611
clarified caret focus modifier, depending on option "jedit_focus_modifier";
wenzelm
parents:
72926
diff
changeset
|
534 |
else entity_focus_defs(defs_range) |
69f768aff611
clarified caret focus modifier, depending on option "jedit_focus_modifier";
wenzelm
parents:
72926
diff
changeset
|
535 |
entity_focus(caret_range, defs_focus) |
69f768aff611
clarified caret focus modifier, depending on option "jedit_focus_modifier";
wenzelm
parents:
72926
diff
changeset
|
536 |
} |
64767 | 537 |
} |
538 |
||
72927
69f768aff611
clarified caret focus modifier, depending on option "jedit_focus_modifier";
wenzelm
parents:
72926
diff
changeset
|
539 |
def caret_focus_ranges(caret_range: Text.Range, defs_range: Text.Range): List[Text.Range] = |
64767 | 540 |
{ |
72927
69f768aff611
clarified caret focus modifier, depending on option "jedit_focus_modifier";
wenzelm
parents:
72926
diff
changeset
|
541 |
val focus = caret_focus(caret_range, defs_range) |
72926 | 542 |
if (focus.defined) { |
72927
69f768aff611
clarified caret focus modifier, depending on option "jedit_focus_modifier";
wenzelm
parents:
72926
diff
changeset
|
543 |
snapshot.cumulate[Boolean](defs_range, false, Rendering.entity_elements, _ => |
72904 | 544 |
{ |
72929 | 545 |
case (_, Text.Info(_, XML.Elem(Markup.Entity.Occ(i), _))) if focus(i) => Some(true) |
72904 | 546 |
case _ => None |
547 |
}).flatMap(info => if (info.info) Some(info.range) else None) |
|
64767 | 548 |
} |
549 |
else Nil |
|
550 |
} |
|
65121 | 551 |
|
552 |
||
72858
cb0c407fbc6e
added "isabelle log": print messages from build database;
wenzelm
parents:
72856
diff
changeset
|
553 |
/* messages */ |
65121 | 554 |
|
65129
06a7c2d316cf
more general tooltips, with uniform info range handling;
wenzelm
parents:
65126
diff
changeset
|
555 |
def message_underline_color(elements: Markup.Elements, range: Text.Range) |
06a7c2d316cf
more general tooltips, with uniform info range handling;
wenzelm
parents:
65126
diff
changeset
|
556 |
: List[Text.Info[Rendering.Color.Value]] = |
65121 | 557 |
{ |
558 |
val results = |
|
559 |
snapshot.cumulate[Int](range, 0, elements, _ => |
|
560 |
{ |
|
561 |
case (pri, Text.Info(_, elem)) => Some(pri max Rendering.message_pri(elem.name)) |
|
562 |
}) |
|
563 |
for { |
|
564 |
Text.Info(r, pri) <- results |
|
565 |
color <- Rendering.message_underline_color.get(pri) |
|
566 |
} yield Text.Info(r, color) |
|
567 |
} |
|
65149 | 568 |
|
72869 | 569 |
def text_messages(range: Text.Range): List[Text.Info[XML.Elem]] = |
72858
cb0c407fbc6e
added "isabelle log": print messages from build database;
wenzelm
parents:
72856
diff
changeset
|
570 |
{ |
cb0c407fbc6e
added "isabelle log": print messages from build database;
wenzelm
parents:
72856
diff
changeset
|
571 |
val results = |
72872 | 572 |
snapshot.cumulate[Vector[Command.Results.Entry]]( |
573 |
range, Vector.empty, Rendering.message_elements, command_states => |
|
72858
cb0c407fbc6e
added "isabelle log": print messages from build database;
wenzelm
parents:
72856
diff
changeset
|
574 |
{ |
cb0c407fbc6e
added "isabelle log": print messages from build database;
wenzelm
parents:
72856
diff
changeset
|
575 |
case (res, Text.Info(_, elem)) => |
72872 | 576 |
Command.State.get_result_proper(command_states, elem.markup.properties) |
577 |
.map(res :+ _) |
|
72858
cb0c407fbc6e
added "isabelle log": print messages from build database;
wenzelm
parents:
72856
diff
changeset
|
578 |
case _ => None |
cb0c407fbc6e
added "isabelle log": print messages from build database;
wenzelm
parents:
72856
diff
changeset
|
579 |
}) |
cb0c407fbc6e
added "isabelle log": print messages from build database;
wenzelm
parents:
72856
diff
changeset
|
580 |
|
cb0c407fbc6e
added "isabelle log": print messages from build database;
wenzelm
parents:
72856
diff
changeset
|
581 |
var seen_serials = Set.empty[Long] |
72872 | 582 |
def seen(i: Long): Boolean = |
583 |
{ |
|
584 |
val b = seen_serials(i) |
|
585 |
seen_serials += i |
|
586 |
b |
|
587 |
} |
|
72858
cb0c407fbc6e
added "isabelle log": print messages from build database;
wenzelm
parents:
72856
diff
changeset
|
588 |
for { |
72872 | 589 |
Text.Info(range, entries) <- results |
590 |
(i, elem) <- entries if !seen(i) |
|
72869 | 591 |
} yield Text.Info(range, elem) |
72858
cb0c407fbc6e
added "isabelle log": print messages from build database;
wenzelm
parents:
72856
diff
changeset
|
592 |
} |
cb0c407fbc6e
added "isabelle log": print messages from build database;
wenzelm
parents:
72856
diff
changeset
|
593 |
|
65149 | 594 |
|
595 |
/* tooltips */ |
|
596 |
||
69899 | 597 |
def timing_threshold: Double = 0.0 |
65149 | 598 |
|
599 |
private sealed case class Tooltip_Info( |
|
600 |
range: Text.Range, |
|
601 |
timing: Timing = Timing.zero, |
|
72869 | 602 |
messages: List[(Long, XML.Tree)] = Nil, |
65149 | 603 |
rev_infos: List[(Boolean, XML.Tree)] = Nil) |
604 |
{ |
|
605 |
def + (t: Timing): Tooltip_Info = copy(timing = timing + t) |
|
606 |
def + (r0: Text.Range, serial: Long, tree: XML.Tree): Tooltip_Info = |
|
607 |
{ |
|
608 |
val r = snapshot.convert(r0) |
|
609 |
if (range == r) copy(messages = (serial -> tree) :: messages) |
|
610 |
else copy(range = r, messages = List(serial -> tree)) |
|
611 |
} |
|
612 |
def + (r0: Text.Range, important: Boolean, tree: XML.Tree): Tooltip_Info = |
|
613 |
{ |
|
614 |
val r = snapshot.convert(r0) |
|
615 |
if (range == r) copy(rev_infos = (important -> tree) :: rev_infos) |
|
616 |
else copy (range = r, rev_infos = List(important -> tree)) |
|
617 |
} |
|
67933
604da273e18d
more robust timing info: do not rely on order of markup;
wenzelm
parents:
67824
diff
changeset
|
618 |
|
604da273e18d
more robust timing info: do not rely on order of markup;
wenzelm
parents:
67824
diff
changeset
|
619 |
def timing_info(tree: XML.Tree): Option[XML.Tree] = |
604da273e18d
more robust timing info: do not rely on order of markup;
wenzelm
parents:
67824
diff
changeset
|
620 |
tree match { |
604da273e18d
more robust timing info: do not rely on order of markup;
wenzelm
parents:
67824
diff
changeset
|
621 |
case XML.Elem(Markup(Markup.TIMING, _), _) => |
604da273e18d
more robust timing info: do not rely on order of markup;
wenzelm
parents:
67824
diff
changeset
|
622 |
if (timing.elapsed.seconds >= timing_threshold) Some(XML.Text(timing.message)) else None |
604da273e18d
more robust timing info: do not rely on order of markup;
wenzelm
parents:
67824
diff
changeset
|
623 |
case _ => Some(tree) |
604da273e18d
more robust timing info: do not rely on order of markup;
wenzelm
parents:
67824
diff
changeset
|
624 |
} |
65149 | 625 |
def infos(important: Boolean): List[XML.Tree] = |
67933
604da273e18d
more robust timing info: do not rely on order of markup;
wenzelm
parents:
67824
diff
changeset
|
626 |
for { |
604da273e18d
more robust timing info: do not rely on order of markup;
wenzelm
parents:
67824
diff
changeset
|
627 |
(is_important, tree) <- rev_infos.reverse if is_important == important |
604da273e18d
more robust timing info: do not rely on order of markup;
wenzelm
parents:
67824
diff
changeset
|
628 |
tree1 <- timing_info(tree) |
604da273e18d
more robust timing info: do not rely on order of markup;
wenzelm
parents:
67824
diff
changeset
|
629 |
} yield tree1 |
65149 | 630 |
} |
631 |
||
65488 | 632 |
def perhaps_append_file(node_name: Document.Node.Name, name: String): String = |
633 |
if (Path.is_valid(name)) session.resources.append(node_name, Path.explode(name)) else name |
|
65487 | 634 |
|
65149 | 635 |
def tooltips(elements: Markup.Elements, range: Text.Range): Option[Text.Info[List[XML.Tree]]] = |
636 |
{ |
|
637 |
val results = |
|
67824
661cd25304ae
more compact markup tree: output messages are already stored in command results (e.g. relevant for XML data representation);
wenzelm
parents:
67395
diff
changeset
|
638 |
snapshot.cumulate[Tooltip_Info](range, Tooltip_Info(range), elements, command_states => |
65149 | 639 |
{ |
640 |
case (info, Text.Info(_, XML.Elem(Markup.Timing(t), _))) => Some(info + t) |
|
641 |
||
67824
661cd25304ae
more compact markup tree: output messages are already stored in command results (e.g. relevant for XML data representation);
wenzelm
parents:
67395
diff
changeset
|
642 |
case (info, Text.Info(r0, msg @ XML.Elem(Markup(Markup.BAD, Markup.Serial(i)), body))) |
661cd25304ae
more compact markup tree: output messages are already stored in command results (e.g. relevant for XML data representation);
wenzelm
parents:
67395
diff
changeset
|
643 |
if body.nonEmpty => Some(info + (r0, i, msg)) |
661cd25304ae
more compact markup tree: output messages are already stored in command results (e.g. relevant for XML data representation);
wenzelm
parents:
67395
diff
changeset
|
644 |
|
661cd25304ae
more compact markup tree: output messages are already stored in command results (e.g. relevant for XML data representation);
wenzelm
parents:
67395
diff
changeset
|
645 |
case (info, Text.Info(r0, XML.Elem(Markup(name, props), _))) |
661cd25304ae
more compact markup tree: output messages are already stored in command results (e.g. relevant for XML data representation);
wenzelm
parents:
67395
diff
changeset
|
646 |
if Rendering.tooltip_message_elements(name) => |
661cd25304ae
more compact markup tree: output messages are already stored in command results (e.g. relevant for XML data representation);
wenzelm
parents:
67395
diff
changeset
|
647 |
for ((i, tree) <- Command.State.get_result_proper(command_states, props)) |
661cd25304ae
more compact markup tree: output messages are already stored in command results (e.g. relevant for XML data representation);
wenzelm
parents:
67395
diff
changeset
|
648 |
yield (info + (r0, i, tree)) |
65149 | 649 |
|
650 |
case (info, Text.Info(r0, XML.Elem(Markup.Entity(kind, name), _))) |
|
651 |
if kind != "" && kind != Markup.ML_DEF => |
|
652 |
val kind1 = Word.implode(Word.explode('_', kind)) |
|
653 |
val txt1 = |
|
654 |
if (name == "") kind1 |
|
655 |
else if (kind1 == "") quote(name) |
|
656 |
else kind1 + " " + quote(name) |
|
67933
604da273e18d
more robust timing info: do not rely on order of markup;
wenzelm
parents:
67824
diff
changeset
|
657 |
val info1 = info + (r0, true, XML.Text(txt1)) |
604da273e18d
more robust timing info: do not rely on order of markup;
wenzelm
parents:
67824
diff
changeset
|
658 |
Some(if (kind == Markup.COMMAND) info1 + (r0, true, XML.elem(Markup.TIMING)) else info1) |
65149 | 659 |
|
660 |
case (info, Text.Info(r0, XML.Elem(Markup.Path(name), _))) => |
|
65488 | 661 |
val file = perhaps_append_file(snapshot.node_name, name) |
65149 | 662 |
val text = |
663 |
if (name == file) "file " + quote(file) |
|
664 |
else "path " + quote(name) + "\nfile " + quote(file) |
|
665 |
Some(info + (r0, true, XML.Text(text))) |
|
666 |
||
667 |
case (info, Text.Info(r0, XML.Elem(Markup.Doc(name), _))) => |
|
668 |
val text = "doc " + quote(name) |
|
669 |
Some(info + (r0, true, XML.Text(text))) |
|
670 |
||
671 |
case (info, Text.Info(r0, XML.Elem(Markup.Url(name), _))) => |
|
672 |
Some(info + (r0, true, XML.Text("URL " + quote(name)))) |
|
673 |
||
674 |
case (info, Text.Info(r0, XML.Elem(Markup(name, _), body))) |
|
675 |
if name == Markup.SORTING || name == Markup.TYPING => |
|
676 |
Some(info + (r0, true, Pretty.block(XML.Text("::") :: Pretty.brk(1) :: body))) |
|
677 |
||
678 |
case (info, Text.Info(r0, XML.Elem(Markup(Markup.CLASS_PARAMETER, _), body))) => |
|
679 |
Some(info + (r0, true, Pretty.block(0, body))) |
|
680 |
||
681 |
case (info, Text.Info(r0, XML.Elem(Markup(Markup.ML_TYPING, _), body))) => |
|
682 |
Some(info + (r0, false, Pretty.block(XML.Text("ML:") :: Pretty.brk(1) :: body))) |
|
683 |
||
684 |
case (info, Text.Info(r0, Protocol.ML_Breakpoint(breakpoint))) => |
|
65222
fb8253564483
more robust debugger initialization, e.g. required for GUI components before actual session startup;
wenzelm
parents:
65213
diff
changeset
|
685 |
val text = |
fb8253564483
more robust debugger initialization, e.g. required for GUI components before actual session startup;
wenzelm
parents:
65213
diff
changeset
|
686 |
if (session.debugger.breakpoint_state(breakpoint)) "breakpoint (enabled)" |
fb8253564483
more robust debugger initialization, e.g. required for GUI components before actual session startup;
wenzelm
parents:
65213
diff
changeset
|
687 |
else "breakpoint (disabled)" |
fb8253564483
more robust debugger initialization, e.g. required for GUI components before actual session startup;
wenzelm
parents:
65213
diff
changeset
|
688 |
Some(info + (r0, true, XML.Text(text))) |
65149 | 689 |
case (info, Text.Info(r0, XML.Elem(Markup.Language(language, _, _, _), _))) => |
690 |
val lang = Word.implode(Word.explode('_', language)) |
|
691 |
Some(info + (r0, true, XML.Text("language: " + lang))) |
|
692 |
||
693 |
case (info, Text.Info(r0, XML.Elem(Markup.Expression(kind), _))) => |
|
694 |
val descr = if (kind == "") "expression" else "expression: " + kind |
|
695 |
Some(info + (r0, true, XML.Text(descr))) |
|
696 |
||
697 |
case (info, Text.Info(r0, XML.Elem(Markup(Markup.MARKDOWN_PARAGRAPH, _), _))) => |
|
698 |
Some(info + (r0, true, XML.Text("Markdown: paragraph"))) |
|
67323
d02208cefbdb
PIDE markup for Markdown items (which may consist of multiple paragraphs or lists);
wenzelm
parents:
67322
diff
changeset
|
699 |
case (info, Text.Info(r0, XML.Elem(Markup(Markup.MARKDOWN_ITEM, _), _))) => |
d02208cefbdb
PIDE markup for Markdown items (which may consist of multiple paragraphs or lists);
wenzelm
parents:
67322
diff
changeset
|
700 |
Some(info + (r0, true, XML.Text("Markdown: item"))) |
65149 | 701 |
case (info, Text.Info(r0, XML.Elem(Markup.Markdown_List(kind), _))) => |
702 |
Some(info + (r0, true, XML.Text("Markdown: " + kind))) |
|
703 |
||
704 |
case (info, Text.Info(r0, XML.Elem(Markup(name, _), _))) => |
|
705 |
Rendering.tooltip_descriptions.get(name).map(desc => info + (r0, true, XML.Text(desc))) |
|
706 |
}).map(_.info) |
|
707 |
||
708 |
if (results.isEmpty) None |
|
709 |
else { |
|
710 |
val r = Text.Range(results.head.range.start, results.last.range.stop) |
|
711 |
val all_tips = |
|
72869 | 712 |
(SortedMap.empty[Long, XML.Tree] /: results.flatMap(_.messages))(_ + _) |
713 |
.iterator.map(_._2).toList ::: |
|
65149 | 714 |
results.flatMap(res => res.infos(true)) ::: |
715 |
results.flatMap(res => res.infos(false)).lastOption.toList |
|
716 |
if (all_tips.isEmpty) None else Some(Text.Info(r, all_tips)) |
|
717 |
} |
|
718 |
} |
|
65911 | 719 |
|
720 |
||
71499 | 721 |
/* messages */ |
722 |
||
723 |
def warnings(range: Text.Range): List[Text.Markup] = |
|
724 |
snapshot.select(range, Rendering.warning_elements, _ => Some(_)).map(_.info) |
|
725 |
||
726 |
def errors(range: Text.Range): List[Text.Markup] = |
|
727 |
snapshot.select(range, Rendering.error_elements, _ => Some(_)).map(_.info) |
|
728 |
||
729 |
||
65911 | 730 |
/* command status overview */ |
731 |
||
732 |
def overview_color(range: Text.Range): Option[Rendering.Color.Value] = |
|
733 |
{ |
|
734 |
if (snapshot.is_outdated) None |
|
735 |
else { |
|
736 |
val results = |
|
68758 | 737 |
snapshot.cumulate[List[Markup]](range, Nil, Document_Status.Command_Status.liberal_elements, |
738 |
_ => |
|
739 |
{ |
|
740 |
case (status, Text.Info(_, elem)) => Some(elem.markup :: status) |
|
741 |
}, status = true) |
|
65911 | 742 |
if (results.isEmpty) None |
743 |
else { |
|
68758 | 744 |
val status = Document_Status.Command_Status.make(results.iterator.flatMap(_.info)) |
65911 | 745 |
|
746 |
if (status.is_running) Some(Rendering.Color.running) |
|
747 |
else if (status.is_failed) Some(Rendering.Color.error) |
|
748 |
else if (status.is_warned) Some(Rendering.Color.warning) |
|
749 |
else if (status.is_unprocessed) Some(Rendering.Color.unprocessed) |
|
750 |
else None |
|
751 |
} |
|
752 |
} |
|
753 |
} |
|
67132 | 754 |
|
755 |
||
756 |
/* antiquoted text */ |
|
757 |
||
758 |
def antiquoted(range: Text.Range): Option[Text.Range] = |
|
759 |
snapshot.cumulate[Option[Text.Range]](range, None, Rendering.antiquoted_elements, _ => |
|
760 |
{ |
|
761 |
case (res, info) => if (res.isEmpty) Some(Some(info.range)) else None |
|
762 |
}).headOption.flatMap(_.info) |
|
69900 | 763 |
|
764 |
||
765 |
/* meta data */ |
|
766 |
||
767 |
def meta_data(range: Text.Range): Properties.T = |
|
768 |
{ |
|
769 |
val results = |
|
770 |
snapshot.cumulate[Properties.T](range, Nil, Rendering.meta_data_elements, _ => |
|
771 |
{ |
|
772 |
case (res, Text.Info(_, elem)) => |
|
773 |
val plain_text = XML.content(elem) |
|
774 |
Some((elem.name -> plain_text) :: res) |
|
775 |
}) |
|
776 |
Library.distinct(results.flatMap(_.info.reverse)) |
|
777 |
} |
|
70135
ad6d4a14adb5
report document tags as seen in the text (not the active tag of Thy_Output.present_thy);
wenzelm
parents:
69970
diff
changeset
|
778 |
|
ad6d4a14adb5
report document tags as seen in the text (not the active tag of Thy_Output.present_thy);
wenzelm
parents:
69970
diff
changeset
|
779 |
|
ad6d4a14adb5
report document tags as seen in the text (not the active tag of Thy_Output.present_thy);
wenzelm
parents:
69970
diff
changeset
|
780 |
/* document tags */ |
ad6d4a14adb5
report document tags as seen in the text (not the active tag of Thy_Output.present_thy);
wenzelm
parents:
69970
diff
changeset
|
781 |
|
ad6d4a14adb5
report document tags as seen in the text (not the active tag of Thy_Output.present_thy);
wenzelm
parents:
69970
diff
changeset
|
782 |
def document_tags(range: Text.Range): List[String] = |
ad6d4a14adb5
report document tags as seen in the text (not the active tag of Thy_Output.present_thy);
wenzelm
parents:
69970
diff
changeset
|
783 |
{ |
ad6d4a14adb5
report document tags as seen in the text (not the active tag of Thy_Output.present_thy);
wenzelm
parents:
69970
diff
changeset
|
784 |
val results = |
ad6d4a14adb5
report document tags as seen in the text (not the active tag of Thy_Output.present_thy);
wenzelm
parents:
69970
diff
changeset
|
785 |
snapshot.cumulate[List[String]](range, Nil, Rendering.document_tag_elements, _ => |
ad6d4a14adb5
report document tags as seen in the text (not the active tag of Thy_Output.present_thy);
wenzelm
parents:
69970
diff
changeset
|
786 |
{ |
ad6d4a14adb5
report document tags as seen in the text (not the active tag of Thy_Output.present_thy);
wenzelm
parents:
69970
diff
changeset
|
787 |
case (res, Text.Info(_, XML.Elem(Markup.Document_Tag(name), _))) => Some(name :: res) |
ad6d4a14adb5
report document tags as seen in the text (not the active tag of Thy_Output.present_thy);
wenzelm
parents:
69970
diff
changeset
|
788 |
case _ => None |
ad6d4a14adb5
report document tags as seen in the text (not the active tag of Thy_Output.present_thy);
wenzelm
parents:
69970
diff
changeset
|
789 |
}) |
ad6d4a14adb5
report document tags as seen in the text (not the active tag of Thy_Output.present_thy);
wenzelm
parents:
69970
diff
changeset
|
790 |
Library.distinct(results.flatMap(_.info.reverse)) |
ad6d4a14adb5
report document tags as seen in the text (not the active tag of Thy_Output.present_thy);
wenzelm
parents:
69970
diff
changeset
|
791 |
} |
64622
529bbb8977c7
more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
diff
changeset
|
792 |
} |