static JSpinner jspinner_disableDigitGrouping(final JSpinner spinner) {
  if (spinner != null) swing {
    spinner.setEditor(new JSpinner.NumberEditor(spinner, "#"));
  }
  ret spinner;
}