src/Tools/jEdit/src/rendering.scala
changeset 52081 29566b6810f7
parent 51588 167e2d64327a
child 52101 7679178b0aa5
     1.1 --- a/src/Tools/jEdit/src/rendering.scala	Mon May 20 13:38:48 2013 +0200
     1.2 +++ b/src/Tools/jEdit/src/rendering.scala	Mon May 20 13:54:24 2013 +0200
     1.3 @@ -481,17 +481,12 @@
     1.4                  (None, Some(bad_color))
     1.5                case (_, Text.Info(_, XML.Elem(Markup(Markup.INTENSIFY, _), _))) =>
     1.6                  (None, Some(intensify_color))
     1.7 -              case (acc, Text.Info(_, elem @ XML.Elem(Markup(Markup.DIALOG, _), _))) =>
     1.8 -                // FIXME pattern match problem in scala-2.9.2 (!??)
     1.9 -                elem match {
    1.10 -                  case Protocol.Dialog(_, serial, result) =>
    1.11 -                    command_state.results.get(serial) match {
    1.12 -                      case Some(Protocol.Dialog_Result(res)) if res == result =>
    1.13 -                        (None, Some(active_result_color))
    1.14 -                      case _ =>
    1.15 -                        (None, Some(active_color))
    1.16 -                    }
    1.17 -                  case _ => acc
    1.18 +              case (acc, Text.Info(_, Protocol.Dialog(_, serial, result))) =>
    1.19 +                command_state.results.get(serial) match {
    1.20 +                  case Some(Protocol.Dialog_Result(res)) if res == result =>
    1.21 +                    (None, Some(active_result_color))
    1.22 +                  case _ =>
    1.23 +                    (None, Some(active_color))
    1.24                  }
    1.25                case (_, Text.Info(_, XML.Elem(markup, _))) if active_include(markup.name) =>
    1.26                  (None, Some(active_color))