editors/Viewer.py
changeset 1042 6dbdc6844eb9
parent 980 c7ba67d01d65
child 1057 3837e165b3f9
equal deleted inserted replaced
1041:736ec395399a 1042:6dbdc6844eb9
  2039                         movey *= 10
  2039                         movey *= 10
  2040                 self.SelectedElement.Move(movex, movey)
  2040                 self.SelectedElement.Move(movex, movey)
  2041                 self.StartBuffering()
  2041                 self.StartBuffering()
  2042                 self.SelectedElement.RefreshModel()
  2042                 self.SelectedElement.RefreshModel()
  2043                 self.RefreshScrollBars()
  2043                 self.RefreshScrollBars()
       
  2044                 self.RefreshVisibleElements()
  2044                 self.RefreshRect(self.GetScrolledRect(self.SelectedElement.GetRedrawRect(movex, movey)), False)
  2045                 self.RefreshRect(self.GetScrolledRect(self.SelectedElement.GetRedrawRect(movex, movey)), False)
  2045         elif not self.Debug and keycode == wx.WXK_SPACE and self.SelectedElement is not None and self.SelectedElement.Dragging:
  2046         elif not self.Debug and keycode == wx.WXK_SPACE and self.SelectedElement is not None and self.SelectedElement.Dragging:
  2046             if self.IsBlock(self.SelectedElement) or self.IsComment(self.SelectedElement):
  2047             if self.IsBlock(self.SelectedElement) or self.IsComment(self.SelectedElement):
  2047                 block = self.CopyBlock(self.SelectedElement, wx.Point(*self.SelectedElement.GetPosition()))
  2048                 block = self.CopyBlock(self.SelectedElement, wx.Point(*self.SelectedElement.GetPosition()))
  2048                 event = wx.MouseEvent()
  2049                 event = wx.MouseEvent()