/*
 * sets font size one small
 *
 */

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