diff -r 1f46424c6220 -r 5a0b439cf576 editors/CodeFileEditor.py --- a/editors/CodeFileEditor.py Wed May 08 23:13:10 2013 +0200 +++ b/editors/CodeFileEditor.py Wed May 08 23:31:12 2013 +0200 @@ -195,7 +195,7 @@ text += section_comments["end"] return text - def RefreshView(self): + def RefreshView(self, scroll_to_highlight=False): self.ResetBuffer() self.DisableEvents = True old_cursor_pos = self.GetCurrentPos() @@ -203,8 +203,8 @@ column = self.GetXOffset() old_text = self.GetText() new_text = self.GetCodeText() - self.SetText(new_text) if old_text != new_text: + self.SetText(new_text) new_cursor_pos = GetCursorPos(old_text, new_text) self.LineScroll(column, line) if new_cursor_pos != None: @@ -431,6 +431,8 @@ self.CurrentFindHighlight = self.SearchResults[0] self.AddHighlight(*self.CurrentFindHighlight) + self.ScrollToLine(self.CurrentFindHighlight[0][0]) + else: if self.CurrentFindHighlight is not None: self.RemoveHighlight(*self.CurrentFindHighlight) @@ -441,7 +443,7 @@ #------------------------------------------------------------------------------- def OnRefreshHighlightsTimer(self, event): - self.RefreshView() + self.RefreshView(True) event.Skip() def ClearHighlights(self, highlight_type=None):