basic support for warning/error gutter icons;
authorwenzelm
Tue Sep 07 18:44:28 2010 +0200 (2010-09-07)
changeset 39175a08d68e993ea
parent 39174 b95cf3892483
child 39176 b8fdd3ae8815
basic support for warning/error gutter icons;
src/Pure/PIDE/isar_document.scala
src/Tools/jEdit/src/jedit/document_view.scala
     1.1 --- a/src/Pure/PIDE/isar_document.scala	Tue Sep 07 17:34:28 2010 +0200
     1.2 +++ b/src/Pure/PIDE/isar_document.scala	Tue Sep 07 18:44:28 2010 +0200
     1.3 @@ -56,6 +56,21 @@
     1.4    }
     1.5  
     1.6  
     1.7 +  /* result messages */
     1.8 +
     1.9 +  def is_warning(msg: XML.Tree): Boolean =
    1.10 +    msg match {
    1.11 +      case XML.Elem(Markup(Markup.WARNING, _), _) => true
    1.12 +      case _ => false
    1.13 +    }
    1.14 +
    1.15 +  def is_error(msg: XML.Tree): Boolean =
    1.16 +    msg match {
    1.17 +      case XML.Elem(Markup(Markup.ERROR, _), _) => true
    1.18 +      case _ => false
    1.19 +    }
    1.20 +
    1.21 +
    1.22    /* reported positions */
    1.23  
    1.24    private val include_pos = Set(Markup.BINDING, Markup.ENTITY, Markup.REPORT, Markup.POSITION)
     2.1 --- a/src/Tools/jEdit/src/jedit/document_view.scala	Tue Sep 07 17:34:28 2010 +0200
     2.2 +++ b/src/Tools/jEdit/src/jedit/document_view.scala	Tue Sep 07 18:44:28 2010 +0200
     2.3 @@ -17,7 +17,7 @@
     2.4  import javax.swing.{JPanel, ToolTipManager}
     2.5  import javax.swing.event.{CaretListener, CaretEvent}
     2.6  
     2.7 -import org.gjt.sp.jedit.OperatingSystem
     2.8 +import org.gjt.sp.jedit.{GUIUtilities, OperatingSystem}
     2.9  import org.gjt.sp.jedit.gui.RolloverButton
    2.10  import org.gjt.sp.jedit.textarea.{JEditTextArea, TextArea, TextAreaExtension, TextAreaPainter}
    2.11  import org.gjt.sp.jedit.syntax.SyntaxStyle
    2.12 @@ -35,6 +35,9 @@
    2.13    val error_color = new Color(255, 106, 106)
    2.14    val bad_color = new Color(255, 204, 153, 100)
    2.15  
    2.16 +  val warning_icon = GUIUtilities.loadIcon("16x16/status/dialog-warning.png")
    2.17 +  val error_icon = GUIUtilities.loadIcon("16x16/status/dialog-error.png")
    2.18 +
    2.19    def status_color(snapshot: Document.Snapshot, command: Command): Option[Color] =
    2.20    {
    2.21      val state = snapshot.state(command)
    2.22 @@ -353,6 +356,48 @@
    2.23    }
    2.24  
    2.25  
    2.26 +  /* gutter_extension */
    2.27 +
    2.28 +  private val gutter_extension = new TextAreaExtension
    2.29 +  {
    2.30 +    override def paintScreenLineRange(gfx: Graphics2D,
    2.31 +      first_line: Int, last_line: Int, physical_lines: Array[Int],
    2.32 +      start: Array[Int], end: Array[Int], y: Int, line_height: Int)
    2.33 +    {
    2.34 +      Isabelle.swing_buffer_lock(model.buffer) {
    2.35 +        val snapshot = model.snapshot()
    2.36 +        val saved_color = gfx.getColor
    2.37 +        try {
    2.38 +          for (i <- 0 until physical_lines.length) {
    2.39 +            if (physical_lines(i) != -1) {
    2.40 +              val line_range = proper_line_range(start(i), end(i))
    2.41 +              val cmds = snapshot.node.command_range(snapshot.revert(line_range)).toStream
    2.42 +
    2.43 +              // gutter icons
    2.44 +              val states = cmds.map(p => snapshot.state(p._1))
    2.45 +              val opt_icon =
    2.46 +                if (states.exists(_.results.exists(p => Isar_Document.is_error(p._2))))
    2.47 +                  Some(Document_View.error_icon)
    2.48 +                else if (states.exists(_.results.exists(p => Isar_Document.is_warning(p._2))))
    2.49 +                  Some(Document_View.warning_icon)
    2.50 +                else None
    2.51 +              opt_icon match {
    2.52 +                case Some(icon) if icon.getIconWidth > 0 && icon.getIconHeight > 0 =>
    2.53 +                  val FOLD_MARKER_SIZE = 12
    2.54 +                  val x0 = ((FOLD_MARKER_SIZE - icon.getIconWidth) / 2) max 0
    2.55 +                  val y0 = y + i * line_height + (((line_height - icon.getIconHeight) / 2) max 0)
    2.56 +                  icon.paintIcon(text_area.getPainter, gfx, x0, y0)
    2.57 +                case _ =>
    2.58 +              }
    2.59 +            }
    2.60 +          }
    2.61 +        }
    2.62 +        finally { gfx.setColor(saved_color) }
    2.63 +      }
    2.64 +    }
    2.65 +  }
    2.66 +
    2.67 +
    2.68    /* caret handling */
    2.69  
    2.70    def selected_command(): Option[Command] =
    2.71 @@ -445,6 +490,7 @@
    2.72    {
    2.73      text_area.getPainter.
    2.74        addExtension(TextAreaPainter.LINE_BACKGROUND_LAYER + 1, text_area_extension)
    2.75 +    text_area.getGutter.addExtension(gutter_extension)
    2.76      text_area.addFocusListener(focus_listener)
    2.77      text_area.getPainter.addMouseMotionListener(mouse_motion_listener)
    2.78      text_area.addCaretListener(caret_listener)
    2.79 @@ -459,6 +505,7 @@
    2.80      text_area.getPainter.removeMouseMotionListener(mouse_motion_listener)
    2.81      text_area.removeCaretListener(caret_listener)
    2.82      text_area.removeLeftOfScrollBar(overview)
    2.83 +    text_area.getGutter.removeExtension(gutter_extension)
    2.84      text_area.getPainter.removeExtension(text_area_extension)
    2.85    }
    2.86  }
    2.87 \ No newline at end of file