# HG changeset patch
# User wenzelm
# Date 1397048587 -7200
# Node ID 0b9334adcf05abc5c61f145a0c1de270d6e58d8c
# Parent  1b74abf064e1c8168117df898dad71c55b55b7bc
more explicit message discrimination;

diff -r 1b74abf064e1 -r 0b9334adcf05 src/Pure/PIDE/protocol.scala
--- 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 */
 
diff -r 1b74abf064e1 -r 0b9334adcf05 src/Tools/jEdit/src/document_view.scala
--- 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)
diff -r 1b74abf064e1 -r 0b9334adcf05 src/Tools/jEdit/src/rendering.scala
--- 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 _))
   }