src/Tools/jEdit/src/rendering.scala
author wenzelm
Sun Oct 05 17:58:36 2014 +0200 (2014-10-05 ago)
changeset 58545 30b75b7958d6
parent 58464 5e7fc9974aba
child 58592 b0fff34d3247
permissions -rw-r--r--
citation tooltip/hyperlink based on open buffers with .bib files;
     1 /*  Title:      Tools/jEdit/src/rendering.scala
     2     Author:     Makarius
     3 
     4 Isabelle-specific implementation of quasi-abstract rendering and
     5 markup interpretation.
     6 */
     7 
     8 package isabelle.jedit
     9 
    10 
    11 import isabelle._
    12 
    13 import java.awt.Color
    14 import javax.swing.Icon
    15 
    16 import org.gjt.sp.jedit.syntax.{Token => JEditToken}
    17 import org.gjt.sp.jedit.{jEdit, View}
    18 
    19 import scala.collection.immutable.SortedMap
    20 
    21 
    22 object Rendering
    23 {
    24   def apply(snapshot: Document.Snapshot, options: Options): Rendering =
    25     new Rendering(snapshot, options)
    26 
    27 
    28   /* message priorities */
    29 
    30   private val writeln_pri = 1
    31   private val information_pri = 2
    32   private val tracing_pri = 3
    33   private val warning_pri = 4
    34   private val legacy_pri = 5
    35   private val error_pri = 6
    36 
    37   private val message_pri = Map(
    38     Markup.WRITELN -> writeln_pri, Markup.WRITELN_MESSAGE -> writeln_pri,
    39     Markup.TRACING -> tracing_pri, Markup.TRACING_MESSAGE -> tracing_pri,
    40     Markup.WARNING -> warning_pri, Markup.WARNING_MESSAGE -> warning_pri,
    41     Markup.ERROR -> error_pri, Markup.ERROR_MESSAGE -> error_pri)
    42 
    43 
    44   /* popup window bounds */
    45 
    46   def popup_bounds: Double = (PIDE.options.real("jedit_popup_bounds") max 0.2) min 0.8
    47 
    48 
    49   /* Isabelle/Isar token markup */
    50 
    51   private val command_style: Map[String, Byte] =
    52   {
    53     import JEditToken._
    54     Map[String, Byte](
    55       Keyword.THY_END -> KEYWORD2,
    56       Keyword.QED_SCRIPT -> DIGIT,
    57       Keyword.PRF_SCRIPT -> DIGIT,
    58       Keyword.PRF_ASM -> KEYWORD3,
    59       Keyword.PRF_ASM_GOAL -> KEYWORD3,
    60       Keyword.PRF_ASM_GOAL_SCRIPT -> DIGIT
    61     ).withDefaultValue(KEYWORD1)
    62   }
    63 
    64   private val token_style: Map[Token.Kind.Value, Byte] =
    65   {
    66     import JEditToken._
    67     Map[Token.Kind.Value, Byte](
    68       Token.Kind.KEYWORD -> KEYWORD2,
    69       Token.Kind.IDENT -> NULL,
    70       Token.Kind.LONG_IDENT -> NULL,
    71       Token.Kind.SYM_IDENT -> NULL,
    72       Token.Kind.VAR -> NULL,
    73       Token.Kind.TYPE_IDENT -> NULL,
    74       Token.Kind.TYPE_VAR -> NULL,
    75       Token.Kind.NAT -> NULL,
    76       Token.Kind.FLOAT -> NULL,
    77       Token.Kind.STRING -> LITERAL1,
    78       Token.Kind.ALT_STRING -> LITERAL2,
    79       Token.Kind.VERBATIM -> COMMENT3,
    80       Token.Kind.CARTOUCHE -> COMMENT4,
    81       Token.Kind.SPACE -> NULL,
    82       Token.Kind.COMMENT -> COMMENT1,
    83       Token.Kind.ERROR -> INVALID
    84     ).withDefaultValue(NULL)
    85   }
    86 
    87   def token_markup(syntax: Outer_Syntax, token: Token): Byte =
    88     if (token.is_command) command_style(syntax.keyword_kind(token.content).getOrElse(""))
    89     else if (token.is_delimiter) JEditToken.OPERATOR
    90     else token_style(token.kind)
    91 
    92 
    93   /* Isabelle/ML token markup */
    94 
    95   private val ml_token_style: Map[ML_Lex.Kind.Value, Byte] =
    96   {
    97     import JEditToken._
    98     Map[ML_Lex.Kind.Value, Byte](
    99       ML_Lex.Kind.KEYWORD -> NULL,
   100       ML_Lex.Kind.IDENT -> NULL,
   101       ML_Lex.Kind.LONG_IDENT -> NULL,
   102       ML_Lex.Kind.TYPE_VAR -> NULL,
   103       ML_Lex.Kind.WORD -> DIGIT,
   104       ML_Lex.Kind.INT -> DIGIT,
   105       ML_Lex.Kind.REAL -> DIGIT,
   106       ML_Lex.Kind.CHAR -> LITERAL2,
   107       ML_Lex.Kind.STRING -> LITERAL1,
   108       ML_Lex.Kind.SPACE -> NULL,
   109       ML_Lex.Kind.COMMENT -> COMMENT1,
   110       ML_Lex.Kind.ANTIQ -> NULL,
   111       ML_Lex.Kind.ANTIQ_START -> LITERAL4,
   112       ML_Lex.Kind.ANTIQ_STOP -> LITERAL4,
   113       ML_Lex.Kind.ANTIQ_OTHER -> NULL,
   114       ML_Lex.Kind.ANTIQ_STRING -> NULL,
   115       ML_Lex.Kind.ANTIQ_ALT_STRING -> NULL,
   116       ML_Lex.Kind.ANTIQ_CARTOUCHE -> NULL,
   117       ML_Lex.Kind.ERROR -> INVALID
   118     ).withDefaultValue(NULL)
   119   }
   120 
   121   def ml_token_markup(token: ML_Lex.Token): Byte =
   122     if (!token.is_keyword) ml_token_style(token.kind)
   123     else if (token.is_delimiter) JEditToken.OPERATOR
   124     else if (ML_Lex.keywords2(token.source)) JEditToken.KEYWORD2
   125     else if (ML_Lex.keywords3(token.source)) JEditToken.KEYWORD3
   126     else JEditToken.KEYWORD1
   127 
   128 
   129   /* markup elements */
   130 
   131   private val semantic_completion_elements =
   132     Markup.Elements(Markup.COMPLETION, Markup.NO_COMPLETION)
   133 
   134   private val language_context_elements =
   135     Markup.Elements(Markup.STRING, Markup.ALTSTRING, Markup.VERBATIM,
   136       Markup.CARTOUCHE, Markup.COMMENT, Markup.LANGUAGE,
   137       Markup.ML_STRING, Markup.ML_COMMENT)
   138 
   139   private val language_elements = Markup.Elements(Markup.LANGUAGE)
   140 
   141   private val highlight_elements =
   142     Markup.Elements(Markup.EXPRESSION, Markup.CITATION, Markup.LANGUAGE, Markup.ML_TYPING,
   143       Markup.TOKEN_RANGE, Markup.ENTITY, Markup.PATH, Markup.URL, Markup.SORTING,
   144       Markup.TYPING, Markup.FREE, Markup.SKOLEM, Markup.BOUND,
   145       Markup.VAR, Markup.TFREE, Markup.TVAR)
   146 
   147   private val hyperlink_elements =
   148     Markup.Elements(Markup.ENTITY, Markup.PATH, Markup.POSITION, Markup.CITATION, Markup.URL)
   149 
   150   private val active_elements =
   151     Markup.Elements(Markup.DIALOG, Markup.BROWSER, Markup.GRAPHVIEW,
   152       Markup.SENDBACK, Markup.SIMP_TRACE_PANEL)
   153 
   154   private val tooltip_message_elements =
   155     Markup.Elements(Markup.WRITELN, Markup.WARNING, Markup.ERROR, Markup.BAD)
   156 
   157   private val tooltip_descriptions =
   158     Map(
   159       Markup.EXPRESSION -> "expression",
   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   private val tooltip_elements =
   170     Markup.Elements(Markup.LANGUAGE, Markup.TIMING, Markup.ENTITY, Markup.SORTING,
   171       Markup.TYPING, Markup.ML_TYPING, Markup.PATH, Markup.URL) ++
   172     Markup.Elements(tooltip_descriptions.keySet)
   173 
   174   private val gutter_elements =
   175     Markup.Elements(Markup.WRITELN, Markup.WARNING, Markup.ERROR)
   176 
   177   private val squiggly_elements =
   178     Markup.Elements(Markup.WRITELN, Markup.WARNING, Markup.ERROR)
   179 
   180   private val line_background_elements =
   181     Markup.Elements(Markup.WRITELN_MESSAGE, Markup.TRACING_MESSAGE,
   182       Markup.WARNING_MESSAGE, Markup.ERROR_MESSAGE,
   183       Markup.INFORMATION)
   184 
   185   private val separator_elements =
   186     Markup.Elements(Markup.SEPARATOR)
   187 
   188   private val background_elements =
   189     Protocol.proper_status_elements + Markup.WRITELN_MESSAGE +
   190       Markup.TRACING_MESSAGE + Markup.WARNING_MESSAGE +
   191       Markup.ERROR_MESSAGE + Markup.BAD + Markup.INTENSIFY ++
   192       active_elements
   193 
   194   private val foreground_elements =
   195     Markup.Elements(Markup.STRING, Markup.ALTSTRING, Markup.VERBATIM,
   196       Markup.CARTOUCHE, Markup.ANTIQUOTED)
   197 
   198   private val bullet_elements =
   199     Markup.Elements(Markup.BULLET)
   200 
   201   private val fold_depth_elements =
   202     Markup.Elements(Markup.TEXT_FOLD, Markup.GOAL, Markup.SUBGOAL)
   203 }
   204 
   205 
   206 class Rendering private(val snapshot: Document.Snapshot, val options: Options)
   207 {
   208   override def toString: String = "Rendering(" + snapshot.toString + ")"
   209 
   210 
   211   /* colors */
   212 
   213   def color_value(s: String): Color = Color_Value(options.string(s))
   214 
   215   val outdated_color = color_value("outdated_color")
   216   val unprocessed_color = color_value("unprocessed_color")
   217   val unprocessed1_color = color_value("unprocessed1_color")
   218   val running_color = color_value("running_color")
   219   val running1_color = color_value("running1_color")
   220   val bullet_color = color_value("bullet_color")
   221   val tooltip_color = color_value("tooltip_color")
   222   val writeln_color = color_value("writeln_color")
   223   val information_color = color_value("information_color")
   224   val warning_color = color_value("warning_color")
   225   val error_color = color_value("error_color")
   226   val error1_color = color_value("error1_color")
   227   val writeln_message_color = color_value("writeln_message_color")
   228   val information_message_color = color_value("information_message_color")
   229   val tracing_message_color = color_value("tracing_message_color")
   230   val warning_message_color = color_value("warning_message_color")
   231   val error_message_color = color_value("error_message_color")
   232   val spell_checker_color = color_value("spell_checker_color")
   233   val bad_color = color_value("bad_color")
   234   val intensify_color = color_value("intensify_color")
   235   val quoted_color = color_value("quoted_color")
   236   val antiquoted_color = color_value("antiquoted_color")
   237   val antiquote_color = color_value("antiquote_color")
   238   val highlight_color = color_value("highlight_color")
   239   val hyperlink_color = color_value("hyperlink_color")
   240   val active_color = color_value("active_color")
   241   val active_hover_color = color_value("active_hover_color")
   242   val active_result_color = color_value("active_result_color")
   243   val keyword1_color = color_value("keyword1_color")
   244   val keyword2_color = color_value("keyword2_color")
   245   val keyword3_color = color_value("keyword3_color")
   246   val quasi_keyword_color = color_value("quasi_keyword_color")
   247   val improper_color = color_value("improper_color")
   248   val operator_color = color_value("operator_color")
   249   val caret_invisible_color = color_value("caret_invisible_color")
   250   val completion_color = color_value("completion_color")
   251   val search_color = color_value("search_color")
   252 
   253   val tfree_color = color_value("tfree_color")
   254   val tvar_color = color_value("tvar_color")
   255   val free_color = color_value("free_color")
   256   val skolem_color = color_value("skolem_color")
   257   val bound_color = color_value("bound_color")
   258   val var_color = color_value("var_color")
   259   val inner_numeral_color = color_value("inner_numeral_color")
   260   val inner_quoted_color = color_value("inner_quoted_color")
   261   val inner_cartouche_color = color_value("inner_cartouche_color")
   262   val inner_comment_color = color_value("inner_comment_color")
   263   val dynamic_color = color_value("dynamic_color")
   264 
   265 
   266   /* completion */
   267 
   268   def semantic_completion(range: Text.Range): Option[Text.Info[Completion.Semantic]] =
   269     if (snapshot.is_outdated) None
   270     else {
   271       snapshot.select(range, Rendering.semantic_completion_elements, _ =>
   272         {
   273           case Completion.Semantic.Info(info) => Some(info)
   274           case _ => None
   275         }).headOption.map(_.info)
   276     }
   277 
   278   def language_context(range: Text.Range): Option[Completion.Language_Context] =
   279     snapshot.select(range, Rendering.language_context_elements, _ =>
   280       {
   281         case Text.Info(_, XML.Elem(Markup.Language(language, symbols, antiquotes, delimited), _)) =>
   282           if (delimited) Some(Completion.Language_Context(language, symbols, antiquotes))
   283           else None
   284         case Text.Info(_, elem)
   285         if elem.name == Markup.ML_STRING || elem.name == Markup.ML_COMMENT =>
   286           Some(Completion.Language_Context.ML_inner)
   287         case Text.Info(_, _) =>
   288           Some(Completion.Language_Context.inner)
   289       }).headOption.map(_.info)
   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 
   300   /* spell checker */
   301 
   302   private lazy val spell_checker_elements =
   303     Markup.Elements(space_explode(',', options.string("spell_checker_elements")): _*)
   304 
   305   def spell_checker_ranges(range: Text.Range): List[Text.Range] =
   306     snapshot.select(range, spell_checker_elements, _ => _ => Some(())).map(_.range)
   307 
   308   def spell_checker_point(range: Text.Range): Option[Text.Range] =
   309     snapshot.select(range, spell_checker_elements, _ =>
   310       {
   311         case info => Some(snapshot.convert(info.range))
   312       }).headOption.map(_.info)
   313 
   314 
   315   /* command status overview */
   316 
   317   def overview_limit: Int = options.int("jedit_text_overview_limit")
   318 
   319   def overview_color(range: Text.Range): Option[Color] =
   320   {
   321     if (snapshot.is_outdated) None
   322     else {
   323       val results =
   324         snapshot.cumulate[List[Markup]](range, Nil, Protocol.liberal_status_elements, _ =>
   325           {
   326             case (status, Text.Info(_, elem)) => Some(elem.markup :: status)
   327           }, status = true)
   328       if (results.isEmpty) None
   329       else {
   330         val status = Protocol.Status.make(results.iterator.flatMap(_.info))
   331 
   332         if (status.is_running) Some(running_color)
   333         else if (status.is_failed) Some(error_color)
   334         else if (status.is_warned) Some(warning_color)
   335         else if (status.is_unprocessed) Some(unprocessed_color)
   336         else None
   337       }
   338     }
   339   }
   340 
   341 
   342   /* highlighted area */
   343 
   344   def highlight(range: Text.Range): Option[Text.Info[Color]] =
   345     snapshot.select(range, Rendering.highlight_elements, _ =>
   346       {
   347         case info => Some(Text.Info(snapshot.convert(info.range), highlight_color))
   348       }).headOption.map(_.info)
   349 
   350 
   351   /* hyperlinks */
   352 
   353   private def jedit_file(name: String): String =
   354     if (Path.is_valid(name))
   355       PIDE.resources.append(snapshot.node_name.master_dir, Path.explode(name))
   356     else name
   357 
   358   def hyperlink(range: Text.Range): Option[Text.Info[PIDE.editor.Hyperlink]] =
   359   {
   360     snapshot.cumulate[Vector[Text.Info[PIDE.editor.Hyperlink]]](
   361       range, Vector.empty, Rendering.hyperlink_elements, _ =>
   362         {
   363           case (links, Text.Info(info_range, XML.Elem(Markup.Path(name), _))) =>
   364             val link = PIDE.editor.hyperlink_file(jedit_file(name))
   365             Some(links :+ Text.Info(snapshot.convert(info_range), link))
   366 
   367           case (links, Text.Info(info_range, XML.Elem(Markup.Url(name), _))) =>
   368             val link = PIDE.editor.hyperlink_url(name)
   369             Some(links :+ Text.Info(snapshot.convert(info_range), link))
   370 
   371           case (links, Text.Info(info_range, XML.Elem(Markup(Markup.ENTITY, props), _)))
   372           if !props.exists(
   373             { case (Markup.KIND, Markup.ML_OPEN) => true
   374               case (Markup.KIND, Markup.ML_STRUCTURE) => true
   375               case _ => false }) =>
   376             val opt_link =
   377               props match {
   378                 case Position.Def_Line_File(line, name) =>
   379                   val offset = Position.Def_Offset.unapply(props) getOrElse 0
   380                   PIDE.editor.hyperlink_source_file(name, line, offset)
   381                 case Position.Def_Id_Offset0(id, offset) =>
   382                   PIDE.editor.hyperlink_command_id(snapshot, id, offset)
   383                 case _ => None
   384               }
   385             opt_link.map(link => (links :+ Text.Info(snapshot.convert(info_range), link)))
   386 
   387           case (links, Text.Info(info_range, XML.Elem(Markup(Markup.POSITION, props), _))) =>
   388             val opt_link =
   389               props match {
   390                 case Position.Line_File(line, name) =>
   391                   val offset = Position.Offset.unapply(props) getOrElse 0
   392                   PIDE.editor.hyperlink_source_file(name, line, offset)
   393                 case Position.Id_Offset0(id, offset) =>
   394                   PIDE.editor.hyperlink_command_id(snapshot, id, offset)
   395                 case _ => None
   396               }
   397             opt_link.map(link => (links :+ Text.Info(snapshot.convert(info_range), link)))
   398 
   399           case (links, Text.Info(info_range, XML.Elem(Markup.Citation(name), _))) =>
   400             val opt_link =
   401               Bibtex_JEdit.entries_iterator.collectFirst(
   402                 { case (a, buffer, offset) if a == name =>
   403                     PIDE.editor.hyperlink_buffer(buffer, offset) })
   404             opt_link.map(link => (links :+ Text.Info(snapshot.convert(info_range), link)))
   405 
   406           case _ => None
   407         }) match { case Text.Info(_, _ :+ info) :: _ => Some(info) case _ => None }
   408   }
   409 
   410 
   411   /* active elements */
   412 
   413   def active(range: Text.Range): Option[Text.Info[XML.Elem]] =
   414     snapshot.select(range, Rendering.active_elements, command_states =>
   415       {
   416         case Text.Info(info_range, elem) =>
   417           if (elem.name == Markup.DIALOG) {
   418             elem match {
   419               case Protocol.Dialog(_, serial, _)
   420               if !command_states.exists(st => st.results.defined(serial)) =>
   421                 Some(Text.Info(snapshot.convert(info_range), elem))
   422               case _ => None
   423             }
   424           }
   425           else Some(Text.Info(snapshot.convert(info_range), elem))
   426       }).headOption.map(_.info)
   427 
   428   def command_results(range: Text.Range): Command.Results =
   429     Command.State.merge_results(
   430       snapshot.select[List[Command.State]](range, Markup.Elements.full, command_states =>
   431         { case _ => Some(command_states) }).flatMap(_.info))
   432 
   433 
   434   /* tooltip messages */
   435 
   436   def tooltip_message(range: Text.Range): Option[Text.Info[XML.Body]] =
   437   {
   438     val results =
   439       snapshot.cumulate[List[Text.Info[Command.Results.Entry]]](
   440         range, Nil, Rendering.tooltip_message_elements, _ =>
   441         {
   442           case (msgs, Text.Info(info_range,
   443             XML.Elem(Markup(name, props @ Markup.Serial(serial)), body)))
   444           if name == Markup.WRITELN || name == Markup.WARNING || name == Markup.ERROR =>
   445             val entry: Command.Results.Entry =
   446               (serial -> XML.Elem(Markup(Markup.message(name), props), body))
   447             Some(Text.Info(snapshot.convert(info_range), entry) :: msgs)
   448 
   449           case (msgs, Text.Info(info_range, msg @ XML.Elem(Markup(Markup.BAD, _), body)))
   450           if !body.isEmpty =>
   451             val entry: Command.Results.Entry = (Document_ID.make(), msg)
   452             Some(Text.Info(snapshot.convert(info_range), entry) :: msgs)
   453 
   454           case _ => None
   455         }).flatMap(_.info)
   456     if (results.isEmpty) None
   457     else {
   458       val r = Text.Range(results.head.range.start, results.last.range.stop)
   459       val msgs = Command.Results.make(results.map(_.info))
   460       Some(Text.Info(r, Pretty.separate(msgs.iterator.map(_._2).toList)))
   461     }
   462   }
   463 
   464 
   465   /* tooltips */
   466 
   467   private def pretty_typing(kind: String, body: XML.Body): XML.Tree =
   468     Pretty.block(XML.Text(kind) :: Pretty.Break(1) :: body)
   469 
   470   private def timing_threshold: Double = options.real("jedit_timing_threshold")
   471 
   472   def tooltip(range: Text.Range): Option[Text.Info[XML.Body]] =
   473   {
   474     def add(prev: Text.Info[(Timing, Vector[(Boolean, XML.Tree)])],
   475       r0: Text.Range, p: (Boolean, XML.Tree)): Text.Info[(Timing, Vector[(Boolean, XML.Tree)])] =
   476     {
   477       val r = snapshot.convert(r0)
   478       val (t, info) = prev.info
   479       if (prev.range == r)
   480         Text.Info(r, (t, info :+ p))
   481       else Text.Info(r, (t, Vector(p)))
   482     }
   483 
   484     val results =
   485       snapshot.cumulate[Text.Info[(Timing, Vector[(Boolean, XML.Tree)])]](
   486         range, Text.Info(range, (Timing.zero, Vector.empty)), Rendering.tooltip_elements, _ =>
   487         {
   488           case (Text.Info(r, (t1, info)), Text.Info(_, XML.Elem(Markup.Timing(t2), _))) =>
   489             Some(Text.Info(r, (t1 + t2, info)))
   490           case (prev, Text.Info(r, XML.Elem(Markup.Entity(kind, name), _))) =>
   491             val kind1 = Word.implode(Word.explode('_', kind))
   492             val txt1 =
   493               if (name == "") kind1
   494               else kind1 + " " + quote(name)
   495             val t = prev.info._1
   496             val txt2 =
   497               if (kind == Markup.COMMAND && t.elapsed.seconds >= timing_threshold)
   498                 "\n" + t.message
   499               else ""
   500             Some(add(prev, r, (true, XML.Text(txt1 + txt2))))
   501           case (prev, Text.Info(r, XML.Elem(Markup.Path(name), _))) =>
   502             val file = jedit_file(name)
   503             val text =
   504               if (name == file) "file " + quote(file)
   505               else "path " + quote(name) + "\nfile " + quote(file)
   506             Some(add(prev, r, (true, XML.Text(text))))
   507           case (prev, Text.Info(r, XML.Elem(Markup.Url(name), _))) =>
   508             Some(add(prev, r, (true, XML.Text("URL " + quote(name)))))
   509           case (prev, Text.Info(r, XML.Elem(Markup(name, _), body)))
   510           if name == Markup.SORTING || name == Markup.TYPING =>
   511             Some(add(prev, r, (true, pretty_typing("::", body))))
   512           case (prev, Text.Info(r, XML.Elem(Markup(Markup.ML_TYPING, _), body))) =>
   513             Some(add(prev, r, (false, pretty_typing("ML:", body))))
   514           case (prev, Text.Info(r, XML.Elem(Markup.Language(language, _, _, _), _))) =>
   515             Some(add(prev, r, (true, XML.Text("language: " + language))))
   516           case (prev, Text.Info(r, XML.Elem(Markup(name, _), _))) =>
   517             Rendering.tooltip_descriptions.get(name).
   518               map(descr => add(prev, r, (true, XML.Text(descr))))
   519         }).map(_.info)
   520 
   521     results.map(_.info).flatMap(res => res._2.toList) match {
   522       case Nil => None
   523       case tips =>
   524         val r = Text.Range(results.head.range.start, results.last.range.stop)
   525         val all_tips = (tips.filter(_._1) ++ tips.filter(!_._1).lastOption.toList).map(_._2)
   526         Some(Text.Info(r, Library.separate(Pretty.FBreak, all_tips)))
   527     }
   528   }
   529 
   530   def tooltip_margin: Int = options.int("jedit_tooltip_margin")
   531 
   532   lazy val tooltip_close_icon = JEdit_Lib.load_icon(options.string("tooltip_close_icon"))
   533   lazy val tooltip_detach_icon = JEdit_Lib.load_icon(options.string("tooltip_detach_icon"))
   534 
   535 
   536   /* gutter */
   537 
   538   private def gutter_message_pri(msg: XML.Tree): Int =
   539     if (Protocol.is_error(msg)) Rendering.error_pri
   540     else if (Protocol.is_legacy(msg)) Rendering.legacy_pri
   541     else if (Protocol.is_warning(msg)) Rendering.warning_pri
   542     else if (Protocol.is_information(msg)) Rendering.information_pri
   543     else 0
   544 
   545   private lazy val gutter_icons = Map(
   546     Rendering.information_pri -> JEdit_Lib.load_icon(options.string("gutter_information_icon")),
   547     Rendering.warning_pri -> JEdit_Lib.load_icon(options.string("gutter_warning_icon")),
   548     Rendering.legacy_pri -> JEdit_Lib.load_icon(options.string("gutter_legacy_icon")),
   549     Rendering.error_pri -> JEdit_Lib.load_icon(options.string("gutter_error_icon")))
   550 
   551   def gutter_icon(range: Text.Range): Option[Icon] =
   552   {
   553     val pris =
   554       snapshot.cumulate[Int](range, 0, Rendering.gutter_elements, _ =>
   555         {
   556           case (pri, Text.Info(_, msg @ XML.Elem(Markup(_, Markup.Serial(serial)), _))) =>
   557             Some(pri max gutter_message_pri(msg))
   558           case _ => None
   559         }).map(_.info)
   560 
   561     gutter_icons.get((0 /: pris)(_ max _))
   562   }
   563 
   564 
   565   /* squiggly underline */
   566 
   567   private lazy val squiggly_colors = Map(
   568     Rendering.writeln_pri -> writeln_color,
   569     Rendering.information_pri -> information_color,
   570     Rendering.warning_pri -> warning_color,
   571     Rendering.error_pri -> error_color)
   572 
   573   def squiggly_underline(range: Text.Range): List[Text.Info[Color]] =
   574   {
   575     val results =
   576       snapshot.cumulate[Int](range, 0, Rendering.squiggly_elements, _ =>
   577         {
   578           case (pri, Text.Info(_, elem)) =>
   579             if (Protocol.is_information(elem))
   580               Some(pri max Rendering.information_pri)
   581             else
   582               Some(pri max Rendering.message_pri(elem.name))
   583         })
   584     for {
   585       Text.Info(r, pri) <- results
   586       color <- squiggly_colors.get(pri)
   587     } yield Text.Info(r, color)
   588   }
   589 
   590 
   591   /* message output */
   592 
   593   private lazy val message_colors = Map(
   594     Rendering.writeln_pri -> writeln_message_color,
   595     Rendering.information_pri -> information_message_color,
   596     Rendering.tracing_pri -> tracing_message_color,
   597     Rendering.warning_pri -> warning_message_color,
   598     Rendering.error_pri -> error_message_color)
   599 
   600   def line_background(range: Text.Range): Option[(Color, Boolean)] =
   601   {
   602     val results =
   603       snapshot.cumulate[Int](range, 0, Rendering.line_background_elements, _ =>
   604         {
   605           case (pri, Text.Info(_, elem)) =>
   606             if (elem.name == Markup.INFORMATION)
   607               Some(pri max Rendering.information_pri)
   608             else
   609               Some(pri max Rendering.message_pri(elem.name))
   610         })
   611     val pri = (0 /: results) { case (p1, Text.Info(_, p2)) => p1 max p2 }
   612 
   613     val is_separator =
   614       pri > 0 &&
   615       snapshot.cumulate[Boolean](range, false, Rendering.separator_elements, _ =>
   616         {
   617           case _ => Some(true)
   618         }).exists(_.info)
   619 
   620     message_colors.get(pri).map((_, is_separator))
   621   }
   622 
   623   def output_messages(results: Command.Results): List[XML.Tree] =
   624   {
   625     val (states, other) =
   626       results.iterator.map(_._2).filterNot(Protocol.is_result(_)).toList
   627         .partition(Protocol.is_state(_))
   628     states ::: other
   629   }
   630 
   631 
   632   /* text background */
   633 
   634   def background(range: Text.Range): List[Text.Info[Color]] =
   635   {
   636     if (snapshot.is_outdated && snapshot.is_loaded) List(Text.Info(range, outdated_color))
   637     else
   638       for {
   639         Text.Info(r, result) <-
   640           snapshot.cumulate[(List[Markup], Option[Color])](
   641             range, (List(Markup.Empty), None), Rendering.background_elements,
   642             command_states =>
   643               {
   644                 case (((status, color), Text.Info(_, XML.Elem(markup, _))))
   645                 if !status.isEmpty && Protocol.proper_status_elements(markup.name) =>
   646                   Some((markup :: status, color))
   647                 case (_, Text.Info(_, XML.Elem(Markup(Markup.BAD, _), _))) =>
   648                   Some((Nil, Some(bad_color)))
   649                 case (_, Text.Info(_, XML.Elem(Markup(Markup.INTENSIFY, _), _))) =>
   650                   Some((Nil, Some(intensify_color)))
   651                 case (acc, Text.Info(_, Protocol.Dialog(_, serial, result))) =>
   652                   command_states.collectFirst(
   653                     { case st if st.results.defined(serial) => st.results.get(serial).get }) match
   654                   {
   655                     case Some(Protocol.Dialog_Result(res)) if res == result =>
   656                       Some((Nil, Some(active_result_color)))
   657                     case _ =>
   658                       Some((Nil, Some(active_color)))
   659                   }
   660                 case (_, Text.Info(_, elem)) =>
   661                   if (Rendering.active_elements(elem.name)) Some((Nil, Some(active_color)))
   662                   else None
   663               })
   664         color <-
   665           (result match {
   666             case (markups, opt_color) if !markups.isEmpty =>
   667               val status = Protocol.Status.make(markups.iterator)
   668               if (status.is_unprocessed) Some(unprocessed1_color)
   669               else if (status.is_running) Some(running1_color)
   670               else opt_color
   671             case (_, opt_color) => opt_color
   672           })
   673       } yield Text.Info(r, color)
   674   }
   675 
   676 
   677   /* text foreground */
   678 
   679   def foreground(range: Text.Range): List[Text.Info[Color]] =
   680     snapshot.select(range, Rendering.foreground_elements, _ =>
   681       {
   682         case Text.Info(_, elem) =>
   683           if (elem.name == Markup.ANTIQUOTED) Some(antiquoted_color) else Some(quoted_color)
   684       })
   685 
   686 
   687   /* text color */
   688 
   689   private lazy val text_colors: Map[String, Color] = Map(
   690       Markup.KEYWORD1 -> keyword1_color,
   691       Markup.KEYWORD2 -> keyword2_color,
   692       Markup.KEYWORD3 -> keyword3_color,
   693       Markup.QUASI_KEYWORD -> quasi_keyword_color,
   694       Markup.IMPROPER -> improper_color,
   695       Markup.OPERATOR -> operator_color,
   696       Markup.STRING -> Color.BLACK,
   697       Markup.ALTSTRING -> Color.BLACK,
   698       Markup.VERBATIM -> Color.BLACK,
   699       Markup.CARTOUCHE -> Color.BLACK,
   700       Markup.LITERAL -> keyword1_color,
   701       Markup.DELIMITER -> Color.BLACK,
   702       Markup.TFREE -> tfree_color,
   703       Markup.TVAR -> tvar_color,
   704       Markup.FREE -> free_color,
   705       Markup.SKOLEM -> skolem_color,
   706       Markup.BOUND -> bound_color,
   707       Markup.VAR -> var_color,
   708       Markup.INNER_STRING -> inner_quoted_color,
   709       Markup.INNER_CARTOUCHE -> inner_cartouche_color,
   710       Markup.INNER_COMMENT -> inner_comment_color,
   711       Markup.DYNAMIC_FACT -> dynamic_color,
   712       Markup.ANTIQUOTE -> antiquote_color,
   713       Markup.ML_KEYWORD1 -> keyword1_color,
   714       Markup.ML_KEYWORD2 -> keyword2_color,
   715       Markup.ML_KEYWORD3 -> keyword3_color,
   716       Markup.ML_DELIMITER -> Color.BLACK,
   717       Markup.ML_NUMERAL -> inner_numeral_color,
   718       Markup.ML_CHAR -> inner_quoted_color,
   719       Markup.ML_STRING -> inner_quoted_color,
   720       Markup.ML_COMMENT -> inner_comment_color,
   721       Markup.SML_STRING -> inner_quoted_color,
   722       Markup.SML_COMMENT -> inner_comment_color)
   723 
   724   private lazy val text_color_elements =
   725     Markup.Elements(text_colors.keySet)
   726 
   727   def text_color(range: Text.Range, color: Color): List[Text.Info[Color]] =
   728   {
   729     if (color == Token_Markup.hidden_color) List(Text.Info(range, color))
   730     else
   731       snapshot.cumulate(range, color, text_color_elements, _ =>
   732         {
   733           case (_, Text.Info(_, elem)) => text_colors.get(elem.name)
   734         })
   735   }
   736 
   737 
   738   /* virtual bullets */
   739 
   740   def bullet(range: Text.Range): List[Text.Info[Color]] =
   741     snapshot.select(range, Rendering.bullet_elements, _ => _ => Some(bullet_color))
   742 
   743 
   744   /* text folds */
   745 
   746   def fold_depth(range: Text.Range): List[Text.Info[Int]] =
   747     snapshot.cumulate[Int](range, 0, Rendering.fold_depth_elements, _ =>
   748       {
   749         case (depth, _) => Some(depth + 1)
   750       })
   751 }