basic support for warning/error gutter icons;

--- a/src/Pure/PIDE/isar_document.scala	Tue Sep 07 17:34:28 2010 +0200
+++ b/src/Pure/PIDE/isar_document.scala	Tue Sep 07 18:44:28 2010 +0200
@@ -56,6 +56,21 @@
   }
 
 
+  /* 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)

--- a/src/Tools/jEdit/src/jedit/document_view.scala	Tue Sep 07 17:34:28 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/document_view.scala	Tue Sep 07 18:44:28 2010 +0200
@@ -17,7 +17,7 @@
 import javax.swing.{JPanel, ToolTipManager}
 import javax.swing.event.{CaretListener, CaretEvent}
 
-import org.gjt.sp.jedit.OperatingSystem
+import org.gjt.sp.jedit.{GUIUtilities, OperatingSystem}
 import org.gjt.sp.jedit.gui.RolloverButton
 import org.gjt.sp.jedit.textarea.{JEditTextArea, TextArea, TextAreaExtension, TextAreaPainter}
 import org.gjt.sp.jedit.syntax.SyntaxStyle
@@ -35,6 +35,9 @@
   val error_color = new Color(255, 106, 106)
   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")
+
   def status_color(snapshot: Document.Snapshot, command: Command): Option[Color] =
   {
     val state = snapshot.state(command)
@@ -353,6 +356,48 @@
   }
 
 
+  /* gutter_extension */
+
+  private val gutter_extension = new TextAreaExtension
+  {
+    override def paintScreenLineRange(gfx: Graphics2D,
+      first_line: Int, last_line: Int, physical_lines: Array[Int],
+      start: Array[Int], end: Array[Int], y: Int, line_height: Int)
+    {
+      Isabelle.swing_buffer_lock(model.buffer) {
+        val snapshot = model.snapshot()
+        val saved_color = gfx.getColor
+        try {
+          for (i <- 0 until physical_lines.length) {
+            if (physical_lines(i) != -1) {
+              val line_range = proper_line_range(start(i), end(i))
+              val cmds = snapshot.node.command_range(snapshot.revert(line_range)).toStream
+
+              // gutter icons
+              val states = cmds.map(p => snapshot.state(p._1))
+              val opt_icon =
+                if (states.exists(_.results.exists(p => Isar_Document.is_error(p._2))))
+                  Some(Document_View.error_icon)
+                else if (states.exists(_.results.exists(p => Isar_Document.is_warning(p._2))))
+                  Some(Document_View.warning_icon)
+                else None
+              opt_icon match {
+                case Some(icon) if icon.getIconWidth > 0 && icon.getIconHeight > 0 =>
+                  val FOLD_MARKER_SIZE = 12
+                  val x0 = ((FOLD_MARKER_SIZE - icon.getIconWidth) / 2) max 0
+                  val y0 = y + i * line_height + (((line_height - icon.getIconHeight) / 2) max 0)
+                  icon.paintIcon(text_area.getPainter, gfx, x0, y0)
+                case _ =>
+              }
+            }
+          }
+        }
+        finally { gfx.setColor(saved_color) }
+      }
+    }
+  }
+
+
   /* caret handling */
 
   def selected_command(): Option[Command] =
@@ -445,6 +490,7 @@
   {
     text_area.getPainter.
       addExtension(TextAreaPainter.LINE_BACKGROUND_LAYER + 1, text_area_extension)
+    text_area.getGutter.addExtension(gutter_extension)
     text_area.addFocusListener(focus_listener)
     text_area.getPainter.addMouseMotionListener(mouse_motion_listener)
     text_area.addCaretListener(caret_listener)
@@ -459,6 +505,7 @@
     text_area.getPainter.removeMouseMotionListener(mouse_motion_listener)
     text_area.removeCaretListener(caret_listener)
     text_area.removeLeftOfScrollBar(overview)
+    text_area.getGutter.removeExtension(gutter_extension)
     text_area.getPainter.removeExtension(text_area_extension)
   }
 }
\ No newline at end of file