From da8dc073d5c480998b111ebcb585167fa1852b36 Mon Sep 17 00:00:00 2001 From: anna Date: Mon, 12 Mar 2012 18:29:30 +0100 Subject: [PATCH] console view: distinguish scrolls for different offsets; requests from heavy filters --- .../execution/impl/ConsoleViewImpl.java | 17 ++++++++++++++--- 1 file changed, 14 insertions(+), 3 deletions(-) diff --git a/platform/lang-impl/src/com/intellij/execution/impl/ConsoleViewImpl.java b/platform/lang-impl/src/com/intellij/execution/impl/ConsoleViewImpl.java index a29cb33d1baf..debad04a65d1 100644 --- a/platform/lang-impl/src/com/intellij/execution/impl/ConsoleViewImpl.java +++ b/platform/lang-impl/src/com/intellij/execution/impl/ConsoleViewImpl.java @@ -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); + } }); } });