--- 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"]
+ def RefreshView(self, scroll_to_highlight=False): self.DisableEvents = True
old_cursor_pos = self.GetCurrentPos()
@@ -203,8 +203,8 @@
column = self.GetXOffset()
old_text = self.GetText()
new_text = self.GetCodeText()
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]) if self.CurrentFindHighlight is not None:
self.RemoveHighlight(*self.CurrentFindHighlight)
@@ -441,7 +443,7 @@
#-------------------------------------------------------------------------------
def OnRefreshHighlightsTimer(self, event):
def ClearHighlights(self, highlight_type=None):