Show More
@@ -175,6 +175,7 class ConsoleWidget(editwindow.EditWindow): | |||
|
175 | 175 | current_time = time.time() |
|
176 | 176 | if current_time - self._last_refresh_time > 0.03: |
|
177 | 177 | wx.Yield() |
|
178 | # self.ProcessEvent(wx.PaintEvent()) | |
|
178 | 179 | self._last_refresh_time = current_time |
|
179 | 180 | |
|
180 | 181 |
@@ -320,7 +320,8 class WxController(ConsoleWidget, PrefilterFrontEnd): | |||
|
320 | 320 | def show_traceback(self): |
|
321 | 321 | start_line = self.GetCurrentLine() |
|
322 | 322 | PrefilterFrontEnd.show_traceback(self) |
|
323 | wx.Yield() | |
|
323 | self.ProcessEvent(wx.PaintEvent()) | |
|
324 | #wx.Yield() | |
|
324 | 325 | for i in range(start_line, self.GetCurrentLine()): |
|
325 | 326 | self._markers[i] = self.MarkerAdd(i, _ERROR_MARKER) |
|
326 | 327 |
General Comments 0
You need to be logged in to leave comments.
Login now