From: hansonr <hansonr@STO24954W.ad.stolaf.edu>
Date: Sun, 18 Nov 2018 06:56:58 +0000 (-0600)
Subject: adds JS hook for JTable repaint
X-Git-Tag: Release_2_11_4_0~45^2~18^2~386
X-Git-Url: http://source.jalview.org/gitweb/?a=commitdiff_plain;h=ddbc2166fb6d75ceb356c48b1bf4f951ce042beb;p=jalview.git

adds JS hook for JTable repaint
---

diff --git a/src/jalview/gui/FeatureSettings.java b/src/jalview/gui/FeatureSettings.java
index 7b708ab..6046a2e 100644
--- 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
     {