editors/ResourceEditor.py
branchpython3
changeset 3765 88fe6fc9fd38
parent 3752 9f6f46dbe3ae
equal deleted inserted replaced
3764:d92c1a3dafa7 3765:88fe6fc9fd38
   389         self.InstancesTable.ResetView(self.InstancesGrid)
   389         self.InstancesTable.ResetView(self.InstancesGrid)
   390         self.InstancesGrid.RefreshButtons()
   390         self.InstancesGrid.RefreshButtons()
   391 
   391 
   392         self.TasksGrid.SetFocus()
   392         self.TasksGrid.SetFocus()
   393 
   393 
   394     def __del__(self):
       
   395         self.RefreshHighlightsTimer.Stop()
       
   396 
       
   397     def RefreshTypeList(self):
   394     def RefreshTypeList(self):
   398         self.TypeList = []
   395         self.TypeList = []
   399         blocktypes = self.Controler.GetBlockResource()
   396         blocktypes = self.Controler.GetBlockResource()
   400         for blocktype in blocktypes:
   397         for blocktype in blocktypes:
   401             self.TypeList.append(blocktype)
   398             self.TypeList.append(blocktype)