From ddbc2166fb6d75ceb356c48b1bf4f951ce042beb Mon Sep 17 00:00:00 2001 From: hansonr Date: Sun, 18 Nov 2018 00:56:58 -0600 Subject: [PATCH] adds JS hook for JTable repaint --- src/jalview/gui/FeatureSettings.java | 29 ++++++++++++++++++++++++----- 1 file changed, 24 insertions(+), 5 deletions(-) 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 { -- 1.7.10.2