JAL-3371 more fine-grained slider; set Param slider to initial default
authorgmungoc <g.m.carstairs@dundee.ac.uk>
Tue, 11 Aug 2020 09:35:32 +0000 (10:35 +0100)
committergmungoc <g.m.carstairs@dundee.ac.uk>
Tue, 11 Aug 2020 09:35:32 +0000 (10:35 +0100)
src/jalview/gui/OptsAndParamsPage.java
src/jalview/gui/Slider.java

index 0f4d0e7..92b612a 100644 (file)
@@ -92,7 +92,7 @@ public class OptsAndParamsPage
 
     JLabel optlabel = new JLabel();
 
-    JComboBox val = new JComboBox();
+    JComboBox<String> val = new JComboBox<>();
 
     public OptionBox(OptionI opt)
     {
@@ -126,7 +126,7 @@ public class OptsAndParamsPage
         }
       }
       add(enabled, BorderLayout.NORTH);
-      for (Object str : opt.getPossibleValues())
+      for (String str : opt.getPossibleValues())
       {
         val.addItem(str);
       }
@@ -588,7 +588,7 @@ public class OptsAndParamsPage
       {
         if (choice)
         {
-          choicebox = new JComboBox();
+          choicebox = new JComboBox<>();
           choicebox.addActionListener(this);
           controlPanel.add(choicebox, BorderLayout.CENTER);
         }
@@ -622,7 +622,9 @@ public class OptsAndParamsPage
             }
           });
           valueField.setPreferredSize(new Dimension(60, 25));
+          valueField.setText(parm.getValue());
           slider = makeSlider(parm.getValidValue());
+          updateSliderFromValueField();
           slider.addChangeListener(this);
 
           controlPanel.add(slider, BorderLayout.WEST);
index 7f18461..714e770 100644 (file)
@@ -16,6 +16,12 @@ import javax.swing.JSlider;
 public class Slider extends JSlider
 {
   /*
+   * the number of nominal positions the slider represents
+   * (higher number = more fine-grained positioning)
+   */
+  private static final int SCALE_TICKS = 1000;
+
+  /*
    * 'true' value corresponding to zero on the slider
    */
   private float trueMin;
@@ -57,7 +63,7 @@ public class Slider extends JSlider
     trueMin = min;
     trueMax = max;
     setMinimum(0);
-    sliderScaleFactor = 100f / (max - min);
+    sliderScaleFactor = SCALE_TICKS / (max - min);
     int sliderMax = (int) ((max - min) * sliderScaleFactor);
     setMaximum(sliderMax);
     setSliderValue(value);