src/Tools/jEdit/src/rendering.scala
author wenzelm
Wed Aug 13 22:29:43 2014 +0200 (2014-08-13)
changeset 57931 4e2cbff02f23
parent 57914 cbc55e5091a1
child 58048 aa6296d09e0e
permissions -rw-r--r--
tuned;
     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.LANGUAGE, Markup.ML_TYPING, Markup.TOKEN_RANGE,
   143       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.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.TOKEN_RANGE -> "inner syntax token",
   160       Markup.FREE -> "free variable",
   161       Markup.SKOLEM -> "skolem variable",
   162       Markup.BOUND -> "bound variable",
   163       Markup.VAR -> "schematic variable",
   164       Markup.TFREE -> "free type variable",
   165       Markup.TVAR -> "schematic type variable")
   166 
   167   private val tooltip_elements =
   168     Markup.Elements(Markup.LANGUAGE, Markup.TIMING, Markup.ENTITY, Markup.SORTING,
   169       Markup.TYPING, Markup.ML_TYPING, Markup.PATH, Markup.URL) ++
   170     Markup.Elements(tooltip_descriptions.keySet)
   171 
   172   private val gutter_elements =
   173     Markup.Elements(Markup.WRITELN, Markup.WARNING, Markup.ERROR)
   174 
   175   private val squiggly_elements =
   176     Markup.Elements(Markup.WRITELN, Markup.WARNING, Markup.ERROR)
   177 
   178   private val line_background_elements =
   179     Markup.Elements(Markup.WRITELN_MESSAGE, Markup.TRACING_MESSAGE,
   180       Markup.WARNING_MESSAGE, Markup.ERROR_MESSAGE,
   181       Markup.INFORMATION)
   182 
   183   private val separator_elements =
   184     Markup.Elements(Markup.SEPARATOR)
   185 
   186   private val background_elements =
   187     Protocol.proper_status_elements + Markup.WRITELN_MESSAGE +
   188       Markup.TRACING_MESSAGE + Markup.WARNING_MESSAGE +
   189       Markup.ERROR_MESSAGE + Markup.BAD + Markup.INTENSIFY ++
   190       active_elements
   191 
   192   private val foreground_elements =
   193     Markup.Elements(Markup.STRING, Markup.ALTSTRING, Markup.VERBATIM,
   194       Markup.CARTOUCHE, Markup.ANTIQUOTED)
   195 
   196   private val bullet_elements =
   197     Markup.Elements(Markup.BULLET)
   198 
   199   private val fold_depth_elements =
   200     Markup.Elements(Markup.TEXT_FOLD, Markup.GOAL, Markup.SUBGOAL)
   201 }
   202 
   203 
   204 class Rendering private(val snapshot: Document.Snapshot, val options: Options)
   205 {
   206   override def toString: String = "Rendering(" + snapshot.toString + ")"
   207 
   208 
   209   /* colors */
   210 
   211   def color_value(s: String): Color = Color_Value(options.string(s))
   212 
   213   val outdated_color = color_value("outdated_color")
   214   val unprocessed_color = color_value("unprocessed_color")
   215   val unprocessed1_color = color_value("unprocessed1_color")
   216   val running_color = color_value("running_color")
   217   val running1_color = color_value("running1_color")
   218   val bullet_color = color_value("bullet_color")
   219   val tooltip_color = color_value("tooltip_color")
   220   val writeln_color = color_value("writeln_color")
   221   val information_color = color_value("information_color")
   222   val warning_color = color_value("warning_color")
   223   val error_color = color_value("error_color")
   224   val error1_color = color_value("error1_color")
   225   val writeln_message_color = color_value("writeln_message_color")
   226   val information_message_color = color_value("information_message_color")
   227   val tracing_message_color = color_value("tracing_message_color")
   228   val warning_message_color = color_value("warning_message_color")
   229   val error_message_color = color_value("error_message_color")
   230   val spell_checker_color = color_value("spell_checker_color")
   231   val bad_color = color_value("bad_color")
   232   val intensify_color = color_value("intensify_color")
   233   val quoted_color = color_value("quoted_color")
   234   val antiquoted_color = color_value("antiquoted_color")
   235   val antiquote_color = color_value("antiquote_color")
   236   val highlight_color = color_value("highlight_color")
   237   val hyperlink_color = color_value("hyperlink_color")
   238   val active_color = color_value("active_color")
   239   val active_hover_color = color_value("active_hover_color")
   240   val active_result_color = color_value("active_result_color")
   241   val keyword1_color = color_value("keyword1_color")
   242   val keyword2_color = color_value("keyword2_color")
   243   val keyword3_color = color_value("keyword3_color")
   244   val quasi_keyword_color = color_value("quasi_keyword_color")
   245   val improper_color = color_value("improper_color")
   246   val operator_color = color_value("operator_color")
   247   val caret_invisible_color = color_value("caret_invisible_color")
   248   val completion_color = color_value("completion_color")
   249   val search_color = color_value("search_color")
   250 
   251   val tfree_color = color_value("tfree_color")
   252   val tvar_color = color_value("tvar_color")
   253   val free_color = color_value("free_color")
   254   val skolem_color = color_value("skolem_color")
   255   val bound_color = color_value("bound_color")
   256   val var_color = color_value("var_color")
   257   val inner_numeral_color = color_value("inner_numeral_color")
   258   val inner_quoted_color = color_value("inner_quoted_color")
   259   val inner_cartouche_color = color_value("inner_cartouche_color")
   260   val inner_comment_color = color_value("inner_comment_color")
   261   val dynamic_color = color_value("dynamic_color")
   262 
   263 
   264   /* completion */
   265 
   266   def semantic_completion(range: Text.Range): Option[Text.Info[Completion.Semantic]] =
   267     if (snapshot.is_outdated) None
   268     else {
   269       snapshot.select(range, Rendering.semantic_completion_elements, _ =>
   270         {
   271           case Completion.Semantic.Info(info) => Some(info)
   272           case _ => None
   273         }).headOption.map(_.info)
   274     }
   275 
   276   def language_context(range: Text.Range): Option[Completion.Language_Context] =
   277     snapshot.select(range, Rendering.language_context_elements, _ =>
   278       {
   279         case Text.Info(_, XML.Elem(Markup.Language(language, symbols, antiquotes, delimited), _)) =>
   280           if (delimited) Some(Completion.Language_Context(language, symbols, antiquotes))
   281           else None
   282         case Text.Info(_, elem)
   283         if elem.name == Markup.ML_STRING || elem.name == Markup.ML_COMMENT =>
   284           Some(Completion.Language_Context.ML_inner)
   285         case Text.Info(_, _) =>
   286           Some(Completion.Language_Context.inner)
   287       }).headOption.map(_.info)
   288 
   289   def language_path(range: Text.Range): Option[Text.Range] =
   290     snapshot.select(range, Rendering.language_elements, _ =>
   291       {
   292         case Text.Info(info_range, XML.Elem(Markup.Language(Markup.Language.PATH, _, _, _), _)) =>
   293           Some(snapshot.convert(info_range))
   294         case _ => None
   295       }).headOption.map(_.info)
   296 
   297 
   298   /* spell checker */
   299 
   300   private lazy val spell_checker_elements =
   301     Markup.Elements(space_explode(',', options.string("spell_checker_elements")): _*)
   302 
   303   def spell_checker_ranges(range: Text.Range): List[Text.Range] =
   304     snapshot.select(range, spell_checker_elements, _ => _ => Some(())).map(_.range)
   305 
   306   def spell_checker_point(range: Text.Range): Option[Text.Range] =
   307     snapshot.select(range, spell_checker_elements, _ =>
   308       {
   309         case info => Some(snapshot.convert(info.range))
   310       }).headOption.map(_.info)
   311 
   312 
   313   /* command status overview */
   314 
   315   def overview_limit: Int = options.int("jedit_text_overview_limit")
   316 
   317   def overview_color(range: Text.Range): Option[Color] =
   318   {
   319     if (snapshot.is_outdated) None
   320     else {
   321       val results =
   322         snapshot.cumulate[List[Markup]](range, Nil, Protocol.liberal_status_elements, _ =>
   323           {
   324             case (status, Text.Info(_, elem)) => Some(elem.markup :: status)
   325           }, status = true)
   326       if (results.isEmpty) None
   327       else {
   328         val status = Protocol.Status.make(results.iterator.flatMap(_.info))
   329 
   330         if (status.is_running) Some(running_color)
   331         else if (status.is_failed) Some(error_color)
   332         else if (status.is_warned) Some(warning_color)
   333         else if (status.is_unprocessed) Some(unprocessed_color)
   334         else None
   335       }
   336     }
   337   }
   338 
   339 
   340   /* highlighted area */
   341 
   342   def highlight(range: Text.Range): Option[Text.Info[Color]] =
   343     snapshot.select(range, Rendering.highlight_elements, _ =>
   344       {
   345         case info => Some(Text.Info(snapshot.convert(info.range), highlight_color))
   346       }).headOption.map(_.info)
   347 
   348 
   349   /* hyperlinks */
   350 
   351   private def jedit_file(name: String): String =
   352     if (Path.is_valid(name))
   353       PIDE.resources.append(snapshot.node_name.master_dir, Path.explode(name))
   354     else name
   355 
   356   def hyperlink(range: Text.Range): Option[Text.Info[PIDE.editor.Hyperlink]] =
   357   {
   358     snapshot.cumulate[Vector[Text.Info[PIDE.editor.Hyperlink]]](
   359       range, Vector.empty, Rendering.hyperlink_elements, _ =>
   360         {
   361           case (links, Text.Info(info_range, XML.Elem(Markup.Path(name), _))) =>
   362             val link = PIDE.editor.hyperlink_file(jedit_file(name))
   363             Some(links :+ Text.Info(snapshot.convert(info_range), link))
   364 
   365           case (links, Text.Info(info_range, XML.Elem(Markup.Url(name), _))) =>
   366             val link = PIDE.editor.hyperlink_url(name)
   367             Some(links :+ Text.Info(snapshot.convert(info_range), link))
   368 
   369           case (links, Text.Info(info_range, XML.Elem(Markup(Markup.ENTITY, props), _)))
   370           if !props.exists(
   371             { case (Markup.KIND, Markup.ML_OPEN) => true
   372               case (Markup.KIND, Markup.ML_STRUCTURE) => true
   373               case _ => false }) =>
   374             val opt_link =
   375               props match {
   376                 case Position.Def_Line_File(line, name) =>
   377                   val offset = Position.Def_Offset.unapply(props) getOrElse 0
   378                   PIDE.editor.hyperlink_source_file(name, line, offset)
   379                 case Position.Def_Id_Offset0(id, offset) =>
   380                   PIDE.editor.hyperlink_command_id(snapshot, id, offset)
   381                 case _ => None
   382               }
   383             opt_link.map(link => (links :+ Text.Info(snapshot.convert(info_range), link)))
   384 
   385           case (links, Text.Info(info_range, XML.Elem(Markup(Markup.POSITION, props), _))) =>
   386             val opt_link =
   387               props match {
   388                 case Position.Line_File(line, name) =>
   389                   val offset = Position.Offset.unapply(props) getOrElse 0
   390                   PIDE.editor.hyperlink_source_file(name, line, offset)
   391                 case Position.Id_Offset0(id, offset) =>
   392                   PIDE.editor.hyperlink_command_id(snapshot, id, offset)
   393                 case _ => None
   394               }
   395             opt_link.map(link => (links :+ Text.Info(snapshot.convert(info_range), link)))
   396 
   397           case _ => None
   398         }) match { case Text.Info(_, _ :+ info) :: _ => Some(info) case _ => None }
   399   }
   400 
   401 
   402   /* active elements */
   403 
   404   def active(range: Text.Range): Option[Text.Info[XML.Elem]] =
   405     snapshot.select(range, Rendering.active_elements, command_states =>
   406       {
   407         case Text.Info(info_range, elem) =>
   408           if (elem.name == Markup.DIALOG) {
   409             elem match {
   410               case Protocol.Dialog(_, serial, _)
   411               if !command_states.exists(st => st.results.defined(serial)) =>
   412                 Some(Text.Info(snapshot.convert(info_range), elem))
   413               case _ => None
   414             }
   415           }
   416           else Some(Text.Info(snapshot.convert(info_range), elem))
   417       }).headOption.map(_.info)
   418 
   419   def command_results(range: Text.Range): Command.Results =
   420     Command.State.merge_results(
   421       snapshot.select[List[Command.State]](range, Markup.Elements.full, command_states =>
   422         { case _ => Some(command_states) }).flatMap(_.info))
   423 
   424 
   425   /* tooltip messages */
   426 
   427   def tooltip_message(range: Text.Range): Option[Text.Info[XML.Body]] =
   428   {
   429     val results =
   430       snapshot.cumulate[List[Text.Info[Command.Results.Entry]]](
   431         range, Nil, Rendering.tooltip_message_elements, _ =>
   432         {
   433           case (msgs, Text.Info(info_range,
   434             XML.Elem(Markup(name, props @ Markup.Serial(serial)), body)))
   435           if name == Markup.WRITELN || name == Markup.WARNING || name == Markup.ERROR =>
   436             val entry: Command.Results.Entry =
   437               (serial -> XML.Elem(Markup(Markup.message(name), props), body))
   438             Some(Text.Info(snapshot.convert(info_range), entry) :: msgs)
   439 
   440           case (msgs, Text.Info(info_range, msg @ XML.Elem(Markup(Markup.BAD, _), body)))
   441           if !body.isEmpty =>
   442             val entry: Command.Results.Entry = (Document_ID.make(), msg)
   443             Some(Text.Info(snapshot.convert(info_range), entry) :: msgs)
   444 
   445           case _ => None
   446         }).flatMap(_.info)
   447     if (results.isEmpty) None
   448     else {
   449       val r = Text.Range(results.head.range.start, results.last.range.stop)
   450       val msgs = Command.Results.make(results.map(_.info))
   451       Some(Text.Info(r, Pretty.separate(msgs.iterator.map(_._2).toList)))
   452     }
   453   }
   454 
   455 
   456   /* tooltips */
   457 
   458   private def pretty_typing(kind: String, body: XML.Body): XML.Tree =
   459     Pretty.block(XML.Text(kind) :: Pretty.Break(1) :: body)
   460 
   461   private def timing_threshold: Double = options.real("jedit_timing_threshold")
   462 
   463   def tooltip(range: Text.Range): Option[Text.Info[XML.Body]] =
   464   {
   465     def add(prev: Text.Info[(Timing, Vector[(Boolean, XML.Tree)])],
   466       r0: Text.Range, p: (Boolean, XML.Tree)): Text.Info[(Timing, Vector[(Boolean, XML.Tree)])] =
   467     {
   468       val r = snapshot.convert(r0)
   469       val (t, info) = prev.info
   470       if (prev.range == r)
   471         Text.Info(r, (t, info :+ p))
   472       else Text.Info(r, (t, Vector(p)))
   473     }
   474 
   475     val results =
   476       snapshot.cumulate[Text.Info[(Timing, Vector[(Boolean, XML.Tree)])]](
   477         range, Text.Info(range, (Timing.zero, Vector.empty)), Rendering.tooltip_elements, _ =>
   478         {
   479           case (Text.Info(r, (t1, info)), Text.Info(_, XML.Elem(Markup.Timing(t2), _))) =>
   480             Some(Text.Info(r, (t1 + t2, info)))
   481           case (prev, Text.Info(r, XML.Elem(Markup.Entity(kind, name), _))) =>
   482             val kind1 = Word.implode(Word.explode('_', kind))
   483             val txt1 = kind1 + " " + quote(name)
   484             val t = prev.info._1
   485             val txt2 =
   486               if (kind == Markup.COMMAND && t.elapsed.seconds >= timing_threshold)
   487                 "\n" + t.message
   488               else ""
   489             Some(add(prev, r, (true, XML.Text(txt1 + txt2))))
   490           case (prev, Text.Info(r, XML.Elem(Markup.Path(name), _))) =>
   491             val file = jedit_file(name)
   492             val text =
   493               if (name == file) "file " + quote(file)
   494               else "path " + quote(name) + "\nfile " + quote(file)
   495             Some(add(prev, r, (true, XML.Text(text))))
   496           case (prev, Text.Info(r, XML.Elem(Markup.Url(name), _))) =>
   497             Some(add(prev, r, (true, XML.Text("URL " + quote(name)))))
   498           case (prev, Text.Info(r, XML.Elem(Markup(name, _), body)))
   499           if name == Markup.SORTING || name == Markup.TYPING =>
   500             Some(add(prev, r, (true, pretty_typing("::", body))))
   501           case (prev, Text.Info(r, XML.Elem(Markup(Markup.ML_TYPING, _), body))) =>
   502             Some(add(prev, r, (false, pretty_typing("ML:", body))))
   503           case (prev, Text.Info(r, XML.Elem(Markup.Language(language, _, _, _), _))) =>
   504             Some(add(prev, r, (true, XML.Text("language: " + language))))
   505           case (prev, Text.Info(r, XML.Elem(Markup(name, _), _))) =>
   506             Rendering.tooltip_descriptions.get(name).
   507               map(descr => add(prev, r, (true, XML.Text(descr))))
   508         }).map(_.info)
   509 
   510     results.map(_.info).flatMap(res => res._2.toList) match {
   511       case Nil => None
   512       case tips =>
   513         val r = Text.Range(results.head.range.start, results.last.range.stop)
   514         val all_tips = (tips.filter(_._1) ++ tips.filter(!_._1).lastOption.toList).map(_._2)
   515         Some(Text.Info(r, Library.separate(Pretty.FBreak, all_tips)))
   516     }
   517   }
   518 
   519   def tooltip_margin: Int = options.int("jedit_tooltip_margin")
   520 
   521   lazy val tooltip_close_icon = JEdit_Lib.load_icon(options.string("tooltip_close_icon"))
   522   lazy val tooltip_detach_icon = JEdit_Lib.load_icon(options.string("tooltip_detach_icon"))
   523 
   524 
   525   /* gutter */
   526 
   527   private def gutter_message_pri(msg: XML.Tree): Int =
   528     if (Protocol.is_error(msg)) Rendering.error_pri
   529     else if (Protocol.is_legacy(msg)) Rendering.legacy_pri
   530     else if (Protocol.is_warning(msg)) Rendering.warning_pri
   531     else if (Protocol.is_information(msg)) Rendering.information_pri
   532     else 0
   533 
   534   private lazy val gutter_icons = Map(
   535     Rendering.information_pri -> JEdit_Lib.load_icon(options.string("gutter_information_icon")),
   536     Rendering.warning_pri -> JEdit_Lib.load_icon(options.string("gutter_warning_icon")),
   537     Rendering.legacy_pri -> JEdit_Lib.load_icon(options.string("gutter_legacy_icon")),
   538     Rendering.error_pri -> JEdit_Lib.load_icon(options.string("gutter_error_icon")))
   539 
   540   def gutter_icon(range: Text.Range): Option[Icon] =
   541   {
   542     val pris =
   543       snapshot.cumulate[Int](range, 0, Rendering.gutter_elements, _ =>
   544         {
   545           case (pri, Text.Info(_, msg @ XML.Elem(Markup(_, Markup.Serial(serial)), _))) =>
   546             Some(pri max gutter_message_pri(msg))
   547           case _ => None
   548         }).map(_.info)
   549 
   550     gutter_icons.get((0 /: pris)(_ max _))
   551   }
   552 
   553 
   554   /* squiggly underline */
   555 
   556   private lazy val squiggly_colors = Map(
   557     Rendering.writeln_pri -> writeln_color,
   558     Rendering.information_pri -> information_color,
   559     Rendering.warning_pri -> warning_color,
   560     Rendering.error_pri -> error_color)
   561 
   562   def squiggly_underline(range: Text.Range): List[Text.Info[Color]] =
   563   {
   564     val results =
   565       snapshot.cumulate[Int](range, 0, Rendering.squiggly_elements, _ =>
   566         {
   567           case (pri, Text.Info(_, elem)) =>
   568             if (Protocol.is_information(elem))
   569               Some(pri max Rendering.information_pri)
   570             else
   571               Some(pri max Rendering.message_pri(elem.name))
   572         })
   573     for {
   574       Text.Info(r, pri) <- results
   575       color <- squiggly_colors.get(pri)
   576     } yield Text.Info(r, color)
   577   }
   578 
   579 
   580   /* message output */
   581 
   582   private lazy val message_colors = Map(
   583     Rendering.writeln_pri -> writeln_message_color,
   584     Rendering.information_pri -> information_message_color,
   585     Rendering.tracing_pri -> tracing_message_color,
   586     Rendering.warning_pri -> warning_message_color,
   587     Rendering.error_pri -> error_message_color)
   588 
   589   def line_background(range: Text.Range): Option[(Color, Boolean)] =
   590   {
   591     val results =
   592       snapshot.cumulate[Int](range, 0, Rendering.line_background_elements, _ =>
   593         {
   594           case (pri, Text.Info(_, elem)) =>
   595             if (elem.name == Markup.INFORMATION)
   596               Some(pri max Rendering.information_pri)
   597             else
   598               Some(pri max Rendering.message_pri(elem.name))
   599         })
   600     val pri = (0 /: results) { case (p1, Text.Info(_, p2)) => p1 max p2 }
   601 
   602     val is_separator =
   603       pri > 0 &&
   604       snapshot.cumulate[Boolean](range, false, Rendering.separator_elements, _ =>
   605         {
   606           case _ => Some(true)
   607         }).exists(_.info)
   608 
   609     message_colors.get(pri).map((_, is_separator))
   610   }
   611 
   612   def output_messages(results: Command.Results): List[XML.Tree] =
   613   {
   614     val (states, other) =
   615       results.iterator.map(_._2).filterNot(Protocol.is_result(_)).toList
   616         .partition(Protocol.is_state(_))
   617     states ::: other
   618   }
   619 
   620 
   621   /* text background */
   622 
   623   def background(range: Text.Range): List[Text.Info[Color]] =
   624   {
   625     if (snapshot.is_outdated && snapshot.is_loaded) List(Text.Info(range, outdated_color))
   626     else
   627       for {
   628         Text.Info(r, result) <-
   629           snapshot.cumulate[(List[Markup], Option[Color])](
   630             range, (List(Markup.Empty), None), Rendering.background_elements,
   631             command_states =>
   632               {
   633                 case (((status, color), Text.Info(_, XML.Elem(markup, _))))
   634                 if !status.isEmpty && Protocol.proper_status_elements(markup.name) =>
   635                   Some((markup :: status, color))
   636                 case (_, Text.Info(_, XML.Elem(Markup(Markup.BAD, _), _))) =>
   637                   Some((Nil, Some(bad_color)))
   638                 case (_, Text.Info(_, XML.Elem(Markup(Markup.INTENSIFY, _), _))) =>
   639                   Some((Nil, Some(intensify_color)))
   640                 case (acc, Text.Info(_, Protocol.Dialog(_, serial, result))) =>
   641                   command_states.collectFirst(
   642                     { case st if st.results.defined(serial) => st.results.get(serial).get }) match
   643                   {
   644                     case Some(Protocol.Dialog_Result(res)) if res == result =>
   645                       Some((Nil, Some(active_result_color)))
   646                     case _ =>
   647                       Some((Nil, Some(active_color)))
   648                   }
   649                 case (_, Text.Info(_, elem)) =>
   650                   if (Rendering.active_elements(elem.name)) Some((Nil, Some(active_color)))
   651                   else None
   652               })
   653         color <-
   654           (result match {
   655             case (markups, opt_color) if !markups.isEmpty =>
   656               val status = Protocol.Status.make(markups.iterator)
   657               if (status.is_unprocessed) Some(unprocessed1_color)
   658               else if (status.is_running) Some(running1_color)
   659               else opt_color
   660             case (_, opt_color) => opt_color
   661           })
   662       } yield Text.Info(r, color)
   663   }
   664 
   665 
   666   /* text foreground */
   667 
   668   def foreground(range: Text.Range): List[Text.Info[Color]] =
   669     snapshot.select(range, Rendering.foreground_elements, _ =>
   670       {
   671         case Text.Info(_, elem) =>
   672           if (elem.name == Markup.ANTIQUOTED) Some(antiquoted_color) else Some(quoted_color)
   673       })
   674 
   675 
   676   /* text color */
   677 
   678   private lazy val text_colors: Map[String, Color] = Map(
   679       Markup.KEYWORD1 -> keyword1_color,
   680       Markup.KEYWORD2 -> keyword2_color,
   681       Markup.KEYWORD3 -> keyword3_color,
   682       Markup.QUASI_KEYWORD -> quasi_keyword_color,
   683       Markup.IMPROPER -> improper_color,
   684       Markup.OPERATOR -> operator_color,
   685       Markup.STRING -> Color.BLACK,
   686       Markup.ALTSTRING -> Color.BLACK,
   687       Markup.VERBATIM -> Color.BLACK,
   688       Markup.CARTOUCHE -> Color.BLACK,
   689       Markup.LITERAL -> keyword1_color,
   690       Markup.DELIMITER -> Color.BLACK,
   691       Markup.TFREE -> tfree_color,
   692       Markup.TVAR -> tvar_color,
   693       Markup.FREE -> free_color,
   694       Markup.SKOLEM -> skolem_color,
   695       Markup.BOUND -> bound_color,
   696       Markup.VAR -> var_color,
   697       Markup.INNER_STRING -> inner_quoted_color,
   698       Markup.INNER_CARTOUCHE -> inner_cartouche_color,
   699       Markup.INNER_COMMENT -> inner_comment_color,
   700       Markup.DYNAMIC_FACT -> dynamic_color,
   701       Markup.ANTIQUOTE -> antiquote_color,
   702       Markup.ML_KEYWORD1 -> keyword1_color,
   703       Markup.ML_KEYWORD2 -> keyword2_color,
   704       Markup.ML_KEYWORD3 -> keyword3_color,
   705       Markup.ML_DELIMITER -> Color.BLACK,
   706       Markup.ML_NUMERAL -> inner_numeral_color,
   707       Markup.ML_CHAR -> inner_quoted_color,
   708       Markup.ML_STRING -> inner_quoted_color,
   709       Markup.ML_COMMENT -> inner_comment_color,
   710       Markup.SML_STRING -> inner_quoted_color,
   711       Markup.SML_COMMENT -> inner_comment_color)
   712 
   713   private lazy val text_color_elements =
   714     Markup.Elements(text_colors.keySet)
   715 
   716   def text_color(range: Text.Range, color: Color): List[Text.Info[Color]] =
   717   {
   718     if (color == Token_Markup.hidden_color) List(Text.Info(range, color))
   719     else
   720       snapshot.cumulate(range, color, text_color_elements, _ =>
   721         {
   722           case (_, Text.Info(_, elem)) => text_colors.get(elem.name)
   723         })
   724   }
   725 
   726 
   727   /* virtual bullets */
   728 
   729   def bullet(range: Text.Range): List[Text.Info[Color]] =
   730     snapshot.select(range, Rendering.bullet_elements, _ => _ => Some(bullet_color))
   731 
   732 
   733   /* text folds */
   734 
   735   def fold_depth(range: Text.Range): List[Text.Info[Int]] =
   736     snapshot.cumulate[Int](range, 0, Rendering.fold_depth_elements, _ =>
   737       {
   738         case (depth, _) => Some(depth + 1)
   739       })
   740 }