String property = jEdit.getProperty("mode." + name + "." + key); if(property != null) { Object value; try { value = new Integer(property); } catch(NumberFormatException nf) { value = property; } return value; }
	public Object getProperty(String key)	{		return props.get(key);	}