src/Tools/jEdit/src/rendering.scala
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)) =>