function onMouseOver(style) {
size = style.getProperty("font-size");
isize = getSizeInPoint(size);
if (size <= 20) {
style.setProperty("font-size", (size+1) + "pt");
}
}
function onMouseOver(style) {
size = style.getPropertyCSSValue("font-size");
isize = size.getFloatValue(POINT);
if (isize <= 20) {
size.setFloatValue(isize+1, POINT);
}
}