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