console view: distinguish scrolls for different offsets; requests from heavy filters

This commit is contained in:
anna
2012-03-12 18:31:29 +01:00
parent c772e74631
commit da8dc073d5
@@ -331,7 +331,8 @@ public class ConsoleViewImpl extends JPanel implements ConsoleView, ObservableCo
public void scrollTo(final int offset) {
if (myEditor == null) return;
final MyFlushRunnable scrollRunnable = new MyFlushRunnable() {
class ScrollRunnable extends MyFlushRunnable {
private int myOffset = offset;
public void doRun() {
flushDeferredText();
if (myEditor == null) return;
@@ -342,8 +343,13 @@ public class ConsoleViewImpl extends JPanel implements ConsoleView, ObservableCo
myEditor.getCaretModel().moveToOffset(moveOffset);
myEditor.getScrollingModel().scrollToCaret(ScrollType.MAKE_VISIBLE);
}
};
addFlushRequest(scrollRunnable);
@Override
public boolean equals(Object o) {
return super.equals(o) && myOffset == ((ScrollRunnable)o).myOffset;
}
}
addFlushRequest(new ScrollRunnable());
}
public void requestScrollingToEnd() {
@@ -897,6 +903,11 @@ public class ConsoleViewImpl extends JPanel implements ConsoleView, ObservableCo
if (myHeavyUpdateTicket != currentValue) return;
myHyperlinks.adjustHighlighters(Collections.singletonList(additionalHighlight));
}
@Override
public boolean equals(Object o) {
return this == o && super.equals(o);
}
});
}
});