--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/pgconsole/panedext.py Tue Aug 16 23:53:54 2011 +0200
@@ -0,0 +1,61 @@
+import gtk
+
+
+class PanedExt(gtk.Paned):
+ """Extended gtk.Paned (abstract)
+
+ set_snap1(int), set_snap2(int)
+ set minimum size of child widget
+ if the handle is moved to the edge, child widget is hidden
+ """
+ def __init__(self):
+ self.connect('notify::position', self.on_position_change)
+ self.min1 = 0
+ self.min2 = 0
+
+
+ def set_snap1(self, minpos):
+ self.min1 = minpos
+
+
+ def set_snap2(self, minpos):
+ self.min2 = minpos
+
+
+ def on_position_change(self, w, scrolltype):
+ if self.allocation[0] == -1:
+ return False
+
+ pos = self.get_position()
+ maxpos = self.get_property('max-position')
+
+ if self.min1:
+ if pos > 0 and pos < self.min1:
+ if pos < self.min1 / 2:
+ self.set_position(0)
+ else:
+ self.set_position(self.min1)
+ return True
+
+ if self.min2:
+ if pos > maxpos - self.min2 and pos < maxpos:
+ if pos > maxpos - self.min2 / 2:
+ self.set_position(maxpos)
+ else:
+ self.set_position(maxpos - self.min2)
+ return True
+
+ return False
+
+
+class HPanedExt(gtk.HPaned, PanedExt):
+ def __init__(self):
+ gtk.HPaned.__init__(self)
+ PanedExt.__init__(self)
+
+
+class VPanedExt(gtk.VPaned, PanedExt):
+ def __init__(self):
+ gtk.VPaned.__init__(self)
+ PanedExt.__init__(self)
+