Show More
@@ -175,6 +175,7 class ConsoleWidget(editwindow.EditWindow): | |||||
175 | current_time = time.time() |
|
175 | current_time = time.time() | |
176 | if current_time - self._last_refresh_time > 0.03: |
|
176 | if current_time - self._last_refresh_time > 0.03: | |
177 | wx.Yield() |
|
177 | wx.Yield() | |
|
178 | # self.ProcessEvent(wx.PaintEvent()) | |||
178 | self._last_refresh_time = current_time |
|
179 | self._last_refresh_time = current_time | |
179 |
|
180 | |||
180 |
|
181 |
@@ -320,7 +320,8 class WxController(ConsoleWidget, PrefilterFrontEnd): | |||||
320 | def show_traceback(self): |
|
320 | def show_traceback(self): | |
321 | start_line = self.GetCurrentLine() |
|
321 | start_line = self.GetCurrentLine() | |
322 | PrefilterFrontEnd.show_traceback(self) |
|
322 | PrefilterFrontEnd.show_traceback(self) | |
323 | wx.Yield() |
|
323 | self.ProcessEvent(wx.PaintEvent()) | |
|
324 | #wx.Yield() | |||
324 | for i in range(start_line, self.GetCurrentLine()): |
|
325 | for i in range(start_line, self.GetCurrentLine()): | |
325 | self._markers[i] = self.MarkerAdd(i, _ERROR_MARKER) |
|
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