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