/*
 * sets font size to 9
 *
 */

jEdit.setIntegerProperty("view.fontsize",9);
jEdit.propertiesChanged();