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