more explicit message discrimination;
authorwenzelm
Wed Apr 09 15:03:07 2014 +0200 (2014-04-09)
changeset 564950b9334adcf05
parent 56494 1b74abf064e1
child 56496 46b29bb1c627
more explicit message discrimination;
src/Pure/PIDE/protocol.scala
src/Tools/jEdit/src/document_view.scala
src/Tools/jEdit/src/rendering.scala
     1.1 --- a/src/Pure/PIDE/protocol.scala	Wed Apr 09 13:32:34 2014 +0200
     1.2 +++ b/src/Pure/PIDE/protocol.scala	Wed Apr 09 15:03:07 2014 +0200
     1.3 @@ -214,9 +214,6 @@
     1.4  
     1.5    /* specific messages */
     1.6  
     1.7 -  def is_inlined(msg: XML.Tree): Boolean =
     1.8 -    !(is_result(msg) || is_tracing(msg) || is_state(msg))
     1.9 -
    1.10    def is_result(msg: XML.Tree): Boolean =
    1.11      msg match {
    1.12        case XML.Elem(Markup(Markup.RESULT, _), _) => true
    1.13 @@ -239,8 +236,14 @@
    1.14        case _ => false
    1.15      }
    1.16  
    1.17 -  def is_state(msg: XML.Tree): Boolean = is_writeln_markup(msg, Markup.STATE)
    1.18 -  def is_information(msg: XML.Tree): Boolean = is_writeln_markup(msg, Markup.INFORMATION)
    1.19 +  def is_warning_markup(msg: XML.Tree, name: String): Boolean =
    1.20 +    msg match {
    1.21 +      case XML.Elem(Markup(Markup.WARNING, _),
    1.22 +        List(XML.Elem(markup, _))) => markup.name == name
    1.23 +      case XML.Elem(Markup(Markup.WARNING_MESSAGE, _),
    1.24 +        List(XML.Elem(markup, _))) => markup.name == name
    1.25 +      case _ => false
    1.26 +    }
    1.27  
    1.28    def is_warning(msg: XML.Tree): Boolean =
    1.29      msg match {
    1.30 @@ -256,6 +259,13 @@
    1.31        case _ => false
    1.32      }
    1.33  
    1.34 +  def is_state(msg: XML.Tree): Boolean = is_writeln_markup(msg, Markup.STATE)
    1.35 +  def is_information(msg: XML.Tree): Boolean = is_writeln_markup(msg, Markup.INFORMATION)
    1.36 +  def is_legacy(msg: XML.Tree): Boolean = is_warning_markup(msg, Markup.LEGACY)
    1.37 +
    1.38 +  def is_inlined(msg: XML.Tree): Boolean =
    1.39 +    !(is_result(msg) || is_tracing(msg) || is_state(msg))
    1.40 +
    1.41  
    1.42    /* dialogs */
    1.43  
     2.1 --- a/src/Tools/jEdit/src/document_view.scala	Wed Apr 09 13:32:34 2014 +0200
     2.2 +++ b/src/Tools/jEdit/src/document_view.scala	Wed Apr 09 15:03:07 2014 +0200
     2.3 @@ -144,7 +144,7 @@
     2.4                  val line_range = Text.Range(start(i), end(i))
     2.5  
     2.6                  // gutter icons
     2.7 -                rendering.gutter_message(line_range) match {
     2.8 +                rendering.gutter_icon(line_range) match {
     2.9                    case Some(icon) =>
    2.10                      val x0 = (FOLD_MARKER_SIZE + width - border_width - icon.getIconWidth) max 10
    2.11                      val y0 = y + i * line_height + (((line_height - icon.getIconHeight) / 2) max 0)
     3.1 --- a/src/Tools/jEdit/src/rendering.scala	Wed Apr 09 13:32:34 2014 +0200
     3.2 +++ b/src/Tools/jEdit/src/rendering.scala	Wed Apr 09 15:03:07 2014 +0200
     3.3 @@ -495,7 +495,14 @@
     3.4    lazy val tooltip_detach_icon = JEdit_Lib.load_icon(options.string("tooltip_detach_icon"))
     3.5  
     3.6  
     3.7 -  /* gutter icons */
     3.8 +  /* gutter */
     3.9 +
    3.10 +  private def gutter_message_pri(msg: XML.Tree): Int =
    3.11 +    if (Protocol.is_error(msg)) Rendering.error_pri
    3.12 +    else if (Protocol.is_legacy(msg)) Rendering.legacy_pri
    3.13 +    else if (Protocol.is_warning(msg)) Rendering.warning_pri
    3.14 +    else if (Protocol.is_information(msg)) Rendering.information_pri
    3.15 +    else 0
    3.16  
    3.17    private lazy val gutter_icons = Map(
    3.18      Rendering.information_pri -> JEdit_Lib.load_icon(options.string("gutter_information_icon")),
    3.19 @@ -503,27 +510,17 @@
    3.20      Rendering.legacy_pri -> JEdit_Lib.load_icon(options.string("gutter_legacy_icon")),
    3.21      Rendering.error_pri -> JEdit_Lib.load_icon(options.string("gutter_error_icon")))
    3.22  
    3.23 -  def gutter_message(range: Text.Range): Option[Icon] =
    3.24 +  def gutter_icon(range: Text.Range): Option[Icon] =
    3.25    {
    3.26 -    val results =
    3.27 +    val pris =
    3.28        snapshot.cumulate[Int](range, 0, Rendering.gutter_elements, _ =>
    3.29          {
    3.30 -          case (pri, Text.Info(_, XML.Elem(Markup(Markup.WRITELN, _),
    3.31 -              List(XML.Elem(Markup(Markup.INFORMATION, _), _))))) =>
    3.32 -            Some(pri max Rendering.information_pri)
    3.33 -          case (pri, Text.Info(_, XML.Elem(Markup(Markup.WARNING, _), body))) =>
    3.34 -            body match {
    3.35 -              case List(XML.Elem(Markup(Markup.LEGACY, _), _)) =>
    3.36 -                Some(pri max Rendering.legacy_pri)
    3.37 -              case _ =>
    3.38 -                Some(pri max Rendering.warning_pri)
    3.39 -            }
    3.40 -          case (pri, Text.Info(_, XML.Elem(Markup(Markup.ERROR, _), _))) =>
    3.41 -            Some(pri max Rendering.error_pri)
    3.42 +          case (pri, Text.Info(_, msg @ XML.Elem(Markup(_, Markup.Serial(serial)), _))) =>
    3.43 +            Some(pri max gutter_message_pri(msg))
    3.44            case _ => None
    3.45 -        })
    3.46 -    val pri = (0 /: results) { case (p1, Text.Info(_, p2)) => p1 max p2 }
    3.47 -    gutter_icons.get(pri)
    3.48 +        }).map(_.info)
    3.49 +
    3.50 +    gutter_icons.get((0 /: pris)(_ max _))
    3.51    }
    3.52  
    3.53