--- a/Viewer.py Mon Sep 17 17:51:05 2007 +0200
+++ b/Viewer.py Tue Sep 18 18:05:52 2007 +0200
@@ -192,7 +192,8 @@
dc = wx.BufferedPaintDC(self)
else:
dc = wx.ClientDC(self)
- dc.SetFont(wx.NORMAL_FONT)
+ if wx.Platform != '__WXMSW__':
+ dc.SetFont(wx.NORMAL_FONT)
self.DoPrepareDC(dc)
return dc
@@ -305,6 +306,10 @@
self.RefreshScrollBars()
self.Refresh(False)
+ def Scroll(self, x, y):
+ print "Scroll to (%d, %d)"%(x, y)
+ wx.ScrolledWindow.Scroll(self, x, y)
+
def RefreshScrollBars(self):
xstart, ystart = self.GetViewStart()
window_size = self.GetClientSize()
@@ -321,8 +326,8 @@
maxx = max(maxx, extent.x + extent.width)
maxy = max(maxy, extent.y + extent.height)
self.SetScrollbars(SCROLLBAR_UNIT, SCROLLBAR_UNIT,
- maxx / SCROLLBAR_UNIT, maxy / SCROLLBAR_UNIT, xstart, ystart)
-
+ maxx / SCROLLBAR_UNIT, maxy / SCROLLBAR_UNIT, xstart, ystart, True)
+
# Load instance from given informations
def loadInstance(self, instance, ids):
ids.append(instance["id"])
@@ -926,6 +931,7 @@
self.SelectedElement.OnMotion(event, dc, self.Scaling)
self.SelectedElement.GeneratePoints()
self.Refresh(False)
+ self.UpdateScrollPos(event)
event.Skip()
def UpdateScrollPos(self, event):