py_ext/PythonEditor.py
changeset 734 5c42cafaee15
parent 721 ecf4d203c4d4
child 738 413946c04c87
equal deleted inserted replaced
733:915be999f3f0 734:5c42cafaee15
     1 import  wx, wx.grid
     1 import  wx, wx.grid
     2 import  wx.stc  as  stc
     2 import  wx.stc  as  stc
     3 import keyword
     3 import keyword
       
     4 
       
     5 from util import opjimg
     4 
     6 
     5 from controls import EditorPanel
     7 from controls import EditorPanel
     6 
     8 
     7 if wx.Platform == '__WXMSW__':
     9 if wx.Platform == '__WXMSW__':
     8     faces = { 'times': 'Times New Roman',
    10     faces = { 'times': 'Times New Roman',
   232         EditorPanel.__init__(self, parent, "", window, controler)
   234         EditorPanel.__init__(self, parent, "", window, controler)
   233         
   235         
   234         self.DisableEvents = False
   236         self.DisableEvents = False
   235         self.CurrentAction = None
   237         self.CurrentAction = None
   236         
   238         
   237         img = wx.Bitmap(self.Controler.GetIconPath("Cfile.png"), wx.BITMAP_TYPE_PNG).ConvertToImage()
   239         self.SetIcon(wx.Bitmap(opjimg("Cfile")))
   238         self.SetIcon(wx.BitmapFromImage(img.Rescale(16, 16)))
       
   239     
   240     
   240     def __del__(self):
   241     def __del__(self):
   241         self.Controler.OnCloseEditor(self)
   242         self.Controler.OnCloseEditor(self)
   242     
   243     
   243     def GetTitle(self):
   244     def GetTitle(self):