From 3e85e0bc8df23e09495f57089ec6e26d2552efa5 Mon Sep 17 00:00:00 2001
From: gmungoc <g.m.carstairs@dundee.ac.uk>
Date: Tue, 11 Aug 2020 10:35:32 +0100
Subject: [PATCH] JAL-3371 more fine-grained slider; set Param slider to
 initial default

---
 src/jalview/gui/OptsAndParamsPage.java |    8 +++++---
 src/jalview/gui/Slider.java            |    8 +++++++-
 2 files changed, 12 insertions(+), 4 deletions(-)

diff --git a/src/jalview/gui/OptsAndParamsPage.java b/src/jalview/gui/OptsAndParamsPage.java
index 0f4d0e7..92b612a 100644
--- a/src/jalview/gui/OptsAndParamsPage.java
+++ b/src/jalview/gui/OptsAndParamsPage.java
@@ -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);
diff --git a/src/jalview/gui/Slider.java b/src/jalview/gui/Slider.java
index 7f18461..714e770 100644
--- a/src/jalview/gui/Slider.java
+++ b/src/jalview/gui/Slider.java
@@ -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);
-- 
1.7.10.2