controls/VariablePanel.py
branchpython3
changeset 3765 88fe6fc9fd38
parent 3764 d92c1a3dafa7
child 3789 8def429216ca
equal deleted inserted replaced
3764:d92c1a3dafa7 3765:88fe6fc9fd38
   683             if (panel_width > self.PanelWidthMin) and not self.ColSettings["fixed_size"][col]:
   683             if (panel_width > self.PanelWidthMin) and not self.ColSettings["fixed_size"][col]:
   684                 self.VariablesGrid.SetColSize(col, int((self.ColSettings["size"][col]/stretch_cols_sum)*stretch_cols_width))
   684                 self.VariablesGrid.SetColSize(col, int((self.ColSettings["size"][col]/stretch_cols_sum)*stretch_cols_width))
   685             else:
   685             else:
   686                 self.VariablesGrid.SetColSize(col, self.ColSettings["size"][col])
   686                 self.VariablesGrid.SetColSize(col, self.ColSettings["size"][col])
   687 
   687 
   688     def __del__(self):
       
   689         self.RefreshHighlightsTimer.Stop()
       
   690 
       
   691     def SetTagName(self, tagname):
   688     def SetTagName(self, tagname):
   692         self.TagName = tagname
   689         self.TagName = tagname
   693         self.BodyType = self.Controler.GetEditedElementBodyType(self.TagName)
   690         self.BodyType = self.Controler.GetEditedElementBodyType(self.TagName)
   694 
   691 
   695     def GetTagName(self):
   692     def GetTagName(self):