: BELOW_THRESHOLD_OPTION);
slider.setEnabled(true);
slider.setValue((int) (fc.getThreshold() * scaleFactor));
- thresholdValue.setText(String.valueOf(getRoundedSliderValue()));
+ float roundedSliderValue = getRoundedSliderValue();
+ thresholdValue.setText(String.valueOf(fc.getThreshold()));// roundedSliderValue));
thresholdValue.setEnabled(true);
thresholdIsMin.setEnabled(true);
}
{
try
{
+ /*
+ * set 'adjusting' flag while moving the slider, so it
+ * doesn't then in turn change the value (with rounding)
+ */
adjusting = true;
float f = Float.parseFloat(thresholdValue.getText());
+ f = Float.max(f, this.min);
+ f = Float.min(f, this.max);
+ thresholdValue.setText(String.valueOf(f));
slider.setValue((int) (f * scaleFactor));
threshline.value = f;
thresholdValue.setBackground(Color.white); // ok
-
- /*
- * force repaint of any Overview window or structure
- */
- ap.paintAlignment(true, true);
+ adjusting = false;
+ colourChanged(true);
} catch (NumberFormatException ex)
{
thresholdValue.setBackground(Color.red); // not ok
- } finally
- {
adjusting = false;
}
}