1 /* Title: Tools/jEdit/src/rendering.scala |
|
2 Author: Makarius |
|
3 |
|
4 Isabelle-specific implementation of quasi-abstract rendering and |
|
5 markup interpretation. |
|
6 */ |
|
7 |
|
8 package isabelle.jedit |
|
9 |
|
10 |
|
11 import isabelle._ |
|
12 |
|
13 import java.awt.Color |
|
14 import javax.swing.Icon |
|
15 |
|
16 import org.gjt.sp.jedit.syntax.{Token => JEditToken} |
|
17 import org.gjt.sp.jedit.jEdit |
|
18 |
|
19 import scala.collection.immutable.SortedMap |
|
20 |
|
21 |
|
22 object Rendering |
|
23 { |
|
24 def apply(snapshot: Document.Snapshot, options: Options): Rendering = |
|
25 new Rendering(snapshot, options) |
|
26 |
|
27 |
|
28 /* message priorities */ |
|
29 |
|
30 private val state_pri = 1 |
|
31 private val writeln_pri = 2 |
|
32 private val information_pri = 3 |
|
33 private val tracing_pri = 4 |
|
34 private val warning_pri = 5 |
|
35 private val legacy_pri = 6 |
|
36 private val error_pri = 7 |
|
37 |
|
38 private val message_pri = Map( |
|
39 Markup.STATE -> state_pri, |
|
40 Markup.STATE_MESSAGE -> state_pri, |
|
41 Markup.WRITELN -> writeln_pri, |
|
42 Markup.WRITELN_MESSAGE -> writeln_pri, |
|
43 Markup.INFORMATION -> information_pri, |
|
44 Markup.INFORMATION_MESSAGE -> information_pri, |
|
45 Markup.TRACING -> tracing_pri, |
|
46 Markup.TRACING_MESSAGE -> tracing_pri, |
|
47 Markup.WARNING -> warning_pri, |
|
48 Markup.WARNING_MESSAGE -> warning_pri, |
|
49 Markup.LEGACY -> legacy_pri, |
|
50 Markup.LEGACY_MESSAGE -> legacy_pri, |
|
51 Markup.ERROR -> error_pri, |
|
52 Markup.ERROR_MESSAGE -> error_pri) |
|
53 |
|
54 |
|
55 /* popup window bounds */ |
|
56 |
|
57 def popup_bounds: Double = (PIDE.options.real("jedit_popup_bounds") max 0.2) min 0.8 |
|
58 |
|
59 |
|
60 /* Isabelle/Isar token markup */ |
|
61 |
|
62 private val command_style: Map[String, Byte] = |
|
63 { |
|
64 import JEditToken._ |
|
65 Map[String, Byte]( |
|
66 Keyword.THY_END -> KEYWORD2, |
|
67 Keyword.PRF_ASM -> KEYWORD3, |
|
68 Keyword.PRF_ASM_GOAL -> KEYWORD3 |
|
69 ).withDefaultValue(KEYWORD1) |
|
70 } |
|
71 |
|
72 private val token_style: Map[Token.Kind.Value, Byte] = |
|
73 { |
|
74 import JEditToken._ |
|
75 Map[Token.Kind.Value, Byte]( |
|
76 Token.Kind.KEYWORD -> KEYWORD2, |
|
77 Token.Kind.IDENT -> NULL, |
|
78 Token.Kind.LONG_IDENT -> NULL, |
|
79 Token.Kind.SYM_IDENT -> NULL, |
|
80 Token.Kind.VAR -> NULL, |
|
81 Token.Kind.TYPE_IDENT -> NULL, |
|
82 Token.Kind.TYPE_VAR -> NULL, |
|
83 Token.Kind.NAT -> NULL, |
|
84 Token.Kind.FLOAT -> NULL, |
|
85 Token.Kind.SPACE -> NULL, |
|
86 Token.Kind.STRING -> LITERAL1, |
|
87 Token.Kind.ALT_STRING -> LITERAL2, |
|
88 Token.Kind.VERBATIM -> COMMENT3, |
|
89 Token.Kind.CARTOUCHE -> COMMENT4, |
|
90 Token.Kind.COMMENT -> COMMENT1, |
|
91 Token.Kind.ERROR -> INVALID |
|
92 ).withDefaultValue(NULL) |
|
93 } |
|
94 |
|
95 def token_markup(syntax: Outer_Syntax, token: Token): Byte = |
|
96 if (token.is_command) command_style(syntax.keywords.kinds.getOrElse(token.content, "")) |
|
97 else if (token.is_keyword && token.source == Symbol.comment_decoded) JEditToken.NULL |
|
98 else if (token.is_delimiter) JEditToken.OPERATOR |
|
99 else token_style(token.kind) |
|
100 |
|
101 |
|
102 /* Isabelle/ML token markup */ |
|
103 |
|
104 private val ml_token_style: Map[ML_Lex.Kind.Value, Byte] = |
|
105 { |
|
106 import JEditToken._ |
|
107 Map[ML_Lex.Kind.Value, Byte]( |
|
108 ML_Lex.Kind.KEYWORD -> NULL, |
|
109 ML_Lex.Kind.IDENT -> NULL, |
|
110 ML_Lex.Kind.LONG_IDENT -> NULL, |
|
111 ML_Lex.Kind.TYPE_VAR -> NULL, |
|
112 ML_Lex.Kind.WORD -> DIGIT, |
|
113 ML_Lex.Kind.INT -> DIGIT, |
|
114 ML_Lex.Kind.REAL -> DIGIT, |
|
115 ML_Lex.Kind.CHAR -> LITERAL2, |
|
116 ML_Lex.Kind.STRING -> LITERAL1, |
|
117 ML_Lex.Kind.SPACE -> NULL, |
|
118 ML_Lex.Kind.COMMENT -> COMMENT1, |
|
119 ML_Lex.Kind.ANTIQ -> NULL, |
|
120 ML_Lex.Kind.ANTIQ_START -> LITERAL4, |
|
121 ML_Lex.Kind.ANTIQ_STOP -> LITERAL4, |
|
122 ML_Lex.Kind.ANTIQ_OTHER -> NULL, |
|
123 ML_Lex.Kind.ANTIQ_STRING -> NULL, |
|
124 ML_Lex.Kind.ANTIQ_ALT_STRING -> NULL, |
|
125 ML_Lex.Kind.ANTIQ_CARTOUCHE -> NULL, |
|
126 ML_Lex.Kind.ERROR -> INVALID |
|
127 ).withDefaultValue(NULL) |
|
128 } |
|
129 |
|
130 def ml_token_markup(token: ML_Lex.Token): Byte = |
|
131 if (!token.is_keyword) ml_token_style(token.kind) |
|
132 else if (token.is_delimiter) JEditToken.OPERATOR |
|
133 else if (ML_Lex.keywords2(token.source)) JEditToken.KEYWORD2 |
|
134 else if (ML_Lex.keywords3(token.source)) JEditToken.KEYWORD3 |
|
135 else JEditToken.KEYWORD1 |
|
136 |
|
137 |
|
138 /* markup elements */ |
|
139 |
|
140 private val indentation_elements = |
|
141 Markup.Elements(Markup.Command_Indent.name) |
|
142 |
|
143 private val semantic_completion_elements = |
|
144 Markup.Elements(Markup.COMPLETION, Markup.NO_COMPLETION) |
|
145 |
|
146 private val language_context_elements = |
|
147 Markup.Elements(Markup.STRING, Markup.ALT_STRING, Markup.VERBATIM, |
|
148 Markup.CARTOUCHE, Markup.COMMENT, Markup.LANGUAGE, |
|
149 Markup.ML_STRING, Markup.ML_COMMENT) |
|
150 |
|
151 private val language_elements = Markup.Elements(Markup.LANGUAGE) |
|
152 |
|
153 private val citation_elements = Markup.Elements(Markup.CITATION) |
|
154 |
|
155 private val breakpoint_elements = Markup.Elements(Markup.ML_BREAKPOINT) |
|
156 |
|
157 private val caret_focus_elements = Markup.Elements(Markup.ENTITY) |
|
158 |
|
159 private val highlight_elements = |
|
160 Markup.Elements(Markup.EXPRESSION, Markup.CITATION, Markup.LANGUAGE, Markup.ML_TYPING, |
|
161 Markup.TOKEN_RANGE, Markup.ENTITY, Markup.PATH, Markup.DOC, Markup.URL, Markup.SORTING, |
|
162 Markup.TYPING, Markup.CLASS_PARAMETER, Markup.FREE, Markup.SKOLEM, Markup.BOUND, |
|
163 Markup.VAR, Markup.TFREE, Markup.TVAR, Markup.ML_BREAKPOINT, |
|
164 Markup.MARKDOWN_PARAGRAPH, Markup.Markdown_List.name) |
|
165 |
|
166 private val hyperlink_elements = |
|
167 Markup.Elements(Markup.ENTITY, Markup.PATH, Markup.DOC, Markup.POSITION, |
|
168 Markup.CITATION, Markup.URL) |
|
169 |
|
170 private val active_elements = |
|
171 Markup.Elements(Markup.DIALOG, Markup.BROWSER, Markup.GRAPHVIEW, |
|
172 Markup.SENDBACK, Markup.JEDIT_ACTION, Markup.SIMP_TRACE_PANEL) |
|
173 |
|
174 private val tooltip_message_elements = |
|
175 Markup.Elements(Markup.WRITELN, Markup.INFORMATION, Markup.WARNING, Markup.LEGACY, Markup.ERROR, |
|
176 Markup.BAD) |
|
177 |
|
178 private val tooltip_descriptions = |
|
179 Map( |
|
180 Markup.CITATION -> "citation", |
|
181 Markup.TOKEN_RANGE -> "inner syntax token", |
|
182 Markup.FREE -> "free variable", |
|
183 Markup.SKOLEM -> "skolem variable", |
|
184 Markup.BOUND -> "bound variable", |
|
185 Markup.VAR -> "schematic variable", |
|
186 Markup.TFREE -> "free type variable", |
|
187 Markup.TVAR -> "schematic type variable") |
|
188 |
|
189 private val tooltip_elements = |
|
190 Markup.Elements(Markup.LANGUAGE, Markup.EXPRESSION, Markup.TIMING, Markup.ENTITY, |
|
191 Markup.SORTING, Markup.TYPING, Markup.CLASS_PARAMETER, Markup.ML_TYPING, |
|
192 Markup.ML_BREAKPOINT, Markup.PATH, Markup.DOC, Markup.URL, Markup.MARKDOWN_PARAGRAPH, |
|
193 Markup.Markdown_List.name) ++ Markup.Elements(tooltip_descriptions.keySet) |
|
194 |
|
195 private val gutter_elements = |
|
196 Markup.Elements(Markup.WRITELN, Markup.INFORMATION, Markup.WARNING, Markup.LEGACY, Markup.ERROR) |
|
197 |
|
198 private val squiggly_elements = |
|
199 Markup.Elements(Markup.WRITELN, Markup.INFORMATION, Markup.WARNING, Markup.LEGACY, Markup.ERROR) |
|
200 |
|
201 private val line_background_elements = |
|
202 Markup.Elements(Markup.WRITELN_MESSAGE, Markup.STATE_MESSAGE, Markup.INFORMATION_MESSAGE, |
|
203 Markup.TRACING_MESSAGE, Markup.WARNING_MESSAGE, Markup.LEGACY_MESSAGE, |
|
204 Markup.ERROR_MESSAGE) |
|
205 |
|
206 private val separator_elements = |
|
207 Markup.Elements(Markup.SEPARATOR) |
|
208 |
|
209 private val background_elements = |
|
210 Protocol.proper_status_elements + Markup.WRITELN_MESSAGE + |
|
211 Markup.STATE_MESSAGE + Markup.INFORMATION_MESSAGE + |
|
212 Markup.TRACING_MESSAGE + Markup.WARNING_MESSAGE + |
|
213 Markup.LEGACY_MESSAGE + Markup.ERROR_MESSAGE + |
|
214 Markup.BAD + Markup.INTENSIFY + Markup.ENTITY + |
|
215 Markup.Markdown_Item.name ++ active_elements |
|
216 |
|
217 private val foreground_elements = |
|
218 Markup.Elements(Markup.STRING, Markup.ALT_STRING, Markup.VERBATIM, |
|
219 Markup.CARTOUCHE, Markup.ANTIQUOTED) |
|
220 |
|
221 private val bullet_elements = |
|
222 Markup.Elements(Markup.BULLET, Markup.ML_BREAKPOINT) |
|
223 |
|
224 private val fold_depth_elements = |
|
225 Markup.Elements(Markup.TEXT_FOLD, Markup.GOAL, Markup.SUBGOAL) |
|
226 } |
|
227 |
|
228 |
|
229 class Rendering private(val snapshot: Document.Snapshot, val options: Options) |
|
230 { |
|
231 override def toString: String = "Rendering(" + snapshot.toString + ")" |
|
232 |
|
233 |
|
234 /* colors */ |
|
235 |
|
236 def color_value(s: String): Color = Color_Value(options.string(s)) |
|
237 |
|
238 val outdated_color = color_value("outdated_color") |
|
239 val unprocessed_color = color_value("unprocessed_color") |
|
240 val unprocessed1_color = color_value("unprocessed1_color") |
|
241 val running_color = color_value("running_color") |
|
242 val running1_color = color_value("running1_color") |
|
243 val bullet_color = color_value("bullet_color") |
|
244 val tooltip_color = color_value("tooltip_color") |
|
245 val writeln_color = color_value("writeln_color") |
|
246 val information_color = color_value("information_color") |
|
247 val warning_color = color_value("warning_color") |
|
248 val legacy_color = color_value("legacy_color") |
|
249 val error_color = color_value("error_color") |
|
250 val writeln_message_color = color_value("writeln_message_color") |
|
251 val information_message_color = color_value("information_message_color") |
|
252 val tracing_message_color = color_value("tracing_message_color") |
|
253 val warning_message_color = color_value("warning_message_color") |
|
254 val legacy_message_color = color_value("legacy_message_color") |
|
255 val error_message_color = color_value("error_message_color") |
|
256 val spell_checker_color = color_value("spell_checker_color") |
|
257 val bad_color = color_value("bad_color") |
|
258 val intensify_color = color_value("intensify_color") |
|
259 val entity_color = color_value("entity_color") |
|
260 val entity_ref_color = color_value("entity_ref_color") |
|
261 val breakpoint_disabled_color = color_value("breakpoint_disabled_color") |
|
262 val breakpoint_enabled_color = color_value("breakpoint_enabled_color") |
|
263 val caret_debugger_color = color_value("caret_debugger_color") |
|
264 val quoted_color = color_value("quoted_color") |
|
265 val antiquoted_color = color_value("antiquoted_color") |
|
266 val antiquote_color = color_value("antiquote_color") |
|
267 val highlight_color = color_value("highlight_color") |
|
268 val hyperlink_color = color_value("hyperlink_color") |
|
269 val active_color = color_value("active_color") |
|
270 val active_hover_color = color_value("active_hover_color") |
|
271 val active_result_color = color_value("active_result_color") |
|
272 val keyword1_color = color_value("keyword1_color") |
|
273 val keyword2_color = color_value("keyword2_color") |
|
274 val keyword3_color = color_value("keyword3_color") |
|
275 val quasi_keyword_color = color_value("quasi_keyword_color") |
|
276 val improper_color = color_value("improper_color") |
|
277 val operator_color = color_value("operator_color") |
|
278 val caret_invisible_color = color_value("caret_invisible_color") |
|
279 val completion_color = color_value("completion_color") |
|
280 val search_color = color_value("search_color") |
|
281 |
|
282 val tfree_color = color_value("tfree_color") |
|
283 val tvar_color = color_value("tvar_color") |
|
284 val free_color = color_value("free_color") |
|
285 val skolem_color = color_value("skolem_color") |
|
286 val bound_color = color_value("bound_color") |
|
287 val var_color = color_value("var_color") |
|
288 val inner_numeral_color = color_value("inner_numeral_color") |
|
289 val inner_quoted_color = color_value("inner_quoted_color") |
|
290 val inner_cartouche_color = color_value("inner_cartouche_color") |
|
291 val inner_comment_color = color_value("inner_comment_color") |
|
292 val dynamic_color = color_value("dynamic_color") |
|
293 val class_parameter_color = color_value("class_parameter_color") |
|
294 |
|
295 val markdown_item_color1 = color_value("markdown_item_color1") |
|
296 val markdown_item_color2 = color_value("markdown_item_color2") |
|
297 val markdown_item_color3 = color_value("markdown_item_color3") |
|
298 val markdown_item_color4 = color_value("markdown_item_color4") |
|
299 |
|
300 |
|
301 /* indentation */ |
|
302 |
|
303 def indentation(range: Text.Range): Int = |
|
304 snapshot.select(range, Rendering.indentation_elements, _ => |
|
305 { |
|
306 case Text.Info(_, XML.Elem(Markup.Command_Indent(i), _)) => Some(i) |
|
307 case _ => None |
|
308 }).headOption.map(_.info).getOrElse(0) |
|
309 |
|
310 |
|
311 /* completion */ |
|
312 |
|
313 def semantic_completion(completed_range: Option[Text.Range], range: Text.Range) |
|
314 : Option[Text.Info[Completion.Semantic]] = |
|
315 if (snapshot.is_outdated) None |
|
316 else { |
|
317 snapshot.select(range, Rendering.semantic_completion_elements, _ => |
|
318 { |
|
319 case Completion.Semantic.Info(info) => |
|
320 completed_range match { |
|
321 case Some(range0) if range0.contains(info.range) && range0 != info.range => None |
|
322 case _ => Some(info) |
|
323 } |
|
324 case _ => None |
|
325 }).headOption.map(_.info) |
|
326 } |
|
327 |
|
328 def language_context(range: Text.Range): Option[Completion.Language_Context] = |
|
329 snapshot.select(range, Rendering.language_context_elements, _ => |
|
330 { |
|
331 case Text.Info(_, XML.Elem(Markup.Language(language, symbols, antiquotes, delimited), _)) => |
|
332 if (delimited) Some(Completion.Language_Context(language, symbols, antiquotes)) |
|
333 else None |
|
334 case Text.Info(_, elem) |
|
335 if elem.name == Markup.ML_STRING || elem.name == Markup.ML_COMMENT => |
|
336 Some(Completion.Language_Context.ML_inner) |
|
337 case Text.Info(_, _) => |
|
338 Some(Completion.Language_Context.inner) |
|
339 }).headOption.map(_.info) |
|
340 |
|
341 def language_path(range: Text.Range): Option[Text.Range] = |
|
342 snapshot.select(range, Rendering.language_elements, _ => |
|
343 { |
|
344 case Text.Info(info_range, XML.Elem(Markup.Language(Markup.Language.PATH, _, _, _), _)) => |
|
345 Some(snapshot.convert(info_range)) |
|
346 case _ => None |
|
347 }).headOption.map(_.info) |
|
348 |
|
349 def citation(range: Text.Range): Option[Text.Info[String]] = |
|
350 snapshot.select(range, Rendering.citation_elements, _ => |
|
351 { |
|
352 case Text.Info(info_range, XML.Elem(Markup.Citation(name), _)) => |
|
353 Some(Text.Info(snapshot.convert(info_range), name)) |
|
354 case _ => None |
|
355 }).headOption.map(_.info) |
|
356 |
|
357 |
|
358 /* spell checker */ |
|
359 |
|
360 private lazy val spell_checker_elements = |
|
361 Markup.Elements(space_explode(',', options.string("spell_checker_elements")): _*) |
|
362 |
|
363 def spell_checker_ranges(range: Text.Range): List[Text.Range] = |
|
364 snapshot.select(range, spell_checker_elements, _ => _ => Some(())).map(_.range) |
|
365 |
|
366 def spell_checker_point(range: Text.Range): Option[Text.Range] = |
|
367 snapshot.select(range, spell_checker_elements, _ => |
|
368 { |
|
369 case info => Some(snapshot.convert(info.range)) |
|
370 }).headOption.map(_.info) |
|
371 |
|
372 |
|
373 /* breakpoints */ |
|
374 |
|
375 def breakpoint(range: Text.Range): Option[(Command, Long)] = |
|
376 if (snapshot.is_outdated) None |
|
377 else |
|
378 snapshot.select(range, Rendering.breakpoint_elements, command_states => |
|
379 { |
|
380 case Text.Info(_, Protocol.ML_Breakpoint(breakpoint)) => |
|
381 command_states match { |
|
382 case st :: _ => Some((st.command, breakpoint)) |
|
383 case _ => None |
|
384 } |
|
385 case _ => None |
|
386 }).headOption.map(_.info) |
|
387 |
|
388 |
|
389 /* command status overview */ |
|
390 |
|
391 def overview_color(range: Text.Range): Option[Color] = |
|
392 { |
|
393 if (snapshot.is_outdated) None |
|
394 else { |
|
395 val results = |
|
396 snapshot.cumulate[List[Markup]](range, Nil, Protocol.liberal_status_elements, _ => |
|
397 { |
|
398 case (status, Text.Info(_, elem)) => Some(elem.markup :: status) |
|
399 }, status = true) |
|
400 if (results.isEmpty) None |
|
401 else { |
|
402 val status = Protocol.Status.make(results.iterator.flatMap(_.info)) |
|
403 |
|
404 if (status.is_running) Some(running_color) |
|
405 else if (status.is_failed) Some(error_color) |
|
406 else if (status.is_warned) Some(warning_color) |
|
407 else if (status.is_unprocessed) Some(unprocessed_color) |
|
408 else None |
|
409 } |
|
410 } |
|
411 } |
|
412 |
|
413 |
|
414 /* caret focus */ |
|
415 |
|
416 def entity_focus(range: Text.Range, |
|
417 check: (Boolean, Long) => Boolean = (is_def: Boolean, i: Long) => is_def): Set[Long] = |
|
418 { |
|
419 val results = |
|
420 snapshot.cumulate[Set[Long]](range, Set.empty, Rendering.caret_focus_elements, _ => |
|
421 { |
|
422 case (serials, Text.Info(_, XML.Elem(Markup(Markup.ENTITY, props), _))) => |
|
423 props match { |
|
424 case Markup.Entity.Def(i) if check(true, i) => Some(serials + i) |
|
425 case Markup.Entity.Ref(i) if check(false, i) => Some(serials + i) |
|
426 case _ => None |
|
427 } |
|
428 case _ => None |
|
429 }) |
|
430 (Set.empty[Long] /: results){ case (s1, Text.Info(_, s2)) => s1 ++ s2 } |
|
431 } |
|
432 |
|
433 def caret_focus(caret_range: Text.Range, visible_range: Text.Range): Set[Long] = |
|
434 { |
|
435 val focus_defs = entity_focus(caret_range) |
|
436 if (focus_defs.nonEmpty) focus_defs |
|
437 else { |
|
438 val visible_defs = entity_focus(visible_range) |
|
439 entity_focus(caret_range, (is_def: Boolean, i: Long) => !is_def && visible_defs.contains(i)) |
|
440 } |
|
441 } |
|
442 |
|
443 def caret_focus_ranges(caret_range: Text.Range, visible_range: Text.Range): List[Text.Range] = |
|
444 { |
|
445 val focus = caret_focus(caret_range, visible_range) |
|
446 if (focus.nonEmpty) { |
|
447 val results = |
|
448 snapshot.cumulate[Boolean](visible_range, false, Rendering.caret_focus_elements, _ => |
|
449 { |
|
450 case (_, Text.Info(_, XML.Elem(Markup(Markup.ENTITY, props), _))) => |
|
451 props match { |
|
452 case Markup.Entity.Def(i) if focus(i) => Some(true) |
|
453 case Markup.Entity.Ref(i) if focus(i) => Some(true) |
|
454 case _ => None |
|
455 } |
|
456 }) |
|
457 for (info <- results if info.info) yield info.range |
|
458 } |
|
459 else Nil |
|
460 } |
|
461 |
|
462 def entity_ref(range: Text.Range, focus: Set[Long]): List[Text.Info[Color]] = |
|
463 snapshot.select(range, Rendering.caret_focus_elements, _ => |
|
464 { |
|
465 case Text.Info(_, XML.Elem(Markup(Markup.ENTITY, Markup.Entity.Ref(i)), _)) if focus(i) => |
|
466 Some(entity_ref_color) |
|
467 case _ => None |
|
468 }) |
|
469 |
|
470 |
|
471 /* highlighted area */ |
|
472 |
|
473 def highlight(range: Text.Range): Option[Text.Info[Color]] = |
|
474 snapshot.select(range, Rendering.highlight_elements, _ => |
|
475 { |
|
476 case info => Some(Text.Info(snapshot.convert(info.range), highlight_color)) |
|
477 }).headOption.map(_.info) |
|
478 |
|
479 |
|
480 /* hyperlinks */ |
|
481 |
|
482 private def jedit_file(name: String): String = |
|
483 if (Path.is_valid(name)) |
|
484 PIDE.resources.append(snapshot.node_name.master_dir, Path.explode(name)) |
|
485 else name |
|
486 |
|
487 def hyperlink(range: Text.Range): Option[Text.Info[PIDE.editor.Hyperlink]] = |
|
488 { |
|
489 snapshot.cumulate[Vector[Text.Info[PIDE.editor.Hyperlink]]]( |
|
490 range, Vector.empty, Rendering.hyperlink_elements, _ => |
|
491 { |
|
492 case (links, Text.Info(info_range, XML.Elem(Markup.Path(name), _))) => |
|
493 val link = PIDE.editor.hyperlink_file(true, jedit_file(name)) |
|
494 Some(links :+ Text.Info(snapshot.convert(info_range), link)) |
|
495 |
|
496 case (links, Text.Info(info_range, XML.Elem(Markup.Doc(name), _))) => |
|
497 PIDE.editor.hyperlink_doc(name).map(link => |
|
498 (links :+ Text.Info(snapshot.convert(info_range), link))) |
|
499 |
|
500 case (links, Text.Info(info_range, XML.Elem(Markup.Url(name), _))) => |
|
501 val link = PIDE.editor.hyperlink_url(name) |
|
502 Some(links :+ Text.Info(snapshot.convert(info_range), link)) |
|
503 |
|
504 case (links, Text.Info(info_range, XML.Elem(Markup(Markup.ENTITY, props), _))) |
|
505 if !props.exists( |
|
506 { case (Markup.KIND, Markup.ML_OPEN) => true |
|
507 case (Markup.KIND, Markup.ML_STRUCTURE) => true |
|
508 case _ => false }) => |
|
509 val opt_link = PIDE.editor.hyperlink_def_position(true, snapshot, props) |
|
510 opt_link.map(link => links :+ Text.Info(snapshot.convert(info_range), link)) |
|
511 |
|
512 case (links, Text.Info(info_range, XML.Elem(Markup(Markup.POSITION, props), _))) => |
|
513 val opt_link = PIDE.editor.hyperlink_position(true, snapshot, props) |
|
514 opt_link.map(link => links :+ Text.Info(snapshot.convert(info_range), link)) |
|
515 |
|
516 case (links, Text.Info(info_range, XML.Elem(Markup.Citation(name), _))) => |
|
517 val opt_link = |
|
518 Bibtex_JEdit.entries_iterator.collectFirst( |
|
519 { case (a, buffer, offset) if a == name => |
|
520 PIDE.editor.hyperlink_buffer(true, buffer, offset) }) |
|
521 opt_link.map(link => links :+ Text.Info(snapshot.convert(info_range), link)) |
|
522 |
|
523 case _ => None |
|
524 }) match { case Text.Info(_, _ :+ info) :: _ => Some(info) case _ => None } |
|
525 } |
|
526 |
|
527 |
|
528 /* active elements */ |
|
529 |
|
530 def active(range: Text.Range): Option[Text.Info[XML.Elem]] = |
|
531 snapshot.select(range, Rendering.active_elements, command_states => |
|
532 { |
|
533 case Text.Info(info_range, elem) => |
|
534 if (elem.name == Markup.DIALOG) { |
|
535 elem match { |
|
536 case Protocol.Dialog(_, serial, _) |
|
537 if !command_states.exists(st => st.results.defined(serial)) => |
|
538 Some(Text.Info(snapshot.convert(info_range), elem)) |
|
539 case _ => None |
|
540 } |
|
541 } |
|
542 else Some(Text.Info(snapshot.convert(info_range), elem)) |
|
543 }).headOption.map(_.info) |
|
544 |
|
545 def command_results(range: Text.Range): Command.Results = |
|
546 Command.State.merge_results( |
|
547 snapshot.select[List[Command.State]](range, Markup.Elements.full, command_states => |
|
548 { case _ => Some(command_states) }).flatMap(_.info)) |
|
549 |
|
550 |
|
551 /* tooltip messages */ |
|
552 |
|
553 def tooltip_message(range: Text.Range): Option[Text.Info[XML.Body]] = |
|
554 { |
|
555 val results = |
|
556 snapshot.cumulate[List[Text.Info[Command.Results.Entry]]]( |
|
557 range, Nil, Rendering.tooltip_message_elements, _ => |
|
558 { |
|
559 case (msgs, Text.Info(info_range, msg @ XML.Elem(Markup(Markup.BAD, _), body))) |
|
560 if body.nonEmpty => |
|
561 val entry: Command.Results.Entry = (Document_ID.make(), msg) |
|
562 Some(Text.Info(snapshot.convert(info_range), entry) :: msgs) |
|
563 |
|
564 case (msgs, Text.Info(info_range, |
|
565 XML.Elem(Markup(name, props @ Markup.Serial(serial)), body))) => |
|
566 val entry: Command.Results.Entry = |
|
567 serial -> XML.Elem(Markup(Markup.message(name), props), body) |
|
568 Some(Text.Info(snapshot.convert(info_range), entry) :: msgs) |
|
569 |
|
570 case _ => None |
|
571 }).flatMap(_.info) |
|
572 if (results.isEmpty) None |
|
573 else { |
|
574 val r = Text.Range(results.head.range.start, results.last.range.stop) |
|
575 val msgs = Command.Results.make(results.map(_.info)) |
|
576 Some(Text.Info(r, Pretty.separate(msgs.iterator.map(_._2).toList))) |
|
577 } |
|
578 } |
|
579 |
|
580 |
|
581 /* tooltips */ |
|
582 |
|
583 private def pretty_typing(kind: String, body: XML.Body): XML.Tree = |
|
584 Pretty.block(XML.Text(kind) :: Pretty.brk(1) :: body) |
|
585 |
|
586 private def timing_threshold: Double = options.real("jedit_timing_threshold") |
|
587 |
|
588 def tooltip(range: Text.Range): Option[Text.Info[XML.Body]] = |
|
589 { |
|
590 def add(prev: Text.Info[(Timing, Vector[(Boolean, XML.Tree)])], |
|
591 r0: Text.Range, p: (Boolean, XML.Tree)): Text.Info[(Timing, Vector[(Boolean, XML.Tree)])] = |
|
592 { |
|
593 val r = snapshot.convert(r0) |
|
594 val (t, info) = prev.info |
|
595 if (prev.range == r) |
|
596 Text.Info(r, (t, info :+ p)) |
|
597 else Text.Info(r, (t, Vector(p))) |
|
598 } |
|
599 |
|
600 val results = |
|
601 snapshot.cumulate[Text.Info[(Timing, Vector[(Boolean, XML.Tree)])]]( |
|
602 range, Text.Info(range, (Timing.zero, Vector.empty)), Rendering.tooltip_elements, _ => |
|
603 { |
|
604 case (Text.Info(r, (t1, info)), Text.Info(_, XML.Elem(Markup.Timing(t2), _))) => |
|
605 Some(Text.Info(r, (t1 + t2, info))) |
|
606 |
|
607 case (prev, Text.Info(r, XML.Elem(Markup.Entity(kind, name), _))) |
|
608 if kind != "" && |
|
609 kind != Markup.ML_DEF && |
|
610 kind != Markup.ML_OPEN && |
|
611 kind != Markup.ML_STRUCTURE => |
|
612 val kind1 = Word.implode(Word.explode('_', kind)) |
|
613 val txt1 = |
|
614 if (name == "") kind1 |
|
615 else if (kind1 == "") quote(name) |
|
616 else kind1 + " " + quote(name) |
|
617 val t = prev.info._1 |
|
618 val txt2 = |
|
619 if (kind == Markup.COMMAND && t.elapsed.seconds >= timing_threshold) |
|
620 "\n" + t.message |
|
621 else "" |
|
622 Some(add(prev, r, (true, XML.Text(txt1 + txt2)))) |
|
623 |
|
624 case (prev, Text.Info(r, XML.Elem(Markup.Path(name), _))) => |
|
625 val file = jedit_file(name) |
|
626 val text = |
|
627 if (name == file) "file " + quote(file) |
|
628 else "path " + quote(name) + "\nfile " + quote(file) |
|
629 Some(add(prev, r, (true, XML.Text(text)))) |
|
630 |
|
631 case (prev, Text.Info(r, XML.Elem(Markup.Doc(name), _))) => |
|
632 val text = "doc " + quote(name) |
|
633 Some(add(prev, r, (true, XML.Text(text)))) |
|
634 |
|
635 case (prev, Text.Info(r, XML.Elem(Markup.Url(name), _))) => |
|
636 Some(add(prev, r, (true, XML.Text("URL " + quote(name))))) |
|
637 |
|
638 case (prev, Text.Info(r, XML.Elem(Markup(name, _), body))) |
|
639 if name == Markup.SORTING || name == Markup.TYPING => |
|
640 Some(add(prev, r, (true, pretty_typing("::", body)))) |
|
641 |
|
642 case (prev, Text.Info(r, XML.Elem(Markup(Markup.CLASS_PARAMETER, _), body))) => |
|
643 Some(add(prev, r, (true, Pretty.block(0, body)))) |
|
644 |
|
645 case (prev, Text.Info(r, XML.Elem(Markup(Markup.ML_TYPING, _), body))) => |
|
646 Some(add(prev, r, (false, pretty_typing("ML:", body)))) |
|
647 |
|
648 case (prev, Text.Info(r, Protocol.ML_Breakpoint(breakpoint))) => |
|
649 val text = |
|
650 if (Debugger.breakpoint_state(breakpoint)) "breakpoint (enabled)" |
|
651 else "breakpoint (disabled)" |
|
652 Some(add(prev, r, (true, XML.Text(text)))) |
|
653 |
|
654 case (prev, Text.Info(r, XML.Elem(Markup.Language(language, _, _, _), _))) => |
|
655 val lang = Word.implode(Word.explode('_', language)) |
|
656 Some(add(prev, r, (true, XML.Text("language: " + lang)))) |
|
657 |
|
658 case (prev, Text.Info(r, XML.Elem(Markup.Expression(kind), _))) => |
|
659 val descr = if (kind == "") "expression" else "expression: " + kind |
|
660 Some(add(prev, r, (true, XML.Text(descr)))) |
|
661 |
|
662 case (prev, Text.Info(r, XML.Elem(Markup(Markup.MARKDOWN_PARAGRAPH, _), _))) => |
|
663 Some(add(prev, r, (true, XML.Text("Markdown: paragraph")))) |
|
664 case (prev, Text.Info(r, XML.Elem(Markup.Markdown_List(kind), _))) => |
|
665 Some(add(prev, r, (true, XML.Text("Markdown: " + kind)))) |
|
666 |
|
667 case (prev, Text.Info(r, XML.Elem(Markup(name, _), _))) => |
|
668 Rendering.tooltip_descriptions.get(name). |
|
669 map(descr => add(prev, r, (true, XML.Text(descr)))) |
|
670 }).map(_.info) |
|
671 |
|
672 results.map(_.info).flatMap(res => res._2.toList) match { |
|
673 case Nil => None |
|
674 case tips => |
|
675 val r = Text.Range(results.head.range.start, results.last.range.stop) |
|
676 val all_tips = (tips.filter(_._1) ++ tips.filter(!_._1).lastOption.toList).map(_._2) |
|
677 Some(Text.Info(r, Library.separate(Pretty.fbrk, all_tips))) |
|
678 } |
|
679 } |
|
680 |
|
681 def tooltip_margin: Int = options.int("jedit_tooltip_margin") |
|
682 |
|
683 lazy val tooltip_close_icon = JEdit_Lib.load_icon(options.string("tooltip_close_icon")) |
|
684 lazy val tooltip_detach_icon = JEdit_Lib.load_icon(options.string("tooltip_detach_icon")) |
|
685 |
|
686 |
|
687 /* gutter */ |
|
688 |
|
689 private def gutter_message_pri(msg: XML.Tree): Int = |
|
690 if (Protocol.is_error(msg)) Rendering.error_pri |
|
691 else if (Protocol.is_legacy(msg)) Rendering.legacy_pri |
|
692 else if (Protocol.is_warning(msg)) Rendering.warning_pri |
|
693 else if (Protocol.is_information(msg)) Rendering.information_pri |
|
694 else 0 |
|
695 |
|
696 private lazy val gutter_message_content = Map( |
|
697 Rendering.information_pri -> |
|
698 (JEdit_Lib.load_icon(options.string("gutter_information_icon")), information_message_color), |
|
699 Rendering.warning_pri -> |
|
700 (JEdit_Lib.load_icon(options.string("gutter_warning_icon")), warning_message_color), |
|
701 Rendering.legacy_pri -> |
|
702 (JEdit_Lib.load_icon(options.string("gutter_legacy_icon")), warning_message_color), |
|
703 Rendering.error_pri -> |
|
704 (JEdit_Lib.load_icon(options.string("gutter_error_icon")), error_message_color)) |
|
705 |
|
706 def gutter_content(range: Text.Range): Option[(Icon, Color)] = |
|
707 { |
|
708 val pris = |
|
709 snapshot.cumulate[Int](range, 0, Rendering.gutter_elements, _ => |
|
710 { |
|
711 case (pri, Text.Info(_, msg @ XML.Elem(Markup(_, Markup.Serial(serial)), _))) => |
|
712 Some(pri max gutter_message_pri(msg)) |
|
713 case _ => None |
|
714 }).map(_.info) |
|
715 |
|
716 gutter_message_content.get((0 /: pris)(_ max _)) |
|
717 } |
|
718 |
|
719 |
|
720 /* squiggly underline */ |
|
721 |
|
722 private lazy val squiggly_colors = Map( |
|
723 Rendering.writeln_pri -> writeln_color, |
|
724 Rendering.information_pri -> information_color, |
|
725 Rendering.warning_pri -> warning_color, |
|
726 Rendering.legacy_pri -> legacy_color, |
|
727 Rendering.error_pri -> error_color) |
|
728 |
|
729 def squiggly_underline(range: Text.Range): List[Text.Info[Color]] = |
|
730 { |
|
731 val results = |
|
732 snapshot.cumulate[Int](range, 0, Rendering.squiggly_elements, _ => |
|
733 { |
|
734 case (pri, Text.Info(_, elem)) => Some(pri max Rendering.message_pri(elem.name)) |
|
735 }) |
|
736 for { |
|
737 Text.Info(r, pri) <- results |
|
738 color <- squiggly_colors.get(pri) |
|
739 } yield Text.Info(r, color) |
|
740 } |
|
741 |
|
742 |
|
743 /* message output */ |
|
744 |
|
745 private lazy val message_colors = Map( |
|
746 Rendering.writeln_pri -> writeln_message_color, |
|
747 Rendering.information_pri -> information_message_color, |
|
748 Rendering.tracing_pri -> tracing_message_color, |
|
749 Rendering.warning_pri -> warning_message_color, |
|
750 Rendering.legacy_pri -> legacy_message_color, |
|
751 Rendering.error_pri -> error_message_color) |
|
752 |
|
753 def line_background(range: Text.Range): Option[(Color, Boolean)] = |
|
754 { |
|
755 val results = |
|
756 snapshot.cumulate[Int](range, 0, Rendering.line_background_elements, _ => |
|
757 { |
|
758 case (pri, Text.Info(_, elem)) => Some(pri max Rendering.message_pri(elem.name)) |
|
759 }) |
|
760 val pri = (0 /: results) { case (p1, Text.Info(_, p2)) => p1 max p2 } |
|
761 |
|
762 message_colors.get(pri).map(message_color => |
|
763 { |
|
764 val is_separator = |
|
765 snapshot.cumulate[Boolean](range, false, Rendering.separator_elements, _ => |
|
766 { |
|
767 case _ => Some(true) |
|
768 }).exists(_.info) |
|
769 (message_color, is_separator) |
|
770 }) |
|
771 } |
|
772 |
|
773 def output_messages(results: Command.Results): List[XML.Tree] = |
|
774 { |
|
775 val (states, other) = |
|
776 results.iterator.map(_._2).filterNot(Protocol.is_result(_)).toList |
|
777 .partition(Protocol.is_state(_)) |
|
778 states ::: other |
|
779 } |
|
780 |
|
781 |
|
782 /* text background */ |
|
783 |
|
784 def background(range: Text.Range, focus: Set[Long]): List[Text.Info[Color]] = |
|
785 { |
|
786 for { |
|
787 Text.Info(r, result) <- |
|
788 snapshot.cumulate[(List[Markup], Option[Color])]( |
|
789 range, (List(Markup.Empty), None), Rendering.background_elements, |
|
790 command_states => |
|
791 { |
|
792 case (((status, color), Text.Info(_, XML.Elem(markup, _)))) |
|
793 if status.nonEmpty && Protocol.proper_status_elements(markup.name) => |
|
794 Some((markup :: status, color)) |
|
795 case (_, Text.Info(_, XML.Elem(Markup(Markup.BAD, _), _))) => |
|
796 Some((Nil, Some(bad_color))) |
|
797 case (_, Text.Info(_, XML.Elem(Markup(Markup.INTENSIFY, _), _))) => |
|
798 Some((Nil, Some(intensify_color))) |
|
799 case (_, Text.Info(_, XML.Elem(Markup(Markup.ENTITY, props), _))) => |
|
800 props match { |
|
801 case Markup.Entity.Def(i) if focus(i) => Some((Nil, Some(entity_color))) |
|
802 case Markup.Entity.Ref(i) if focus(i) => Some((Nil, Some(entity_color))) |
|
803 case _ => None |
|
804 } |
|
805 case (_, Text.Info(_, XML.Elem(Markup.Markdown_Item(depth), _))) => |
|
806 val color = |
|
807 depth match { |
|
808 case 1 => markdown_item_color1 |
|
809 case 2 => markdown_item_color2 |
|
810 case 3 => markdown_item_color3 |
|
811 case _ => markdown_item_color4 |
|
812 } |
|
813 Some((Nil, Some(color))) |
|
814 case (acc, Text.Info(_, Protocol.Dialog(_, serial, result))) => |
|
815 command_states.collectFirst( |
|
816 { case st if st.results.defined(serial) => st.results.get(serial).get }) match |
|
817 { |
|
818 case Some(Protocol.Dialog_Result(res)) if res == result => |
|
819 Some((Nil, Some(active_result_color))) |
|
820 case _ => |
|
821 Some((Nil, Some(active_color))) |
|
822 } |
|
823 case (_, Text.Info(_, elem)) => |
|
824 if (Rendering.active_elements(elem.name)) Some((Nil, Some(active_color))) |
|
825 else None |
|
826 }) |
|
827 color <- |
|
828 (result match { |
|
829 case (markups, opt_color) if markups.nonEmpty => |
|
830 val status = Protocol.Status.make(markups.iterator) |
|
831 if (status.is_unprocessed) Some(unprocessed1_color) |
|
832 else if (status.is_running) Some(running1_color) |
|
833 else opt_color |
|
834 case (_, opt_color) => opt_color |
|
835 }) |
|
836 } yield Text.Info(r, color) |
|
837 } |
|
838 |
|
839 |
|
840 /* text foreground */ |
|
841 |
|
842 def foreground(range: Text.Range): List[Text.Info[Color]] = |
|
843 snapshot.select(range, Rendering.foreground_elements, _ => |
|
844 { |
|
845 case Text.Info(_, elem) => |
|
846 if (elem.name == Markup.ANTIQUOTED) Some(antiquoted_color) else Some(quoted_color) |
|
847 }) |
|
848 |
|
849 |
|
850 /* text color */ |
|
851 |
|
852 val foreground_color = jEdit.getColorProperty("view.fgColor") |
|
853 |
|
854 private lazy val text_colors: Map[String, Color] = Map( |
|
855 Markup.KEYWORD1 -> keyword1_color, |
|
856 Markup.KEYWORD2 -> keyword2_color, |
|
857 Markup.KEYWORD3 -> keyword3_color, |
|
858 Markup.QUASI_KEYWORD -> quasi_keyword_color, |
|
859 Markup.IMPROPER -> improper_color, |
|
860 Markup.OPERATOR -> operator_color, |
|
861 Markup.STRING -> foreground_color, |
|
862 Markup.ALT_STRING -> foreground_color, |
|
863 Markup.VERBATIM -> foreground_color, |
|
864 Markup.CARTOUCHE -> foreground_color, |
|
865 Markup.LITERAL -> keyword1_color, |
|
866 Markup.DELIMITER -> foreground_color, |
|
867 Markup.TFREE -> tfree_color, |
|
868 Markup.TVAR -> tvar_color, |
|
869 Markup.FREE -> free_color, |
|
870 Markup.SKOLEM -> skolem_color, |
|
871 Markup.BOUND -> bound_color, |
|
872 Markup.VAR -> var_color, |
|
873 Markup.INNER_STRING -> inner_quoted_color, |
|
874 Markup.INNER_CARTOUCHE -> inner_cartouche_color, |
|
875 Markup.INNER_COMMENT -> inner_comment_color, |
|
876 Markup.DYNAMIC_FACT -> dynamic_color, |
|
877 Markup.CLASS_PARAMETER -> class_parameter_color, |
|
878 Markup.ANTIQUOTE -> antiquote_color, |
|
879 Markup.ML_KEYWORD1 -> keyword1_color, |
|
880 Markup.ML_KEYWORD2 -> keyword2_color, |
|
881 Markup.ML_KEYWORD3 -> keyword3_color, |
|
882 Markup.ML_DELIMITER -> foreground_color, |
|
883 Markup.ML_NUMERAL -> inner_numeral_color, |
|
884 Markup.ML_CHAR -> inner_quoted_color, |
|
885 Markup.ML_STRING -> inner_quoted_color, |
|
886 Markup.ML_COMMENT -> inner_comment_color, |
|
887 Markup.SML_STRING -> inner_quoted_color, |
|
888 Markup.SML_COMMENT -> inner_comment_color) |
|
889 |
|
890 private lazy val text_color_elements = |
|
891 Markup.Elements(text_colors.keySet) |
|
892 |
|
893 def text_color(range: Text.Range, color: Color): List[Text.Info[Color]] = |
|
894 { |
|
895 if (color == Token_Markup.hidden_color) List(Text.Info(range, color)) |
|
896 else |
|
897 snapshot.cumulate(range, color, text_color_elements, _ => |
|
898 { |
|
899 case (_, Text.Info(_, elem)) => text_colors.get(elem.name) |
|
900 }) |
|
901 } |
|
902 |
|
903 |
|
904 /* virtual bullets */ |
|
905 |
|
906 def bullet(range: Text.Range): List[Text.Info[Color]] = |
|
907 snapshot.select(range, Rendering.bullet_elements, _ => |
|
908 { |
|
909 case Text.Info(_, Protocol.ML_Breakpoint(breakpoint)) => |
|
910 Debugger.active_breakpoint_state(breakpoint).map(b => |
|
911 if (b) breakpoint_enabled_color else breakpoint_disabled_color) |
|
912 case _ => Some(bullet_color) |
|
913 }) |
|
914 |
|
915 |
|
916 /* text folds */ |
|
917 |
|
918 def fold_depth(range: Text.Range): List[Text.Info[Int]] = |
|
919 snapshot.cumulate[Int](range, 0, Rendering.fold_depth_elements, _ => |
|
920 { |
|
921 case (depth, _) => Some(depth + 1) |
|
922 }) |
|
923 } |
|