equal
deleted
inserted
replaced
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): |