# HG changeset patch
# User wenzelm
# Date 1283896754 -7200
# Node ID 2257eded83230312f77377384d34c5a60c45daf1
# Parent  e1d160a9bd5facebd0a366c12c0212e358270add
Document_View: select gutter message icons from markup over line range, not full range results;
tuned;

diff -r e1d160a9bd5f -r 2257eded8323 src/Pure/PIDE/isar_document.scala
--- a/src/Pure/PIDE/isar_document.scala	Tue Sep 07 23:53:27 2010 +0200
+++ b/src/Pure/PIDE/isar_document.scala	Tue Sep 07 23:59:14 2010 +0200
@@ -56,21 +56,6 @@
   }
 
 
-  /* result messages */
-
-  def is_warning(msg: XML.Tree): Boolean =
-    msg match {
-      case XML.Elem(Markup(Markup.WARNING, _), _) => true
-      case _ => false
-    }
-
-  def is_error(msg: XML.Tree): Boolean =
-    msg match {
-      case XML.Elem(Markup(Markup.ERROR, _), _) => true
-      case _ => false
-    }
-
-
   /* reported positions */
 
   private val include_pos = Set(Markup.BINDING, Markup.ENTITY, Markup.REPORT, Markup.POSITION)
diff -r e1d160a9bd5f -r 2257eded8323 src/Tools/jEdit/src/jedit/document_view.scala
--- a/src/Tools/jEdit/src/jedit/document_view.scala	Tue Sep 07 23:53:27 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/document_view.scala	Tue Sep 07 23:59:14 2010 +0200
@@ -245,7 +245,6 @@
               for {
                 Text.Info(range, Some(color)) <-
                   snapshot.select_markup(line_range)(Isabelle_Markup.message).iterator
-                if color != null
                 r <- Isabelle.gfx_range(text_area, range)
               } {
                 gfx.setColor(color)
@@ -299,20 +298,17 @@
               val line_range = proper_line_range(start(i), end(i))
 
               // gutter icons
-              val cmds = snapshot.node.command_range(snapshot.revert(line_range))
-              val states = cmds.map(p => snapshot.state(p._1)).toStream
-              val opt_icon =
-                if (states.exists(_.results.exists(p => Isar_Document.is_error(p._2))))
-                  Some(Isabelle_Markup.error_icon)
-                else if (states.exists(_.results.exists(p => Isar_Document.is_warning(p._2))))
-                  Some(Isabelle_Markup.warning_icon)
-                else None
-              opt_icon match {
-                case Some(icon) if icon.getIconWidth > 0 && icon.getIconHeight > 0 =>
-                  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)
-                  icon.paintIcon(gutter, gfx, x0, y0)
-                case _ =>
+              val icons =
+                (for (Text.Info(_, Some(icon)) <-
+                  snapshot.select_markup(line_range)(Isabelle_Markup.gutter_message).iterator)
+                yield icon).toList.sortWith(_ >= _)
+              icons match {
+                case icon :: _ =>
+                  val icn = icon.icon
+                  val x0 = (FOLD_MARKER_SIZE + width - border_width - icn.getIconWidth) max 10
+                  val y0 = y + i * line_height + (((line_height - icn.getIconHeight) / 2) max 0)
+                  icn.paintIcon(gutter, gfx, x0, y0)
+                case Nil =>
               }
             }
           }
diff -r e1d160a9bd5f -r 2257eded8323 src/Tools/jEdit/src/jedit/isabelle_markup.scala
--- a/src/Tools/jEdit/src/jedit/isabelle_markup.scala	Tue Sep 07 23:53:27 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/isabelle_markup.scala	Tue Sep 07 23:59:14 2010 +0200
@@ -27,8 +27,12 @@
   val error_color = new Color(255, 80, 80)
   val bad_color = new Color(255, 204, 153, 100)
 
-  val warning_icon = GUIUtilities.loadIcon("16x16/status/dialog-warning.png")
-  val error_icon = GUIUtilities.loadIcon("16x16/status/dialog-error.png")
+  class Icon(val priority: Int, val icon: javax.swing.Icon)
+  {
+    def >= (that: Icon): Boolean = this.priority >= that.priority
+  }
+  val warning_icon = new Icon(1, GUIUtilities.loadIcon("16x16/status/dialog-warning.png"))
+  val error_icon = new Icon(2, GUIUtilities.loadIcon("16x16/status/dialog-error.png"))
 
 
   /* command status */
@@ -77,6 +81,12 @@
     case Text.Info(_, XML.Elem(Markup(Markup.ERROR, _), _)) => error_color
   }
 
+  val gutter_message: Markup_Tree.Select[Icon] =
+  {
+    case Text.Info(_, XML.Elem(Markup(Markup.WARNING, _), _)) => warning_icon
+    case Text.Info(_, XML.Elem(Markup(Markup.ERROR, _), _)) => error_icon
+  }
+
   val background: Markup_Tree.Select[Color] =
   {
     case Text.Info(_, XML.Elem(Markup(Markup.BAD, _), _)) => bad_color