public void setLineNumeration(EditorSettings.LineNumerationType val) {
    EditorSettings.LineNumerationType old = myOptions.LINE_NUMERATION;
    if (old == val) return;
    myOptions.LINE_NUMERATION = val;
    myPropertyChangeSupport.firePropertyChange(PropNames.PROP_LINE_NUMERATION, old, val);

  }
public void setLineNumeration(EditorSettings.LineNumerationType val)