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 |