Document_View: select gutter message icons from markup over line range, not full range results;
authorwenzelm
Tue Sep 07 23:59:14 2010 +0200 (2010-09-07)
changeset 391812257eded8323
parent 39180 e1d160a9bd5f
child 39182 cce0c10ed943
Document_View: select gutter message icons from markup over line range, not full range results;
tuned;
src/Pure/PIDE/isar_document.scala
src/Tools/jEdit/src/jedit/document_view.scala
src/Tools/jEdit/src/jedit/isabelle_markup.scala
     1.1 --- a/src/Pure/PIDE/isar_document.scala	Tue Sep 07 23:53:27 2010 +0200
     1.2 +++ b/src/Pure/PIDE/isar_document.scala	Tue Sep 07 23:59:14 2010 +0200
     1.3 @@ -56,21 +56,6 @@
     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 23:53:27 2010 +0200
     2.2 +++ b/src/Tools/jEdit/src/jedit/document_view.scala	Tue Sep 07 23:59:14 2010 +0200
     2.3 @@ -245,7 +245,6 @@
     2.4                for {
     2.5                  Text.Info(range, Some(color)) <-
     2.6                    snapshot.select_markup(line_range)(Isabelle_Markup.message).iterator
     2.7 -                if color != null
     2.8                  r <- Isabelle.gfx_range(text_area, range)
     2.9                } {
    2.10                  gfx.setColor(color)
    2.11 @@ -299,20 +298,17 @@
    2.12                val line_range = proper_line_range(start(i), end(i))
    2.13  
    2.14                // gutter icons
    2.15 -              val cmds = snapshot.node.command_range(snapshot.revert(line_range))
    2.16 -              val states = cmds.map(p => snapshot.state(p._1)).toStream
    2.17 -              val opt_icon =
    2.18 -                if (states.exists(_.results.exists(p => Isar_Document.is_error(p._2))))
    2.19 -                  Some(Isabelle_Markup.error_icon)
    2.20 -                else if (states.exists(_.results.exists(p => Isar_Document.is_warning(p._2))))
    2.21 -                  Some(Isabelle_Markup.warning_icon)
    2.22 -                else None
    2.23 -              opt_icon match {
    2.24 -                case Some(icon) if icon.getIconWidth > 0 && icon.getIconHeight > 0 =>
    2.25 -                  val x0 = (FOLD_MARKER_SIZE + width - border_width - icon.getIconWidth) max 10
    2.26 -                  val y0 = y + i * line_height + (((line_height - icon.getIconHeight) / 2) max 0)
    2.27 -                  icon.paintIcon(gutter, gfx, x0, y0)
    2.28 -                case _ =>
    2.29 +              val icons =
    2.30 +                (for (Text.Info(_, Some(icon)) <-
    2.31 +                  snapshot.select_markup(line_range)(Isabelle_Markup.gutter_message).iterator)
    2.32 +                yield icon).toList.sortWith(_ >= _)
    2.33 +              icons match {
    2.34 +                case icon :: _ =>
    2.35 +                  val icn = icon.icon
    2.36 +                  val x0 = (FOLD_MARKER_SIZE + width - border_width - icn.getIconWidth) max 10
    2.37 +                  val y0 = y + i * line_height + (((line_height - icn.getIconHeight) / 2) max 0)
    2.38 +                  icn.paintIcon(gutter, gfx, x0, y0)
    2.39 +                case Nil =>
    2.40                }
    2.41              }
    2.42            }
     3.1 --- a/src/Tools/jEdit/src/jedit/isabelle_markup.scala	Tue Sep 07 23:53:27 2010 +0200
     3.2 +++ b/src/Tools/jEdit/src/jedit/isabelle_markup.scala	Tue Sep 07 23:59:14 2010 +0200
     3.3 @@ -27,8 +27,12 @@
     3.4    val error_color = new Color(255, 80, 80)
     3.5    val bad_color = new Color(255, 204, 153, 100)
     3.6  
     3.7 -  val warning_icon = GUIUtilities.loadIcon("16x16/status/dialog-warning.png")
     3.8 -  val error_icon = GUIUtilities.loadIcon("16x16/status/dialog-error.png")
     3.9 +  class Icon(val priority: Int, val icon: javax.swing.Icon)
    3.10 +  {
    3.11 +    def >= (that: Icon): Boolean = this.priority >= that.priority
    3.12 +  }
    3.13 +  val warning_icon = new Icon(1, GUIUtilities.loadIcon("16x16/status/dialog-warning.png"))
    3.14 +  val error_icon = new Icon(2, GUIUtilities.loadIcon("16x16/status/dialog-error.png"))
    3.15  
    3.16  
    3.17    /* command status */
    3.18 @@ -77,6 +81,12 @@
    3.19      case Text.Info(_, XML.Elem(Markup(Markup.ERROR, _), _)) => error_color
    3.20    }
    3.21  
    3.22 +  val gutter_message: Markup_Tree.Select[Icon] =
    3.23 +  {
    3.24 +    case Text.Info(_, XML.Elem(Markup(Markup.WARNING, _), _)) => warning_icon
    3.25 +    case Text.Info(_, XML.Elem(Markup(Markup.ERROR, _), _)) => error_icon
    3.26 +  }
    3.27 +
    3.28    val background: Markup_Tree.Select[Color] =
    3.29    {
    3.30      case Text.Info(_, XML.Elem(Markup(Markup.BAD, _), _)) => bad_color