I concur with your comment in console_widget.py that the _on_key_down (and possibly other similar functions) might best be implemented with a dict-based callback mechanism. But since that would be a more invasive change, we can postpone that thought for now.
Otherwise the fix looks good. I'll wait 48 hours on this and if nobody notices a problem and objects, I'll merge it into trunk for 0.10.
Only question: can you let me know if there are any open tickets that I should close when merging?
It looks fine to me, thanks.
I concur with your comment in console_widget.py that the _on_key_down (and possibly other similar functions) might best be implemented with a dict-based callback mechanism. But since that would be a more invasive change, we can postpone that thought for now.
Otherwise the fix looks good. I'll wait 48 hours on this and if nobody notices a problem and objects, I'll merge it into trunk for 0.10.
Only question: can you let me know if there are any open tickets that I should close when merging?