# Sample extension: zoom a window to maximum height
('_Zoom Height', '<<zoom-height>>'),
def __init__(self
, editwin
):
def zoom_height_event(self
, event
):
m
= re
.match(r
"(\d+)x(\d+)\+(-?\d+)\+(-?\d+)", geom
)
width
, height
, x
, y
= map(int, m
.groups())
newheight
= top
.winfo_screenheight()
if sys
.platform
== 'win32':
newheight
= newheight
- 72
#newheight = newheight - 96
newheight
= newheight
- 88
newgeom
= "%dx%d+%d+%d" % (width
, newheight
, x
, newy
)