##// END OF EJS Templates
Clean up the title-setting code.
Gael Varoquaux -
Show More
@@ -196,9 +196,14 b' class ConsoleWidget(editwindow.EditWindow):'
196 """ Write given text to buffer, while translating the ansi escape
196 """ Write given text to buffer, while translating the ansi escape
197 sequences.
197 sequences.
198 """
198 """
199 # XXX: do not put print statements in this method, the print
200 # statements will call this method, and you will end up with
201 # an infinit loop
199 title = self.title_pat.split(text)
202 title = self.title_pat.split(text)
200 if len(title)>0:
203 if len(title)>1:
201 self.title = title[-1]
204 import sys
205 print >>sys.__stderr__, "title :", title
206 self.title = title[-2]
202
207
203 text = self.title_pat.sub('', text)
208 text = self.title_pat.sub('', text)
204 segments = self.color_pat.split(text)
209 segments = self.color_pat.split(text)
@@ -241,6 +241,15 b' class WxController(PrefilterFrontEnd, ConsoleWidget):'
241 ConsoleWidget._on_key_up(self, event, skip=skip)
241 ConsoleWidget._on_key_up(self, event, skip=skip)
242
242
243
243
244 def _set_title(self, title):
245 return self.Parent.SetTitle(title)
246
247 def _get_title(self):
248 return self.Parent.GetTitle()
249
250 title = property(_get_title, _set_title)
251
252
244 if __name__ == '__main__':
253 if __name__ == '__main__':
245 class MainWindow(wx.Frame):
254 class MainWindow(wx.Frame):
246 def __init__(self, parent, id, title):
255 def __init__(self, parent, id, title):
General Comments 0
You need to be logged in to leave comments. Login now