tuned;
authorwenzelm
Thu Feb 20 17:21:48 2014 +0100 (2014-02-20 ago)
changeset 556237aea773c5574
parent 55622 ce575c2212fc
child 55624 d52409077135
tuned;
src/Tools/jEdit/src/rendering.scala
     1.1 --- a/src/Tools/jEdit/src/rendering.scala	Thu Feb 20 16:56:51 2014 +0100
     1.2 +++ b/src/Tools/jEdit/src/rendering.scala	Thu Feb 20 17:21:48 2014 +0100
     1.3 @@ -240,10 +240,10 @@
     1.4            range, (Protocol.Status.init, 0), overview_elements, _ =>
     1.5            {
     1.6              case ((status, pri), Text.Info(_, elem)) =>
     1.7 -              if (elem.name == Markup.WARNING || elem.name == Markup.ERROR)
     1.8 +              if (Protocol.command_status_markup(elem.name))
     1.9 +                Some((Protocol.command_status(status, elem.markup), pri))
    1.10 +              else
    1.11                  Some((status, pri max Rendering.message_pri(elem.name)))
    1.12 -              else
    1.13 -                Some((Protocol.command_status(status, elem.markup), pri))
    1.14            })
    1.15        if (results.isEmpty) None
    1.16        else {
    1.17 @@ -345,17 +345,16 @@
    1.18    def active(range: Text.Range): Option[Text.Info[XML.Elem]] =
    1.19      snapshot.select_markup(range, active_elements, command_state =>
    1.20        {
    1.21 -        case Text.Info(info_range, elem @ Protocol.Dialog(_, serial, _))
    1.22 -        if !command_state.results.defined(serial) =>
    1.23 -          Some(Text.Info(snapshot.convert(info_range), elem))
    1.24 -
    1.25          case Text.Info(info_range, elem) =>
    1.26 -          if (elem.name == Markup.BROWSER ||
    1.27 -              elem.name == Markup.GRAPHVIEW ||
    1.28 -              elem.name == Markup.SENDBACK ||
    1.29 -              elem.name == Markup.SIMP_TRACE)
    1.30 -            Some(Text.Info(snapshot.convert(info_range), elem))
    1.31 -          else None
    1.32 +          if (elem.name == Markup.DIALOG) {
    1.33 +            elem match {
    1.34 +              case Protocol.Dialog(_, serial, _)
    1.35 +              if !command_state.results.defined(serial) =>
    1.36 +                Some(Text.Info(snapshot.convert(info_range), elem))
    1.37 +              case _ => None
    1.38 +            }
    1.39 +          }
    1.40 +          else Some(Text.Info(snapshot.convert(info_range), elem))
    1.41        }) match { case Text.Info(_, info) :: _ => Some(info) case _ => None }
    1.42  
    1.43  
    1.44 @@ -556,21 +555,18 @@
    1.45        snapshot.cumulate_markup[Int](range, 0, line_background_elements, _ =>
    1.46          {
    1.47            case (pri, Text.Info(_, elem)) =>
    1.48 -            val name = elem.name
    1.49 -            if (name == Markup.INFORMATION)
    1.50 +            if (elem.name == Markup.INFORMATION)
    1.51                Some(pri max Rendering.information_pri)
    1.52 -            else if (name == Markup.WRITELN_MESSAGE || name == Markup.TRACING_MESSAGE ||
    1.53 -                elem.name == Markup.WARNING_MESSAGE || name == Markup.ERROR_MESSAGE)
    1.54 -              Some(pri max Rendering.message_pri(name))
    1.55 -            else None
    1.56 +            else
    1.57 +              Some(pri max Rendering.message_pri(elem.name))
    1.58          })
    1.59      val pri = (0 /: results) { case (p1, Text.Info(_, p2)) => p1 max p2 }
    1.60  
    1.61 -    val is_separator = pri > 0 &&
    1.62 +    val is_separator =
    1.63 +      pri > 0 &&
    1.64        snapshot.cumulate_markup[Boolean](range, false, Set(Markup.SEPARATOR), _ =>
    1.65          {
    1.66 -          case (_, Text.Info(_, elem)) =>
    1.67 -            if (elem.name == Markup.SEPARATOR) Some(true) else None
    1.68 +          case _ => Some(true)
    1.69          }).exists(_.info)
    1.70  
    1.71      message_colors.get(pri).map((_, is_separator))
    1.72 @@ -626,19 +622,11 @@
    1.73  
    1.74  
    1.75    def background2(range: Text.Range): List[Text.Info[Color]] =
    1.76 -    snapshot.select_markup(range, Set(Markup.TOKEN_RANGE), _ =>
    1.77 -      {
    1.78 -        case Text.Info(_, elem) =>
    1.79 -          if (elem.name == Markup.TOKEN_RANGE) Some(light_color) else None
    1.80 -      })
    1.81 +    snapshot.select_markup(range, Set(Markup.TOKEN_RANGE), _ => _ => Some(light_color))
    1.82  
    1.83  
    1.84    def bullet(range: Text.Range): List[Text.Info[Color]] =
    1.85 -    snapshot.select_markup(range, Set(Markup.BULLET), _ =>
    1.86 -      {
    1.87 -        case Text.Info(_, elem) =>
    1.88 -          if (elem.name == Markup.BULLET) Some(bullet_color) else None
    1.89 -      })
    1.90 +    snapshot.select_markup(range, Set(Markup.BULLET), _ => _ => Some(bullet_color))
    1.91  
    1.92  
    1.93    private val foreground_elements =