Fix slightly uneven splits on shortcut due to handle size, though this will make previously saved layouts off by a few pixels (Steve Boddy, LP#1089162)

This commit is contained in:
Stephen Boddy 2015-07-15 20:05:12 +02:00
parent 45215ef5a6
commit a8865b17ee
1 changed files with 4 additions and 2 deletions

View File

@ -390,10 +390,12 @@ class Paned(Container):
self.set_position(self.get_position()) self.set_position(self.get_position())
def set_position_by_ratio(self): def set_position_by_ratio(self):
self.set_pos(int(self.ratio*self.get_length())) handle_size = self.style_get_property('handle-size')
self.set_pos(int((self.ratio*self.get_length())-(handle_size/2.0)))
def set_position(self, pos): def set_position(self, pos):
self.ratio = float(pos) / self.get_length() handle_size = self.style_get_property('handle-size')
self.ratio = float(pos + (handle_size/2.0)) / self.get_length()
self.set_pos(pos) self.set_pos(pos)
class HPaned(Paned, gtk.HPaned): class HPaned(Paned, gtk.HPaned):