src/Tools/jEdit/src/rendering.scala
changeset 55649 1532ab0dc67b
parent 55647 106a57dec7af
child 55651 fa42cf3fe79b
     1.1 --- a/src/Tools/jEdit/src/rendering.scala	Fri Feb 21 13:36:40 2014 +0100
     1.2 +++ b/src/Tools/jEdit/src/rendering.scala	Fri Feb 21 15:12:50 2014 +0100
     1.3 @@ -301,7 +301,7 @@
     1.4      if (snapshot.is_outdated) None
     1.5      else {
     1.6        val results =
     1.7 -        snapshot.cumulate_markup[(Protocol.Status, Int)](
     1.8 +        snapshot.cumulate_status[(Protocol.Status, Int)](
     1.9            range, (Protocol.Status.init, 0), Protocol.status_elements, _ =>
    1.10            {
    1.11              case ((status, pri), Text.Info(_, elem)) =>