editors/Viewer.py
changeset 1208 d22fcdfae8d0
parent 1205 638d1d430d24
child 1224 30e72bc7d21b
equal deleted inserted replaced
1207:fb9799a0c0f7 1208:d22fcdfae8d0
   737         return dc
   737         return dc
   738     
   738     
   739     def RefreshRect(self, rect, eraseBackground=True):
   739     def RefreshRect(self, rect, eraseBackground=True):
   740         self.Editor.RefreshRect(rect, eraseBackground)
   740         self.Editor.RefreshRect(rect, eraseBackground)
   741     
   741     
   742     def RefreshEditor(self):
       
   743         self.Editor.Thaw()
       
   744         self.Editor.Refresh()
       
   745     
       
   746     def Scroll(self, x, y):
   742     def Scroll(self, x, y):
   747         if self.Debug and wx.Platform == '__WXMSW__':
   743         if self.Debug and wx.Platform == '__WXMSW__':
   748             self.Editor.Freeze()
   744             self.Editor.Freeze()
   749         self.Editor.Scroll(x, y)
   745         self.Editor.Scroll(x, y)
   750         if self.Debug:
   746         if self.Debug:
   751             if wx.Platform == '__WXMSW__':
   747             if wx.Platform == '__WXMSW__':
   752                 wx.CallAfter(self.RefreshEditor)
   748                 self.Editor.Thaw()
   753             else:
   749             else:
   754                 self.Editor.Refresh()
   750                 self.Editor.Refresh()
   755     
   751     
   756     def GetScrollPos(self, orientation):
   752     def GetScrollPos(self, orientation):
   757         return self.Editor.GetScrollPos(orientation)
   753         return self.Editor.GetScrollPos(orientation)
  3323         if self.Editor.HasCapture() and self.StartMousePos:
  3319         if self.Editor.HasCapture() and self.StartMousePos:
  3324             return
  3320             return
  3325         if wx.Platform == '__WXMSW__':
  3321         if wx.Platform == '__WXMSW__':
  3326             wx.CallAfter(self.RefreshVisibleElements)
  3322             wx.CallAfter(self.RefreshVisibleElements)
  3327             self.Editor.Freeze()
  3323             self.Editor.Freeze()
  3328             wx.CallAfter(self.RefreshEditor)
  3324             wx.CallAfter(self.Editor.Thaw)
  3329         elif event.GetOrientation() == wx.HORIZONTAL:
  3325         elif event.GetOrientation() == wx.HORIZONTAL:
  3330             self.RefreshVisibleElements(xp = event.GetPosition())
  3326             self.RefreshVisibleElements(xp = event.GetPosition())
  3331         else:
  3327         else:
  3332             self.RefreshVisibleElements(yp = event.GetPosition())
  3328             self.RefreshVisibleElements(yp = event.GetPosition())
  3333         
  3329