/*
 * sets font size one larger
 *
 */

size = jEdit.getIntegerProperty("view.fontsize",10);
size += 1;
jEdit.setIntegerProperty("view.fontsize",size);
jEdit.propertiesChanged();