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