src/Tools/jEdit/src/jedit/isabelle_markup.scala
changeset 39181 2257eded8323
parent 39179 591bbab9ef59
child 39241 e9a442606db3
     1.1 --- a/src/Tools/jEdit/src/jedit/isabelle_markup.scala	Tue Sep 07 23:53:27 2010 +0200
     1.2 +++ b/src/Tools/jEdit/src/jedit/isabelle_markup.scala	Tue Sep 07 23:59:14 2010 +0200
     1.3 @@ -27,8 +27,12 @@
     1.4    val error_color = new Color(255, 80, 80)
     1.5    val bad_color = new Color(255, 204, 153, 100)
     1.6  
     1.7 -  val warning_icon = GUIUtilities.loadIcon("16x16/status/dialog-warning.png")
     1.8 -  val error_icon = GUIUtilities.loadIcon("16x16/status/dialog-error.png")
     1.9 +  class Icon(val priority: Int, val icon: javax.swing.Icon)
    1.10 +  {
    1.11 +    def >= (that: Icon): Boolean = this.priority >= that.priority
    1.12 +  }
    1.13 +  val warning_icon = new Icon(1, GUIUtilities.loadIcon("16x16/status/dialog-warning.png"))
    1.14 +  val error_icon = new Icon(2, GUIUtilities.loadIcon("16x16/status/dialog-error.png"))
    1.15  
    1.16  
    1.17    /* command status */
    1.18 @@ -77,6 +81,12 @@
    1.19      case Text.Info(_, XML.Elem(Markup(Markup.ERROR, _), _)) => error_color
    1.20    }
    1.21  
    1.22 +  val gutter_message: Markup_Tree.Select[Icon] =
    1.23 +  {
    1.24 +    case Text.Info(_, XML.Elem(Markup(Markup.WARNING, _), _)) => warning_icon
    1.25 +    case Text.Info(_, XML.Elem(Markup(Markup.ERROR, _), _)) => error_icon
    1.26 +  }
    1.27 +
    1.28    val background: Markup_Tree.Select[Color] =
    1.29    {
    1.30      case Text.Info(_, XML.Elem(Markup(Markup.BAD, _), _)) => bad_color