src/Tools/jEdit/src/rendering.scala
changeset 59129 6959ceb53ac8
parent 59125 ee19c92ae8b4
child 59184 830bb7ddb3ab
equal deleted inserted replaced
59128:7b1931111e37 59129:6959ceb53ac8
   221   val tooltip_color = color_value("tooltip_color")
   221   val tooltip_color = color_value("tooltip_color")
   222   val writeln_color = color_value("writeln_color")
   222   val writeln_color = color_value("writeln_color")
   223   val information_color = color_value("information_color")
   223   val information_color = color_value("information_color")
   224   val warning_color = color_value("warning_color")
   224   val warning_color = color_value("warning_color")
   225   val error_color = color_value("error_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")
   226   val writeln_message_color = color_value("writeln_message_color")
   228   val information_message_color = color_value("information_message_color")
   227   val information_message_color = color_value("information_message_color")
   229   val tracing_message_color = color_value("tracing_message_color")
   228   val tracing_message_color = color_value("tracing_message_color")
   230   val warning_message_color = color_value("warning_message_color")
   229   val warning_message_color = color_value("warning_message_color")
   231   val error_message_color = color_value("error_message_color")
   230   val error_message_color = color_value("error_message_color")
   550     else if (Protocol.is_legacy(msg)) Rendering.legacy_pri
   549     else if (Protocol.is_legacy(msg)) Rendering.legacy_pri
   551     else if (Protocol.is_warning(msg)) Rendering.warning_pri
   550     else if (Protocol.is_warning(msg)) Rendering.warning_pri
   552     else if (Protocol.is_information(msg)) Rendering.information_pri
   551     else if (Protocol.is_information(msg)) Rendering.information_pri
   553     else 0
   552     else 0
   554 
   553 
   555   private lazy val gutter_icons = Map(
   554   private lazy val gutter_message_content = Map(
   556     Rendering.information_pri -> JEdit_Lib.load_icon(options.string("gutter_information_icon")),
   555     Rendering.information_pri ->
   557     Rendering.warning_pri -> JEdit_Lib.load_icon(options.string("gutter_warning_icon")),
   556       (JEdit_Lib.load_icon(options.string("gutter_information_icon")), information_message_color),
   558     Rendering.legacy_pri -> JEdit_Lib.load_icon(options.string("gutter_legacy_icon")),
   557     Rendering.warning_pri ->
   559     Rendering.error_pri -> JEdit_Lib.load_icon(options.string("gutter_error_icon")))
   558       (JEdit_Lib.load_icon(options.string("gutter_warning_icon")), warning_message_color),
   560 
   559     Rendering.legacy_pri ->
   561   def gutter_icon(range: Text.Range): Option[Icon] =
   560       (JEdit_Lib.load_icon(options.string("gutter_legacy_icon")), warning_message_color),
       
   561     Rendering.error_pri ->
       
   562       (JEdit_Lib.load_icon(options.string("gutter_error_icon")), error_message_color))
       
   563 
       
   564   def gutter_content(range: Text.Range): Option[(Icon, Color)] =
   562   {
   565   {
   563     val pris =
   566     val pris =
   564       snapshot.cumulate[Int](range, 0, Rendering.gutter_elements, _ =>
   567       snapshot.cumulate[Int](range, 0, Rendering.gutter_elements, _ =>
   565         {
   568         {
   566           case (pri, Text.Info(_, msg @ XML.Elem(Markup(_, Markup.Serial(serial)), _))) =>
   569           case (pri, Text.Info(_, msg @ XML.Elem(Markup(_, Markup.Serial(serial)), _))) =>
   567             Some(pri max gutter_message_pri(msg))
   570             Some(pri max gutter_message_pri(msg))
   568           case _ => None
   571           case _ => None
   569         }).map(_.info)
   572         }).map(_.info)
   570 
   573 
   571     gutter_icons.get((0 /: pris)(_ max _))
   574     gutter_message_content.get((0 /: pris)(_ max _))
   572   }
   575   }
   573 
   576 
   574 
   577 
   575   /* squiggly underline */
   578   /* squiggly underline */
   576 
   579