+ return;
+ }
+ lastSearchResults = results;
+
+ if (av.isFollowHighlight())
+ {
+ /*
+ * if scrollToPosition requires a scroll adjustment, this flag prevents
+ * another scroll event being propagated back to the originator
+ *
+ * @see AlignmentPanel#adjustmentValueChanged
+ */
+ ap.setDontScrollComplement(true);