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