ViewManager/ViewManager.py

changeset 832
eb5ff61f927b
parent 826
2e3e2055e715
child 880
52ed20236a1c
diff -r f046b97785db -r eb5ff61f927b ViewManager/ViewManager.py
--- a/ViewManager/ViewManager.py	Sun Jan 09 14:25:16 2011 +0100
+++ b/ViewManager/ViewManager.py	Sun Jan 09 18:16:46 2011 +0100
@@ -3099,7 +3099,8 @@
             
         self.__setSbFile()
         
-    def openSourceFile(self, fn, lineno = None, filetype = "", selStart = 0, selEnd = 0):
+    def openSourceFile(self, fn, lineno = None, filetype = "", 
+                       selStart = 0, selEnd = 0, pos = 0):
         """
         Public slot to display a file in an editor.
         
@@ -3120,7 +3121,7 @@
         
         if lineno is not None and lineno >= 0:
             editor.ensureVisibleTop(lineno)
-            editor.gotoLine(lineno)
+            editor.gotoLine(lineno, pos)
         
         if selStart != selEnd:
             editor.setSelection(lineno - 1, selStart, lineno - 1, selEnd)

eric ide

mercurial