--- a/src/Pure/PIDE/protocol.scala Wed Apr 09 13:32:34 2014 +0200
+++ b/src/Pure/PIDE/protocol.scala Wed Apr 09 15:03:07 2014 +0200
@@ -214,9 +214,6 @@
/* specific messages */
- def is_inlined(msg: XML.Tree): Boolean =
- !(is_result(msg) || is_tracing(msg) || is_state(msg))
-
def is_result(msg: XML.Tree): Boolean =
msg match {
case XML.Elem(Markup(Markup.RESULT, _), _) => true
@@ -239,8 +236,14 @@
case _ => false
}
- def is_state(msg: XML.Tree): Boolean = is_writeln_markup(msg, Markup.STATE)
- def is_information(msg: XML.Tree): Boolean = is_writeln_markup(msg, Markup.INFORMATION)
+ def is_warning_markup(msg: XML.Tree, name: String): Boolean =
+ msg match {
+ case XML.Elem(Markup(Markup.WARNING, _),
+ List(XML.Elem(markup, _))) => markup.name == name
+ case XML.Elem(Markup(Markup.WARNING_MESSAGE, _),
+ List(XML.Elem(markup, _))) => markup.name == name
+ case _ => false
+ }
def is_warning(msg: XML.Tree): Boolean =
msg match {
@@ -256,6 +259,13 @@
case _ => false
}
+ def is_state(msg: XML.Tree): Boolean = is_writeln_markup(msg, Markup.STATE)
+ def is_information(msg: XML.Tree): Boolean = is_writeln_markup(msg, Markup.INFORMATION)
+ def is_legacy(msg: XML.Tree): Boolean = is_warning_markup(msg, Markup.LEGACY)
+
+ def is_inlined(msg: XML.Tree): Boolean =
+ !(is_result(msg) || is_tracing(msg) || is_state(msg))
+
/* dialogs */
--- a/src/Tools/jEdit/src/document_view.scala Wed Apr 09 13:32:34 2014 +0200
+++ b/src/Tools/jEdit/src/document_view.scala Wed Apr 09 15:03:07 2014 +0200
@@ -144,7 +144,7 @@
val line_range = Text.Range(start(i), end(i))
// gutter icons
- rendering.gutter_message(line_range) match {
+ rendering.gutter_icon(line_range) match {
case Some(icon) =>
val x0 = (FOLD_MARKER_SIZE + width - border_width - icon.getIconWidth) max 10
val y0 = y + i * line_height + (((line_height - icon.getIconHeight) / 2) max 0)
--- a/src/Tools/jEdit/src/rendering.scala Wed Apr 09 13:32:34 2014 +0200
+++ b/src/Tools/jEdit/src/rendering.scala Wed Apr 09 15:03:07 2014 +0200
@@ -495,7 +495,14 @@
lazy val tooltip_detach_icon = JEdit_Lib.load_icon(options.string("tooltip_detach_icon"))
- /* gutter icons */
+ /* gutter */
+
+ private def gutter_message_pri(msg: XML.Tree): Int =
+ if (Protocol.is_error(msg)) Rendering.error_pri
+ else if (Protocol.is_legacy(msg)) Rendering.legacy_pri
+ else if (Protocol.is_warning(msg)) Rendering.warning_pri
+ else if (Protocol.is_information(msg)) Rendering.information_pri
+ else 0
private lazy val gutter_icons = Map(
Rendering.information_pri -> JEdit_Lib.load_icon(options.string("gutter_information_icon")),
@@ -503,27 +510,17 @@
Rendering.legacy_pri -> JEdit_Lib.load_icon(options.string("gutter_legacy_icon")),
Rendering.error_pri -> JEdit_Lib.load_icon(options.string("gutter_error_icon")))
- def gutter_message(range: Text.Range): Option[Icon] =
+ def gutter_icon(range: Text.Range): Option[Icon] =
{
- val results =
+ val pris =
snapshot.cumulate[Int](range, 0, Rendering.gutter_elements, _ =>
{
- case (pri, Text.Info(_, XML.Elem(Markup(Markup.WRITELN, _),
- List(XML.Elem(Markup(Markup.INFORMATION, _), _))))) =>
- Some(pri max Rendering.information_pri)
- case (pri, Text.Info(_, XML.Elem(Markup(Markup.WARNING, _), body))) =>
- body match {
- case List(XML.Elem(Markup(Markup.LEGACY, _), _)) =>
- Some(pri max Rendering.legacy_pri)
- case _ =>
- Some(pri max Rendering.warning_pri)
- }
- case (pri, Text.Info(_, XML.Elem(Markup(Markup.ERROR, _), _))) =>
- Some(pri max Rendering.error_pri)
+ case (pri, Text.Info(_, msg @ XML.Elem(Markup(_, Markup.Serial(serial)), _))) =>
+ Some(pri max gutter_message_pri(msg))
case _ => None
- })
- val pri = (0 /: results) { case (p1, Text.Info(_, p2)) => p1 max p2 }
- gutter_icons.get(pri)
+ }).map(_.info)
+
+ gutter_icons.get((0 /: pris)(_ max _))
}