adds JS hook for JTable repaint

diff --git a/src/jalview/gui/FeatureSettings.java b/src/jalview/gui/FeatureSettings.java
index 7b708ab..6046a2e 100644 (file)
--- a/src/jalview/gui/FeatureSettings.java
+++ b/src/jalview/gui/FeatureSettings.java
@@ -343,7 +343,7 @@ public class FeatureSettings extends JPanel
             data[i + direction] = temp;
           }
           updateFeatureRenderer(data);
-          table.repaint();
+          repaintTable();
           selectedRow = newRow;
         }
       }
@@ -964,7 +964,7 @@ public class FeatureSettings extends JPanel
                 .getData();
         ensureOrder(data);
         updateFeatureRenderer(data, false);
-        table.repaint();
+        repaintTable();
       }
     } catch (Exception ex)
     {
@@ -1078,7 +1078,7 @@ public class FeatureSettings extends JPanel
       data[i][SHOW_COLUMN] = !(Boolean) data[i][SHOW_COLUMN];
     }
     updateFeatureRenderer(data, true);
-    table.repaint();
+    repaintTable();
   }
 
   public void orderByAvWidth()
@@ -1141,10 +1141,29 @@ public class FeatureSettings extends JPanel
     }
 
     updateFeatureRenderer(data, false);
-    table.repaint();
+    repaintTable();
   }
 
-  public void close()
+
+       private void repaintTable() {
+               // BH 2018
+               // Here is a needed intervention
+               // because generally we don't "repaint"
+               // the table. We re-create the HTML divs
+               // that is associated with it. A better
+               // way to do this would be to fire a property change.
+
+               @SuppressWarnings("unused")
+               TableUI ui = table.getUI();
+               /**
+                * @j2sNative ui.repaintTable$();
+                */
+               {
+                       table.repaint();
+               }
+       }
+
+public void close()
   {
     try
     {