Fixing Ctrl-Tab and Ctrl-Shift-Tab behaviour

*closes LP#234904
This commit is contained in:
Emmanuel Bretelle 2008-05-26 11:32:08 +01:00
parent 18c62f3132
commit ae922111b0
1 changed files with 8 additions and 5 deletions

View File

@ -635,13 +635,16 @@ text/plain
return (True) return (True)
if keyname and (keyname == 'Tab' or keyname.endswith('_Tab')): if keyname and (keyname == 'Tab' or keyname.endswith('_Tab')):
if event.state == gtk.gdk.CONTROL_MASK: mask = gtk.gdk.CONTROL_MASK | gtk.gdk.SHIFT_MASK
self.terminator.go_next (self)
return (True)
if (event.state & mask) == mask: if (event.state & mask) == mask:
self.terminator.go_prev (self) self.terminator.go_prev (self)
return (True) return (True)
mask = gtk.gdk.CONTROL_MASK
if (event.state & mask) == mask:
self.terminator.go_next (self)
return (True)
# Warning, mask value is either gtk.gdk.CONTROL_MASK or gtk.gdk.CONTROL_MASK | gtk.gdk.SHIFT_MASK
# if you intend to use it, reinit it
return (False) return (False)
def zoom (self, zoom_in): def zoom (self, zoom_in):
@ -986,7 +989,7 @@ class Terminator:
""" """
vertical = pos in ("top", "bottom") vertical = pos in ("top", "bottom")
pane = (vertical) and gtk.VPaned () or gtk.HPaned () pane = (vertical) and gtk.VPaned () or gtk.HPaned ()
# get the parent of the provided terminal # get the parent of the provided terminal
parent = widget.get_parent () parent = widget.get_parent ()