From 0119f8395afec0eb19b906dc12944f4e82ac48cd Mon Sep 17 00:00:00 2001
From: gmungoc <g.m.carstairs@dundee.ac.uk>
Date: Tue, 18 Dec 2018 17:58:12 +0000
Subject: [PATCH] JAL-3032 revert table repaint customisations

---
 src/jalview/gui/FeatureSettings.java |   29 +++--------------------------
 1 file changed, 3 insertions(+), 26 deletions(-)

diff --git a/src/jalview/gui/FeatureSettings.java b/src/jalview/gui/FeatureSettings.java
index 33ab037..ea0d914 100644
--- a/src/jalview/gui/FeatureSettings.java
+++ b/src/jalview/gui/FeatureSettings.java
@@ -342,7 +342,7 @@ public class FeatureSettings extends JPanel
             data[i + direction] = temp;
           }
           updateFeatureRenderer(data);
-          repaintTable();
+          table.repaint();
           selectedRow = newRow;
         }
       }
@@ -973,7 +973,7 @@ public class FeatureSettings extends JPanel
                 .getData();
         ensureOrder(data);
         updateFeatureRenderer(data, false);
-        repaintTable();
+        table.repaint();
       }
     } catch (Exception ex)
     {
@@ -1087,7 +1087,7 @@ public class FeatureSettings extends JPanel
       data[i][SHOW_COLUMN] = !(Boolean) data[i][SHOW_COLUMN];
     }
     updateFeatureRenderer(data, true);
-    repaintTable();
+    table.repaint();
   }
 
   public void orderByAvWidth()
@@ -1153,29 +1153,6 @@ public class FeatureSettings extends JPanel
     table.repaint();
   }
 
-  /**
-   * Repaints the table using alternative code for Java and J2S
-   */
-  private void repaintTable() 
-  {
-	  table.repaint();
-//	  if (true)
-//		  return;
-//	// 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$();
-//	 */
-//	{
-//	}
-  }
-
   public void close()
   {
     try
-- 
1.7.10.2