src/Pure/PIDE/rendering.scala
author wenzelm
Sat Sep 01 20:20:50 2018 +0200 (10 months ago)
changeset 68871 f5c76072db55
parent 68822 253f04c1e814
child 69320 fc221fa79741
permissions -rw-r--r--
more explicit status for "canceled" command within theory node;
     1 /*  Title:      Pure/PIDE/rendering.scala
     2     Author:     Makarius
     3 
     4 Isabelle-specific implementation of quasi-abstract rendering and
     5 markup interpretation.
     6 */
     7 
     8 package isabelle
     9 
    10 
    11 import java.io.{File => JFile}
    12 import java.nio.file.FileSystems
    13 
    14 
    15 object 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, 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 
   141   val foreground =
   142     Map(
   143       Markup.STRING -> Color.quoted,
   144       Markup.ALT_STRING -> Color.quoted,
   145       Markup.VERBATIM -> Color.quoted,
   146       Markup.CARTOUCHE -> Color.quoted,
   147       Markup.ANTIQUOTED -> Color.antiquoted)
   148 
   149 
   150   /* tooltips */
   151 
   152   val tooltip_descriptions =
   153     Map(
   154       Markup.CITATION -> "citation",
   155       Markup.TOKEN_RANGE -> "inner syntax token",
   156       Markup.FREE -> "free variable",
   157       Markup.SKOLEM -> "skolem variable",
   158       Markup.BOUND -> "bound variable",
   159       Markup.VAR -> "schematic variable",
   160       Markup.TFREE -> "free type variable",
   161       Markup.TVAR -> "schematic type variable")
   162 
   163 
   164   /* markup elements */
   165 
   166   val semantic_completion_elements =
   167     Markup.Elements(Markup.COMPLETION, Markup.NO_COMPLETION)
   168 
   169   val language_context_elements =
   170     Markup.Elements(Markup.STRING, Markup.ALT_STRING, Markup.VERBATIM,
   171       Markup.CARTOUCHE, Markup.COMMENT, Markup.LANGUAGE,
   172       Markup.ML_STRING, Markup.ML_COMMENT)
   173 
   174   val language_elements = Markup.Elements(Markup.LANGUAGE)
   175 
   176   val citation_elements = Markup.Elements(Markup.CITATION)
   177 
   178   val active_elements =
   179     Markup.Elements(Markup.DIALOG, Markup.BROWSER, Markup.GRAPHVIEW,
   180       Markup.SENDBACK, Markup.JEDIT_ACTION, Markup.SIMP_TRACE_PANEL)
   181 
   182   val background_elements =
   183     Document_Status.Command_Status.proper_elements + Markup.WRITELN_MESSAGE +
   184       Markup.STATE_MESSAGE + Markup.INFORMATION_MESSAGE +
   185       Markup.TRACING_MESSAGE + Markup.WARNING_MESSAGE +
   186       Markup.LEGACY_MESSAGE + Markup.ERROR_MESSAGE +
   187       Markup.BAD + Markup.INTENSIFY + Markup.ENTITY +
   188       Markup.Markdown_Bullet.name ++ active_elements
   189 
   190   val foreground_elements = Markup.Elements(foreground.keySet)
   191 
   192   val text_color_elements = Markup.Elements(text_color.keySet)
   193 
   194   val tooltip_elements =
   195     Markup.Elements(Markup.LANGUAGE, Markup.EXPRESSION, Markup.TIMING, Markup.ENTITY,
   196       Markup.SORTING, Markup.TYPING, Markup.CLASS_PARAMETER, Markup.ML_TYPING,
   197       Markup.ML_BREAKPOINT, Markup.PATH, Markup.DOC, Markup.URL, Markup.MARKDOWN_PARAGRAPH,
   198       Markup.MARKDOWN_ITEM, Markup.Markdown_List.name) ++
   199       Markup.Elements(tooltip_descriptions.keySet)
   200 
   201   val tooltip_message_elements =
   202     Markup.Elements(Markup.WRITELN, Markup.INFORMATION, Markup.WARNING, Markup.LEGACY, Markup.ERROR,
   203       Markup.BAD)
   204 
   205   val caret_focus_elements = Markup.Elements(Markup.ENTITY)
   206 
   207   val antiquoted_elements = Markup.Elements(Markup.ANTIQUOTED)
   208 
   209   val markdown_elements =
   210     Markup.Elements(Markup.MARKDOWN_PARAGRAPH, Markup.MARKDOWN_ITEM, Markup.Markdown_List.name,
   211       Markup.Markdown_Bullet.name)
   212 }
   213 
   214 abstract class Rendering(
   215   val snapshot: Document.Snapshot,
   216   val options: Options,
   217   val session: Session)
   218 {
   219   override def toString: String = "Rendering(" + snapshot.toString + ")"
   220 
   221   def model: Document.Model
   222 
   223 
   224   /* caret */
   225 
   226   def before_caret_range(caret: Text.Offset): Text.Range =
   227   {
   228     val former_caret = snapshot.revert(caret)
   229     snapshot.convert(Text.Range(former_caret - 1, former_caret))
   230   }
   231 
   232 
   233   /* completion */
   234 
   235   def semantic_completion(completed_range: Option[Text.Range], caret_range: Text.Range)
   236       : Option[Text.Info[Completion.Semantic]] =
   237     if (snapshot.is_outdated) None
   238     else {
   239       snapshot.select(caret_range, Rendering.semantic_completion_elements, _ =>
   240         {
   241           case Completion.Semantic.Info(info) =>
   242             completed_range match {
   243               case Some(range0) if range0.contains(info.range) && range0 != info.range => None
   244               case _ => Some(info)
   245             }
   246           case _ => None
   247         }).headOption.map(_.info)
   248     }
   249 
   250   def semantic_completion_result(
   251     history: Completion.History,
   252     unicode: Boolean,
   253     completed_range: Option[Text.Range],
   254     caret_range: Text.Range): (Boolean, Option[Completion.Result]) =
   255   {
   256     semantic_completion(completed_range, caret_range) match {
   257       case Some(Text.Info(_, Completion.No_Completion)) => (true, None)
   258       case Some(Text.Info(range, names: Completion.Names)) =>
   259         model.get_text(range) match {
   260           case Some(original) => (false, names.complete(range, history, unicode, original))
   261           case None => (false, None)
   262         }
   263       case None => (false, None)
   264     }
   265   }
   266 
   267   def language_context(range: Text.Range): Option[Completion.Language_Context] =
   268     snapshot.select(range, Rendering.language_context_elements, _ =>
   269       {
   270         case Text.Info(_, XML.Elem(Markup.Language(language, symbols, antiquotes, delimited), _)) =>
   271           if (delimited) Some(Completion.Language_Context(language, symbols, antiquotes))
   272           else None
   273         case Text.Info(_, elem)
   274         if elem.name == Markup.ML_STRING || elem.name == Markup.ML_COMMENT =>
   275           Some(Completion.Language_Context.ML_inner)
   276         case Text.Info(_, _) =>
   277           Some(Completion.Language_Context.inner)
   278       }).headOption.map(_.info)
   279 
   280   def citation(range: Text.Range): Option[Text.Info[String]] =
   281     snapshot.select(range, Rendering.citation_elements, _ =>
   282       {
   283         case Text.Info(info_range, XML.Elem(Markup.Citation(name), _)) =>
   284           Some(Text.Info(snapshot.convert(info_range), name))
   285         case _ => None
   286       }).headOption.map(_.info)
   287 
   288 
   289   /* file-system path completion */
   290 
   291   def language_path(range: Text.Range): Option[Text.Range] =
   292     snapshot.select(range, Rendering.language_elements, _ =>
   293       {
   294         case Text.Info(info_range, XML.Elem(Markup.Language(Markup.Language.PATH, _, _, _), _)) =>
   295           Some(snapshot.convert(info_range))
   296         case _ => None
   297       }).headOption.map(_.info)
   298 
   299   def path_completion(caret: Text.Offset): Option[Completion.Result] =
   300   {
   301     def complete(text: String): List[(String, List[String])] =
   302     {
   303       try {
   304         val path = Path.explode(text)
   305         val (dir, base_name) =
   306           if (text == "" || text.endsWith("/")) (path, "")
   307           else (path.dir, path.base_name)
   308 
   309         val directory = new JFile(session.resources.append(snapshot.node_name, dir))
   310         val files = directory.listFiles
   311         if (files == null) Nil
   312         else {
   313           val ignore =
   314             space_explode(':', options.string("completion_path_ignore")).
   315               map(s => FileSystems.getDefault.getPathMatcher("glob:" + s))
   316           (for {
   317             file <- files.iterator
   318 
   319             name = file.getName
   320             if name.startsWith(base_name)
   321             path_name = new JFile(name).toPath
   322             if !ignore.exists(matcher => matcher.matches(path_name))
   323 
   324             text1 = (dir + Path.basic(name)).implode_short
   325             if text != text1
   326 
   327             is_dir = new JFile(directory, name).isDirectory
   328             replacement = text1 + (if (is_dir) "/" else "")
   329             descr = List(text1, if (is_dir) "(directory)" else "(file)")
   330           } yield (replacement, descr)).take(options.int("completion_limit")).toList
   331         }
   332       }
   333       catch { case ERROR(_) => Nil }
   334     }
   335 
   336     def is_wrapped(s: String): Boolean =
   337       s.startsWith("\"") && s.endsWith("\"") ||
   338       s.startsWith(Symbol.open_decoded) && s.endsWith(Symbol.close_decoded)
   339 
   340     for {
   341       r1 <- language_path(before_caret_range(caret))
   342       s1 <- model.get_text(r1)
   343       if is_wrapped(s1)
   344       r2 = Text.Range(r1.start + 1, r1.stop - 1)
   345       s2 = s1.substring(1, s1.length - 1)
   346       if Path.is_valid(s2)
   347       paths = complete(s2)
   348       if paths.nonEmpty
   349       items = paths.map(p => Completion.Item(r2, s2, "", p._2, p._1, 0, false))
   350     } yield Completion.Result(r2, s2, false, items)
   351   }
   352 
   353 
   354   /* spell checker */
   355 
   356   private lazy val spell_checker_include =
   357     Markup.Elements(space_explode(',', options.string("spell_checker_include")): _*)
   358 
   359   private lazy val spell_checker_elements =
   360     spell_checker_include ++
   361       Markup.Elements(space_explode(',', options.string("spell_checker_exclude")): _*)
   362 
   363   def spell_checker(range: Text.Range): List[Text.Info[Text.Range]] =
   364   {
   365     val result =
   366       snapshot.select(range, spell_checker_elements, _ =>
   367         {
   368           case info =>
   369             Some(
   370               if (spell_checker_include(info.info.name))
   371                 Some(snapshot.convert(info.range))
   372               else None)
   373         })
   374     for (Text.Info(range, Some(range1)) <- result)
   375       yield Text.Info(range, range1)
   376   }
   377 
   378   def spell_checker_point(range: Text.Range): Option[Text.Range] =
   379     spell_checker(range).headOption.map(_.info)
   380 
   381 
   382   /* text background */
   383 
   384   def background(elements: Markup.Elements, range: Text.Range, focus: Set[Long])
   385     : List[Text.Info[Rendering.Color.Value]] =
   386   {
   387     for {
   388       Text.Info(r, result) <-
   389         snapshot.cumulate[(List[Markup], Option[Rendering.Color.Value])](
   390           range, (List(Markup.Empty), None), Rendering.background_elements,
   391           command_states =>
   392             {
   393               case (((markups, color), Text.Info(_, XML.Elem(markup, _))))
   394               if markups.nonEmpty && Document_Status.Command_Status.proper_elements(markup.name) =>
   395                 Some((markup :: markups, color))
   396               case (_, Text.Info(_, XML.Elem(Markup(Markup.BAD, _), _))) =>
   397                 Some((Nil, Some(Rendering.Color.bad)))
   398               case (_, Text.Info(_, XML.Elem(Markup(Markup.INTENSIFY, _), _))) =>
   399                 Some((Nil, Some(Rendering.Color.intensify)))
   400               case (_, Text.Info(_, XML.Elem(Markup(Markup.ENTITY, props), _))) =>
   401                 props match {
   402                   case Markup.Entity.Def(i) if focus(i) => Some((Nil, Some(Rendering.Color.entity)))
   403                   case Markup.Entity.Ref(i) if focus(i) => Some((Nil, Some(Rendering.Color.entity)))
   404                   case _ => None
   405                 }
   406               case (_, Text.Info(_, XML.Elem(Markup.Markdown_Bullet(depth), _))) =>
   407                 val color =
   408                   depth % 4 match {
   409                     case 1 => Rendering.Color.markdown_bullet1
   410                     case 2 => Rendering.Color.markdown_bullet2
   411                     case 3 => Rendering.Color.markdown_bullet3
   412                     case _ => Rendering.Color.markdown_bullet4
   413                   }
   414                 Some((Nil, Some(color)))
   415               case (acc, Text.Info(_, Protocol.Dialog(_, serial, result))) =>
   416                 command_states.collectFirst(
   417                   { case st if st.results.defined(serial) => st.results.get(serial).get }) match
   418                 {
   419                   case Some(Protocol.Dialog_Result(res)) if res == result =>
   420                     Some((Nil, Some(Rendering.Color.active_result)))
   421                   case _ =>
   422                     Some((Nil, Some(Rendering.Color.active)))
   423                 }
   424               case (_, Text.Info(_, elem)) =>
   425                 if (Rendering.active_elements(elem.name))
   426                   Some((Nil, Some(Rendering.Color.active)))
   427                 else None
   428             })
   429       color <-
   430         (result match {
   431           case (markups, opt_color) if markups.nonEmpty =>
   432             val status = Document_Status.Command_Status.make(markups.iterator)
   433             if (status.is_unprocessed) Some(Rendering.Color.unprocessed1)
   434             else if (status.is_running) Some(Rendering.Color.running1)
   435             else if (status.is_canceled) Some(Rendering.Color.canceled)
   436             else opt_color
   437           case (_, opt_color) => opt_color
   438         })
   439     } yield Text.Info(r, color)
   440   }
   441 
   442 
   443   /* text foreground */
   444 
   445   def foreground(range: Text.Range): List[Text.Info[Rendering.Color.Value]] =
   446     snapshot.select(range, Rendering.foreground_elements, _ =>
   447       {
   448         case info => Some(Rendering.foreground(info.info.name))
   449       })
   450 
   451 
   452   /* caret focus */
   453 
   454   private def entity_focus(range: Text.Range,
   455     check: (Boolean, Long) => Boolean = (is_def: Boolean, i: Long) => is_def): Set[Long] =
   456   {
   457     val results =
   458       snapshot.cumulate[Set[Long]](range, Set.empty, Rendering.caret_focus_elements, _ =>
   459           {
   460             case (serials, Text.Info(_, XML.Elem(Markup(Markup.ENTITY, props), _))) =>
   461               props match {
   462                 case Markup.Entity.Def(i) if check(true, i) => Some(serials + i)
   463                 case Markup.Entity.Ref(i) if check(false, i) => Some(serials + i)
   464                 case _ => None
   465               }
   466             case _ => None
   467           })
   468     (Set.empty[Long] /: results){ case (s1, Text.Info(_, s2)) => s1 ++ s2 }
   469   }
   470 
   471   def caret_focus(caret_range: Text.Range, visible_range: Text.Range): Set[Long] =
   472   {
   473     val focus_defs = entity_focus(caret_range)
   474     if (focus_defs.nonEmpty) focus_defs
   475     else {
   476       val visible_defs = entity_focus(visible_range)
   477       entity_focus(caret_range, (is_def: Boolean, i: Long) => !is_def && visible_defs.contains(i))
   478     }
   479   }
   480 
   481   def caret_focus_ranges(caret_range: Text.Range, visible_range: Text.Range): List[Text.Range] =
   482   {
   483     val focus = caret_focus(caret_range, visible_range)
   484     if (focus.nonEmpty) {
   485       val results =
   486         snapshot.cumulate[Boolean](visible_range, false, Rendering.caret_focus_elements, _ =>
   487           {
   488             case (_, Text.Info(_, XML.Elem(Markup(Markup.ENTITY, props), _))) =>
   489               props match {
   490                 case Markup.Entity.Def(i) if focus(i) => Some(true)
   491                 case Markup.Entity.Ref(i) if focus(i) => Some(true)
   492                 case _ => None
   493               }
   494           })
   495       for (info <- results if info.info) yield info.range
   496     }
   497     else Nil
   498   }
   499 
   500 
   501   /* message underline color */
   502 
   503   def message_underline_color(elements: Markup.Elements, range: Text.Range)
   504     : List[Text.Info[Rendering.Color.Value]] =
   505   {
   506     val results =
   507       snapshot.cumulate[Int](range, 0, elements, _ =>
   508         {
   509           case (pri, Text.Info(_, elem)) => Some(pri max Rendering.message_pri(elem.name))
   510         })
   511     for {
   512       Text.Info(r, pri) <- results
   513       color <- Rendering.message_underline_color.get(pri)
   514     } yield Text.Info(r, color)
   515   }
   516 
   517 
   518   /* tooltips */
   519 
   520   def timing_threshold: Double
   521 
   522   private sealed case class Tooltip_Info(
   523     range: Text.Range,
   524     timing: Timing = Timing.zero,
   525     messages: List[Command.Results.Entry] = Nil,
   526     rev_infos: List[(Boolean, XML.Tree)] = Nil)
   527   {
   528     def + (t: Timing): Tooltip_Info = copy(timing = timing + t)
   529     def + (r0: Text.Range, serial: Long, tree: XML.Tree): Tooltip_Info =
   530     {
   531       val r = snapshot.convert(r0)
   532       if (range == r) copy(messages = (serial -> tree) :: messages)
   533       else copy(range = r, messages = List(serial -> tree))
   534     }
   535     def + (r0: Text.Range, important: Boolean, tree: XML.Tree): Tooltip_Info =
   536     {
   537       val r = snapshot.convert(r0)
   538       if (range == r) copy(rev_infos = (important -> tree) :: rev_infos)
   539       else copy (range = r, rev_infos = List(important -> tree))
   540     }
   541 
   542     def timing_info(tree: XML.Tree): Option[XML.Tree] =
   543       tree match {
   544         case XML.Elem(Markup(Markup.TIMING, _), _) =>
   545           if (timing.elapsed.seconds >= timing_threshold) Some(XML.Text(timing.message)) else None
   546         case _ => Some(tree)
   547       }
   548     def infos(important: Boolean): List[XML.Tree] =
   549       for {
   550         (is_important, tree) <- rev_infos.reverse if is_important == important
   551         tree1 <- timing_info(tree)
   552       } yield tree1
   553   }
   554 
   555   def perhaps_append_file(node_name: Document.Node.Name, name: String): String =
   556     if (Path.is_valid(name)) session.resources.append(node_name, Path.explode(name)) else name
   557 
   558   def tooltips(elements: Markup.Elements, range: Text.Range): Option[Text.Info[List[XML.Tree]]] =
   559   {
   560     val results =
   561       snapshot.cumulate[Tooltip_Info](range, Tooltip_Info(range), elements, command_states =>
   562         {
   563           case (info, Text.Info(_, XML.Elem(Markup.Timing(t), _))) => Some(info + t)
   564 
   565           case (info, Text.Info(r0, msg @ XML.Elem(Markup(Markup.BAD, Markup.Serial(i)), body)))
   566           if body.nonEmpty => Some(info + (r0, i, msg))
   567 
   568           case (info, Text.Info(r0, XML.Elem(Markup(name, props), _)))
   569           if Rendering.tooltip_message_elements(name) =>
   570             for ((i, tree) <- Command.State.get_result_proper(command_states, props))
   571             yield (info + (r0, i, tree))
   572 
   573           case (info, Text.Info(r0, XML.Elem(Markup.Entity(kind, name), _)))
   574           if kind != "" && kind != Markup.ML_DEF =>
   575             val kind1 = Word.implode(Word.explode('_', kind))
   576             val txt1 =
   577               if (name == "") kind1
   578               else if (kind1 == "") quote(name)
   579               else kind1 + " " + quote(name)
   580             val info1 = info + (r0, true, XML.Text(txt1))
   581             Some(if (kind == Markup.COMMAND) info1 + (r0, true, XML.elem(Markup.TIMING)) else info1)
   582 
   583           case (info, Text.Info(r0, XML.Elem(Markup.Path(name), _))) =>
   584             val file = perhaps_append_file(snapshot.node_name, name)
   585             val text =
   586               if (name == file) "file " + quote(file)
   587               else "path " + quote(name) + "\nfile " + quote(file)
   588             Some(info + (r0, true, XML.Text(text)))
   589 
   590           case (info, Text.Info(r0, XML.Elem(Markup.Doc(name), _))) =>
   591             val text = "doc " + quote(name)
   592             Some(info + (r0, true, XML.Text(text)))
   593 
   594           case (info, Text.Info(r0, XML.Elem(Markup.Url(name), _))) =>
   595             Some(info + (r0, true, XML.Text("URL " + quote(name))))
   596 
   597           case (info, Text.Info(r0, XML.Elem(Markup(name, _), body)))
   598           if name == Markup.SORTING || name == Markup.TYPING =>
   599             Some(info + (r0, true, Pretty.block(XML.Text("::") :: Pretty.brk(1) :: body)))
   600 
   601           case (info, Text.Info(r0, XML.Elem(Markup(Markup.CLASS_PARAMETER, _), body))) =>
   602             Some(info + (r0, true, Pretty.block(0, body)))
   603 
   604           case (info, Text.Info(r0, XML.Elem(Markup(Markup.ML_TYPING, _), body))) =>
   605             Some(info + (r0, false, Pretty.block(XML.Text("ML:") :: Pretty.brk(1) :: body)))
   606 
   607           case (info, Text.Info(r0, Protocol.ML_Breakpoint(breakpoint))) =>
   608               val text =
   609                 if (session.debugger.breakpoint_state(breakpoint)) "breakpoint (enabled)"
   610                 else "breakpoint (disabled)"
   611               Some(info + (r0, true, XML.Text(text)))
   612           case (info, Text.Info(r0, XML.Elem(Markup.Language(language, _, _, _), _))) =>
   613             val lang = Word.implode(Word.explode('_', language))
   614             Some(info + (r0, true, XML.Text("language: " + lang)))
   615 
   616           case (info, Text.Info(r0, XML.Elem(Markup.Expression(kind), _))) =>
   617             val descr = if (kind == "") "expression" else "expression: " + kind
   618             Some(info + (r0, true, XML.Text(descr)))
   619 
   620           case (info, Text.Info(r0, XML.Elem(Markup(Markup.MARKDOWN_PARAGRAPH, _), _))) =>
   621             Some(info + (r0, true, XML.Text("Markdown: paragraph")))
   622           case (info, Text.Info(r0, XML.Elem(Markup(Markup.MARKDOWN_ITEM, _), _))) =>
   623             Some(info + (r0, true, XML.Text("Markdown: item")))
   624           case (info, Text.Info(r0, XML.Elem(Markup.Markdown_List(kind), _))) =>
   625             Some(info + (r0, true, XML.Text("Markdown: " + kind)))
   626 
   627           case (info, Text.Info(r0, XML.Elem(Markup(name, _), _))) =>
   628             Rendering.tooltip_descriptions.get(name).map(desc => info + (r0, true, XML.Text(desc)))
   629         }).map(_.info)
   630 
   631     if (results.isEmpty) None
   632     else {
   633       val r = Text.Range(results.head.range.start, results.last.range.stop)
   634       val all_tips =
   635         Command.Results.make(results.flatMap(_.messages)).iterator.map(_._2).toList :::
   636         results.flatMap(res => res.infos(true)) :::
   637         results.flatMap(res => res.infos(false)).lastOption.toList
   638       if (all_tips.isEmpty) None else Some(Text.Info(r, all_tips))
   639     }
   640   }
   641 
   642 
   643   /* command status overview */
   644 
   645   def overview_color(range: Text.Range): Option[Rendering.Color.Value] =
   646   {
   647     if (snapshot.is_outdated) None
   648     else {
   649       val results =
   650         snapshot.cumulate[List[Markup]](range, Nil, Document_Status.Command_Status.liberal_elements,
   651           _ =>
   652             {
   653               case (status, Text.Info(_, elem)) => Some(elem.markup :: status)
   654             }, status = true)
   655       if (results.isEmpty) None
   656       else {
   657         val status = Document_Status.Command_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 }