1/* Title: Pure/PIDE/rendering.scala 2 Author: Makarius 3 4Isabelle-specific implementation of quasi-abstract rendering and 5markup interpretation. 6*/ 7 8package isabelle 9 10 11import java.io.{File => JFile} 12import java.nio.file.FileSystems 13 14 15object Rendering 16{ 17 /* color */ 18 19 object Color extends Enumeration 20 { 21 // background 22 val unprocessed1, running1, canceled, bad, intensify, entity, active, active_result, 23 markdown_bullet1, markdown_bullet2, markdown_bullet3, markdown_bullet4 = Value 24 val background_colors = values 25 26 // foreground 27 val quoted, antiquoted = Value 28 val foreground_colors = values -- background_colors 29 30 // message underline 31 val writeln, information, warning, legacy, error = Value 32 val message_underline_colors = values -- background_colors -- foreground_colors 33 34 // message background 35 val writeln_message, information_message, tracing_message, 36 warning_message, legacy_message, error_message = Value 37 val message_background_colors = 38 values -- background_colors -- foreground_colors -- message_underline_colors 39 40 // text 41 val main, keyword1, keyword2, keyword3, quasi_keyword, improper, operator, 42 tfree, tvar, free, skolem, bound, `var`, inner_numeral, inner_quoted, 43 inner_cartouche, comment1, comment2, comment3, dynamic, class_parameter, 44 antiquote, raw_text, plain_text = Value 45 val text_colors = 46 values -- background_colors -- foreground_colors -- message_underline_colors -- 47 message_background_colors 48 49 // text overview 50 val unprocessed, running = Value 51 val text_overview_colors = Set(unprocessed, running, error, warning) 52 } 53 54 55 /* output messages */ 56 57 val state_pri = 1 58 val writeln_pri = 2 59 val information_pri = 3 60 val tracing_pri = 4 61 val warning_pri = 5 62 val legacy_pri = 6 63 val error_pri = 7 64 65 val message_pri = Map( 66 Markup.STATE -> state_pri, 67 Markup.STATE_MESSAGE -> state_pri, 68 Markup.WRITELN -> writeln_pri, 69 Markup.WRITELN_MESSAGE -> writeln_pri, 70 Markup.INFORMATION -> information_pri, 71 Markup.INFORMATION_MESSAGE -> information_pri, 72 Markup.TRACING -> tracing_pri, 73 Markup.TRACING_MESSAGE -> tracing_pri, 74 Markup.WARNING -> warning_pri, 75 Markup.WARNING_MESSAGE -> warning_pri, 76 Markup.LEGACY -> legacy_pri, 77 Markup.LEGACY_MESSAGE -> legacy_pri, 78 Markup.ERROR -> error_pri, 79 Markup.ERROR_MESSAGE -> error_pri 80 ).withDefaultValue(0) 81 82 val message_underline_color = Map( 83 writeln_pri -> Color.writeln, 84 information_pri -> Color.information, 85 warning_pri -> Color.warning, 86 legacy_pri -> Color.legacy, 87 error_pri -> Color.error) 88 89 val message_background_color = Map( 90 writeln_pri -> Color.writeln_message, 91 information_pri -> Color.information_message, 92 tracing_pri -> Color.tracing_message, 93 warning_pri -> Color.warning_message, 94 legacy_pri -> Color.legacy_message, 95 error_pri -> Color.error_message) 96 97 def output_messages(results: Command.Results): List[XML.Tree] = 98 { 99 val (states, other) = 100 results.iterator.map(_._2).filterNot(Protocol.is_result(_)).toList 101 .partition(Protocol.is_state(_)) 102 states ::: other 103 } 104 105 106 /* text color */ 107 108 val text_color = Map( 109 Markup.KEYWORD1 -> Color.keyword1, 110 Markup.KEYWORD2 -> Color.keyword2, 111 Markup.KEYWORD3 -> Color.keyword3, 112 Markup.QUASI_KEYWORD -> Color.quasi_keyword, 113 Markup.IMPROPER -> Color.improper, 114 Markup.OPERATOR -> Color.operator, 115 Markup.STRING -> Color.main, 116 Markup.ALT_STRING -> Color.main, 117 Markup.VERBATIM -> Color.main, 118 Markup.CARTOUCHE -> Color.main, 119 Markup.LITERAL -> Color.keyword1, 120 Markup.DELIMITER -> Color.main, 121 Markup.TFREE -> Color.tfree, 122 Markup.TVAR -> Color.tvar, 123 Markup.FREE -> Color.free, 124 Markup.SKOLEM -> Color.skolem, 125 Markup.BOUND -> Color.bound, 126 Markup.VAR -> Color.`var`, 127 Markup.INNER_STRING -> Color.inner_quoted, 128 Markup.INNER_CARTOUCHE -> Color.inner_cartouche, 129 Markup.DYNAMIC_FACT -> Color.dynamic, 130 Markup.CLASS_PARAMETER -> Color.class_parameter, 131 Markup.ANTIQUOTE -> Color.antiquote, 132 Markup.RAW_TEXT -> Color.raw_text, 133 Markup.PLAIN_TEXT -> Color.plain_text, 134 Markup.ML_KEYWORD1 -> Color.keyword1, 135 Markup.ML_KEYWORD2 -> Color.keyword2, 136 Markup.ML_KEYWORD3 -> Color.keyword3, 137 Markup.ML_DELIMITER -> Color.main, 138 Markup.ML_NUMERAL -> Color.inner_numeral, 139 Markup.ML_CHAR -> Color.inner_quoted, 140 Markup.ML_STRING -> Color.inner_quoted, 141 Markup.ML_COMMENT -> Color.comment1, 142 Markup.COMMENT -> Color.comment1, 143 Markup.COMMENT1 -> Color.comment1, 144 Markup.COMMENT2 -> Color.comment2, 145 Markup.COMMENT3 -> Color.comment3) 146 147 val foreground = 148 Map( 149 Markup.STRING -> Color.quoted, 150 Markup.ALT_STRING -> Color.quoted, 151 Markup.VERBATIM -> Color.quoted, 152 Markup.CARTOUCHE -> Color.quoted, 153 Markup.ANTIQUOTED -> Color.antiquoted) 154 155 156 /* tooltips */ 157 158 val tooltip_descriptions = 159 Map( 160 Markup.CITATION -> "citation", 161 Markup.TOKEN_RANGE -> "inner syntax token", 162 Markup.FREE -> "free variable", 163 Markup.SKOLEM -> "skolem variable", 164 Markup.BOUND -> "bound variable", 165 Markup.VAR -> "schematic variable", 166 Markup.TFREE -> "free type variable", 167 Markup.TVAR -> "schematic type variable") 168 169 170 /* markup elements */ 171 172 val semantic_completion_elements = 173 Markup.Elements(Markup.COMPLETION, Markup.NO_COMPLETION) 174 175 val language_context_elements = 176 Markup.Elements(Markup.STRING, Markup.ALT_STRING, Markup.VERBATIM, 177 Markup.CARTOUCHE, Markup.COMMENT, Markup.LANGUAGE, 178 Markup.ML_STRING, Markup.ML_COMMENT) 179 180 val language_elements = Markup.Elements(Markup.LANGUAGE) 181 182 val citation_elements = Markup.Elements(Markup.CITATION) 183 184 val active_elements = 185 Markup.Elements(Markup.DIALOG, Markup.BROWSER, Markup.GRAPHVIEW, Markup.THEORY_EXPORTS, 186 Markup.SENDBACK, Markup.JEDIT_ACTION, Markup.SIMP_TRACE_PANEL) 187 188 val background_elements = 189 Document_Status.Command_Status.proper_elements + Markup.WRITELN_MESSAGE + 190 Markup.STATE_MESSAGE + Markup.INFORMATION_MESSAGE + 191 Markup.TRACING_MESSAGE + Markup.WARNING_MESSAGE + 192 Markup.LEGACY_MESSAGE + Markup.ERROR_MESSAGE + 193 Markup.BAD + Markup.INTENSIFY + Markup.ENTITY + 194 Markup.Markdown_Bullet.name ++ active_elements 195 196 val foreground_elements = Markup.Elements(foreground.keySet) 197 198 val text_color_elements = Markup.Elements(text_color.keySet) 199 200 val tooltip_elements = 201 Markup.Elements(Markup.LANGUAGE, Markup.EXPRESSION, Markup.TIMING, Markup.ENTITY, 202 Markup.SORTING, Markup.TYPING, Markup.CLASS_PARAMETER, Markup.ML_TYPING, 203 Markup.ML_BREAKPOINT, Markup.PATH, Markup.DOC, Markup.URL, 204 Markup.MARKDOWN_PARAGRAPH, Markup.MARKDOWN_ITEM, Markup.Markdown_List.name) ++ 205 Markup.Elements(tooltip_descriptions.keySet) 206 207 val tooltip_message_elements = 208 Markup.Elements(Markup.WRITELN, Markup.INFORMATION, Markup.WARNING, Markup.LEGACY, Markup.ERROR, 209 Markup.BAD) 210 211 val warning_elements = Markup.Elements(Markup.WARNING, Markup.LEGACY) 212 val error_elements = Markup.Elements(Markup.ERROR) 213 214 val caret_focus_elements = Markup.Elements(Markup.ENTITY) 215 216 val antiquoted_elements = Markup.Elements(Markup.ANTIQUOTED) 217 218 val meta_data_elements = 219 Markup.Elements(Markup.META_TITLE, Markup.META_CREATOR, Markup.META_CONTRIBUTOR, 220 Markup.META_DATE, Markup.META_DESCRIPTION, Markup.META_LICENSE) 221 222 val document_tag_elements = 223 Markup.Elements(Markup.Document_Tag.ELEMENT) 224 225 val markdown_elements = 226 Markup.Elements(Markup.MARKDOWN_PARAGRAPH, Markup.MARKDOWN_ITEM, Markup.Markdown_List.name, 227 Markup.Markdown_Bullet.name) 228} 229 230abstract class Rendering( 231 val snapshot: Document.Snapshot, 232 val options: Options, 233 val session: Session) 234{ 235 override def toString: String = "Rendering(" + snapshot.toString + ")" 236 237 def model: Document.Model 238 239 240 /* caret */ 241 242 def before_caret_range(caret: Text.Offset): Text.Range = 243 { 244 val former_caret = snapshot.revert(caret) 245 snapshot.convert(Text.Range(former_caret - 1, former_caret)) 246 } 247 248 249 /* completion */ 250 251 def semantic_completion(completed_range: Option[Text.Range], caret_range: Text.Range) 252 : Option[Text.Info[Completion.Semantic]] = 253 if (snapshot.is_outdated) None 254 else { 255 snapshot.select(caret_range, Rendering.semantic_completion_elements, _ => 256 { 257 case Completion.Semantic.Info(info) => 258 completed_range match { 259 case Some(range0) if range0.contains(info.range) && range0 != info.range => None 260 case _ => Some(info) 261 } 262 case _ => None 263 }).headOption.map(_.info) 264 } 265 266 def semantic_completion_result( 267 history: Completion.History, 268 unicode: Boolean, 269 completed_range: Option[Text.Range], 270 caret_range: Text.Range): (Boolean, Option[Completion.Result]) = 271 { 272 semantic_completion(completed_range, caret_range) match { 273 case Some(Text.Info(_, Completion.No_Completion)) => (true, None) 274 case Some(Text.Info(range, names: Completion.Names)) => 275 model.get_text(range) match { 276 case Some(original) => (false, names.complete(range, history, unicode, original)) 277 case None => (false, None) 278 } 279 case None => (false, None) 280 } 281 } 282 283 def language_context(range: Text.Range): Option[Completion.Language_Context] = 284 snapshot.select(range, Rendering.language_context_elements, _ => 285 { 286 case Text.Info(_, XML.Elem(Markup.Language(language, symbols, antiquotes, delimited), _)) => 287 if (delimited) Some(Completion.Language_Context(language, symbols, antiquotes)) 288 else None 289 case Text.Info(_, elem) 290 if elem.name == Markup.ML_STRING || elem.name == Markup.ML_COMMENT => 291 Some(Completion.Language_Context.ML_inner) 292 case Text.Info(_, _) => 293 Some(Completion.Language_Context.inner) 294 }).headOption.map(_.info) 295 296 def citation(range: Text.Range): Option[Text.Info[String]] = 297 snapshot.select(range, Rendering.citation_elements, _ => 298 { 299 case Text.Info(info_range, XML.Elem(Markup.Citation(name), _)) => 300 Some(Text.Info(snapshot.convert(info_range), name)) 301 case _ => None 302 }).headOption.map(_.info) 303 304 305 /* file-system path completion */ 306 307 def language_path(range: Text.Range): Option[Text.Range] = 308 snapshot.select(range, Rendering.language_elements, _ => 309 { 310 case Text.Info(info_range, XML.Elem(Markup.Language(Markup.Language.PATH, _, _, _), _)) => 311 Some(snapshot.convert(info_range)) 312 case _ => None 313 }).headOption.map(_.info) 314 315 def path_completion(caret: Text.Offset): Option[Completion.Result] = 316 { 317 def complete(text: String): List[(String, List[String])] = 318 { 319 try { 320 val path = Path.explode(text) 321 val (dir, base_name) = 322 if (text == "" || text.endsWith("/")) (path, "") 323 else (path.dir, path.file_name) 324 325 val directory = new JFile(session.resources.append(snapshot.node_name, dir)) 326 val files = directory.listFiles 327 if (files == null) Nil 328 else { 329 val ignore = 330 space_explode(':', options.string("completion_path_ignore")). 331 map(s => FileSystems.getDefault.getPathMatcher("glob:" + s)) 332 (for { 333 file <- files.iterator 334 335 name = file.getName 336 if name.startsWith(base_name) 337 path_name = new JFile(name).toPath 338 if !ignore.exists(matcher => matcher.matches(path_name)) 339 340 text1 = (dir + Path.basic(name)).implode_short 341 if text != text1 342 343 is_dir = new JFile(directory, name).isDirectory 344 replacement = text1 + (if (is_dir) "/" else "") 345 descr = List(text1, if (is_dir) "(directory)" else "(file)") 346 } yield (replacement, descr)).take(options.int("completion_limit")).toList 347 } 348 } 349 catch { case ERROR(_) => Nil } 350 } 351 352 def is_wrapped(s: String): Boolean = 353 s.startsWith("\"") && s.endsWith("\"") || 354 s.startsWith(Symbol.open_decoded) && s.endsWith(Symbol.close_decoded) 355 356 for { 357 r1 <- language_path(before_caret_range(caret)) 358 s1 <- model.get_text(r1) 359 if is_wrapped(s1) 360 r2 = Text.Range(r1.start + 1, r1.stop - 1) 361 s2 = s1.substring(1, s1.length - 1) 362 if Path.is_valid(s2) 363 paths = complete(s2) 364 if paths.nonEmpty 365 items = paths.map(p => Completion.Item(r2, s2, "", p._2, p._1, 0, false)) 366 } yield Completion.Result(r2, s2, false, items) 367 } 368 369 370 /* spell checker */ 371 372 private lazy val spell_checker_include = 373 Markup.Elements(space_explode(',', options.string("spell_checker_include")): _*) 374 375 private lazy val spell_checker_elements = 376 spell_checker_include ++ 377 Markup.Elements(space_explode(',', options.string("spell_checker_exclude")): _*) 378 379 def spell_checker(range: Text.Range): List[Text.Info[Text.Range]] = 380 { 381 val result = 382 snapshot.select(range, spell_checker_elements, _ => 383 { 384 case info => 385 Some( 386 if (spell_checker_include(info.info.name)) 387 Some(snapshot.convert(info.range)) 388 else None) 389 }) 390 for (Text.Info(range, Some(range1)) <- result) 391 yield Text.Info(range, range1) 392 } 393 394 def spell_checker_point(range: Text.Range): Option[Text.Range] = 395 spell_checker(range).headOption.map(_.info) 396 397 398 /* text background */ 399 400 def background(elements: Markup.Elements, range: Text.Range, focus: Set[Long]) 401 : List[Text.Info[Rendering.Color.Value]] = 402 { 403 for { 404 Text.Info(r, result) <- 405 snapshot.cumulate[(List[Markup], Option[Rendering.Color.Value])]( 406 range, (List(Markup.Empty), None), Rendering.background_elements, 407 command_states => 408 { 409 case (((markups, color), Text.Info(_, XML.Elem(markup, _)))) 410 if markups.nonEmpty && Document_Status.Command_Status.proper_elements(markup.name) => 411 Some((markup :: markups, color)) 412 case (_, Text.Info(_, XML.Elem(Markup(Markup.BAD, _), _))) => 413 Some((Nil, Some(Rendering.Color.bad))) 414 case (_, Text.Info(_, XML.Elem(Markup(Markup.INTENSIFY, _), _))) => 415 Some((Nil, Some(Rendering.Color.intensify))) 416 case (_, Text.Info(_, XML.Elem(Markup(Markup.ENTITY, props), _))) => 417 props match { 418 case Markup.Entity.Def(i) if focus(i) => Some((Nil, Some(Rendering.Color.entity))) 419 case Markup.Entity.Ref(i) if focus(i) => Some((Nil, Some(Rendering.Color.entity))) 420 case _ => None 421 } 422 case (_, Text.Info(_, XML.Elem(Markup.Markdown_Bullet(depth), _))) => 423 val color = 424 depth % 4 match { 425 case 1 => Rendering.Color.markdown_bullet1 426 case 2 => Rendering.Color.markdown_bullet2 427 case 3 => Rendering.Color.markdown_bullet3 428 case _ => Rendering.Color.markdown_bullet4 429 } 430 Some((Nil, Some(color))) 431 case (acc, Text.Info(_, Protocol.Dialog(_, serial, result))) => 432 command_states.collectFirst( 433 { case st if st.results.defined(serial) => st.results.get(serial).get }) match 434 { 435 case Some(Protocol.Dialog_Result(res)) if res == result => 436 Some((Nil, Some(Rendering.Color.active_result))) 437 case _ => 438 Some((Nil, Some(Rendering.Color.active))) 439 } 440 case (_, Text.Info(_, elem)) => 441 if (Rendering.active_elements(elem.name)) 442 Some((Nil, Some(Rendering.Color.active))) 443 else None 444 }) 445 color <- 446 (result match { 447 case (markups, opt_color) if markups.nonEmpty => 448 val status = Document_Status.Command_Status.make(markups.iterator) 449 if (status.is_unprocessed) Some(Rendering.Color.unprocessed1) 450 else if (status.is_running) Some(Rendering.Color.running1) 451 else if (status.is_canceled) Some(Rendering.Color.canceled) 452 else opt_color 453 case (_, opt_color) => opt_color 454 }) 455 } yield Text.Info(r, color) 456 } 457 458 459 /* text foreground */ 460 461 def foreground(range: Text.Range): List[Text.Info[Rendering.Color.Value]] = 462 snapshot.select(range, Rendering.foreground_elements, _ => 463 { 464 case info => Some(Rendering.foreground(info.info.name)) 465 }) 466 467 468 /* caret focus */ 469 470 private def entity_focus(range: Text.Range, 471 check: (Boolean, Long) => Boolean = (is_def: Boolean, i: Long) => is_def): Set[Long] = 472 { 473 val results = 474 snapshot.cumulate[Set[Long]](range, Set.empty, Rendering.caret_focus_elements, _ => 475 { 476 case (serials, Text.Info(_, XML.Elem(Markup(Markup.ENTITY, props), _))) => 477 props match { 478 case Markup.Entity.Def(i) if check(true, i) => Some(serials + i) 479 case Markup.Entity.Ref(i) if check(false, i) => Some(serials + i) 480 case _ => None 481 } 482 case _ => None 483 }) 484 (Set.empty[Long] /: results){ case (s1, Text.Info(_, s2)) => s1 ++ s2 } 485 } 486 487 def caret_focus(caret_range: Text.Range, visible_range: Text.Range): Set[Long] = 488 { 489 val focus_defs = entity_focus(caret_range) 490 if (focus_defs.nonEmpty) focus_defs 491 else { 492 val visible_defs = entity_focus(visible_range) 493 entity_focus(caret_range, (is_def: Boolean, i: Long) => !is_def && visible_defs.contains(i)) 494 } 495 } 496 497 def caret_focus_ranges(caret_range: Text.Range, visible_range: Text.Range): List[Text.Range] = 498 { 499 val focus = caret_focus(caret_range, visible_range) 500 if (focus.nonEmpty) { 501 val results = 502 snapshot.cumulate[Boolean](visible_range, false, Rendering.caret_focus_elements, _ => 503 { 504 case (_, Text.Info(_, XML.Elem(Markup(Markup.ENTITY, props), _))) => 505 props match { 506 case Markup.Entity.Def(i) if focus(i) => Some(true) 507 case Markup.Entity.Ref(i) if focus(i) => Some(true) 508 case _ => None 509 } 510 }) 511 for (info <- results if info.info) yield info.range 512 } 513 else Nil 514 } 515 516 517 /* message underline color */ 518 519 def message_underline_color(elements: Markup.Elements, range: Text.Range) 520 : List[Text.Info[Rendering.Color.Value]] = 521 { 522 val results = 523 snapshot.cumulate[Int](range, 0, elements, _ => 524 { 525 case (pri, Text.Info(_, elem)) => Some(pri max Rendering.message_pri(elem.name)) 526 }) 527 for { 528 Text.Info(r, pri) <- results 529 color <- Rendering.message_underline_color.get(pri) 530 } yield Text.Info(r, color) 531 } 532 533 534 /* tooltips */ 535 536 def timing_threshold: Double = 0.0 537 538 private sealed case class Tooltip_Info( 539 range: Text.Range, 540 timing: Timing = Timing.zero, 541 messages: List[Command.Results.Entry] = Nil, 542 rev_infos: List[(Boolean, XML.Tree)] = Nil) 543 { 544 def + (t: Timing): Tooltip_Info = copy(timing = timing + t) 545 def + (r0: Text.Range, serial: Long, tree: XML.Tree): Tooltip_Info = 546 { 547 val r = snapshot.convert(r0) 548 if (range == r) copy(messages = (serial -> tree) :: messages) 549 else copy(range = r, messages = List(serial -> tree)) 550 } 551 def + (r0: Text.Range, important: Boolean, tree: XML.Tree): Tooltip_Info = 552 { 553 val r = snapshot.convert(r0) 554 if (range == r) copy(rev_infos = (important -> tree) :: rev_infos) 555 else copy (range = r, rev_infos = List(important -> tree)) 556 } 557 558 def timing_info(tree: XML.Tree): Option[XML.Tree] = 559 tree match { 560 case XML.Elem(Markup(Markup.TIMING, _), _) => 561 if (timing.elapsed.seconds >= timing_threshold) Some(XML.Text(timing.message)) else None 562 case _ => Some(tree) 563 } 564 def infos(important: Boolean): List[XML.Tree] = 565 for { 566 (is_important, tree) <- rev_infos.reverse if is_important == important 567 tree1 <- timing_info(tree) 568 } yield tree1 569 } 570 571 def perhaps_append_file(node_name: Document.Node.Name, name: String): String = 572 if (Path.is_valid(name)) session.resources.append(node_name, Path.explode(name)) else name 573 574 def tooltips(elements: Markup.Elements, range: Text.Range): Option[Text.Info[List[XML.Tree]]] = 575 { 576 val results = 577 snapshot.cumulate[Tooltip_Info](range, Tooltip_Info(range), elements, command_states => 578 { 579 case (info, Text.Info(_, XML.Elem(Markup.Timing(t), _))) => Some(info + t) 580 581 case (info, Text.Info(r0, msg @ XML.Elem(Markup(Markup.BAD, Markup.Serial(i)), body))) 582 if body.nonEmpty => Some(info + (r0, i, msg)) 583 584 case (info, Text.Info(r0, XML.Elem(Markup(name, props), _))) 585 if Rendering.tooltip_message_elements(name) => 586 for ((i, tree) <- Command.State.get_result_proper(command_states, props)) 587 yield (info + (r0, i, tree)) 588 589 case (info, Text.Info(r0, XML.Elem(Markup.Entity(kind, name), _))) 590 if kind != "" && kind != Markup.ML_DEF => 591 val kind1 = Word.implode(Word.explode('_', kind)) 592 val txt1 = 593 if (name == "") kind1 594 else if (kind1 == "") quote(name) 595 else kind1 + " " + quote(name) 596 val info1 = info + (r0, true, XML.Text(txt1)) 597 Some(if (kind == Markup.COMMAND) info1 + (r0, true, XML.elem(Markup.TIMING)) else info1) 598 599 case (info, Text.Info(r0, XML.Elem(Markup.Path(name), _))) => 600 val file = perhaps_append_file(snapshot.node_name, name) 601 val text = 602 if (name == file) "file " + quote(file) 603 else "path " + quote(name) + "\nfile " + quote(file) 604 Some(info + (r0, true, XML.Text(text))) 605 606 case (info, Text.Info(r0, XML.Elem(Markup.Doc(name), _))) => 607 val text = "doc " + quote(name) 608 Some(info + (r0, true, XML.Text(text))) 609 610 case (info, Text.Info(r0, XML.Elem(Markup.Url(name), _))) => 611 Some(info + (r0, true, XML.Text("URL " + quote(name)))) 612 613 case (info, Text.Info(r0, XML.Elem(Markup(name, _), body))) 614 if name == Markup.SORTING || name == Markup.TYPING => 615 Some(info + (r0, true, Pretty.block(XML.Text("::") :: Pretty.brk(1) :: body))) 616 617 case (info, Text.Info(r0, XML.Elem(Markup(Markup.CLASS_PARAMETER, _), body))) => 618 Some(info + (r0, true, Pretty.block(0, body))) 619 620 case (info, Text.Info(r0, XML.Elem(Markup(Markup.ML_TYPING, _), body))) => 621 Some(info + (r0, false, Pretty.block(XML.Text("ML:") :: Pretty.brk(1) :: body))) 622 623 case (info, Text.Info(r0, Protocol.ML_Breakpoint(breakpoint))) => 624 val text = 625 if (session.debugger.breakpoint_state(breakpoint)) "breakpoint (enabled)" 626 else "breakpoint (disabled)" 627 Some(info + (r0, true, XML.Text(text))) 628 case (info, Text.Info(r0, XML.Elem(Markup.Language(language, _, _, _), _))) => 629 val lang = Word.implode(Word.explode('_', language)) 630 Some(info + (r0, true, XML.Text("language: " + lang))) 631 632 case (info, Text.Info(r0, XML.Elem(Markup.Expression(kind), _))) => 633 val descr = if (kind == "") "expression" else "expression: " + kind 634 Some(info + (r0, true, XML.Text(descr))) 635 636 case (info, Text.Info(r0, XML.Elem(Markup(Markup.MARKDOWN_PARAGRAPH, _), _))) => 637 Some(info + (r0, true, XML.Text("Markdown: paragraph"))) 638 case (info, Text.Info(r0, XML.Elem(Markup(Markup.MARKDOWN_ITEM, _), _))) => 639 Some(info + (r0, true, XML.Text("Markdown: item"))) 640 case (info, Text.Info(r0, XML.Elem(Markup.Markdown_List(kind), _))) => 641 Some(info + (r0, true, XML.Text("Markdown: " + kind))) 642 643 case (info, Text.Info(r0, XML.Elem(Markup(name, _), _))) => 644 Rendering.tooltip_descriptions.get(name).map(desc => info + (r0, true, XML.Text(desc))) 645 }).map(_.info) 646 647 if (results.isEmpty) None 648 else { 649 val r = Text.Range(results.head.range.start, results.last.range.stop) 650 val all_tips = 651 Command.Results.make(results.flatMap(_.messages)).iterator.map(_._2).toList ::: 652 results.flatMap(res => res.infos(true)) ::: 653 results.flatMap(res => res.infos(false)).lastOption.toList 654 if (all_tips.isEmpty) None else Some(Text.Info(r, all_tips)) 655 } 656 } 657 658 659 /* messages */ 660 661 def warnings(range: Text.Range): List[Text.Markup] = 662 snapshot.select(range, Rendering.warning_elements, _ => Some(_)).map(_.info) 663 664 def errors(range: Text.Range): List[Text.Markup] = 665 snapshot.select(range, Rendering.error_elements, _ => Some(_)).map(_.info) 666 667 668 /* command status overview */ 669 670 def overview_color(range: Text.Range): Option[Rendering.Color.Value] = 671 { 672 if (snapshot.is_outdated) None 673 else { 674 val results = 675 snapshot.cumulate[List[Markup]](range, Nil, Document_Status.Command_Status.liberal_elements, 676 _ => 677 { 678 case (status, Text.Info(_, elem)) => Some(elem.markup :: status) 679 }, status = true) 680 if (results.isEmpty) None 681 else { 682 val status = Document_Status.Command_Status.make(results.iterator.flatMap(_.info)) 683 684 if (status.is_running) Some(Rendering.Color.running) 685 else if (status.is_failed) Some(Rendering.Color.error) 686 else if (status.is_warned) Some(Rendering.Color.warning) 687 else if (status.is_unprocessed) Some(Rendering.Color.unprocessed) 688 else None 689 } 690 } 691 } 692 693 694 /* antiquoted text */ 695 696 def antiquoted(range: Text.Range): Option[Text.Range] = 697 snapshot.cumulate[Option[Text.Range]](range, None, Rendering.antiquoted_elements, _ => 698 { 699 case (res, info) => if (res.isEmpty) Some(Some(info.range)) else None 700 }).headOption.flatMap(_.info) 701 702 703 /* meta data */ 704 705 def meta_data(range: Text.Range): Properties.T = 706 { 707 val results = 708 snapshot.cumulate[Properties.T](range, Nil, Rendering.meta_data_elements, _ => 709 { 710 case (res, Text.Info(_, elem)) => 711 val plain_text = XML.content(elem) 712 Some((elem.name -> plain_text) :: res) 713 }) 714 Library.distinct(results.flatMap(_.info.reverse)) 715 } 716 717 718 /* document tags */ 719 720 def document_tags(range: Text.Range): List[String] = 721 { 722 val results = 723 snapshot.cumulate[List[String]](range, Nil, Rendering.document_tag_elements, _ => 724 { 725 case (res, Text.Info(_, XML.Elem(Markup.Document_Tag(name), _))) => Some(name :: res) 726 case _ => None 727 }) 728 Library.distinct(results.flatMap(_.info.reverse)) 729 } 730} 731