From 39b37500f9301122111be3239572f925ca18018e Mon Sep 17 00:00:00 2001 From: hansonr Date: Tue, 18 Dec 2018 08:32:23 -0600 Subject: [PATCH] removing special needs for JavaScript table repainting --- src/jalview/gui/FeatureSettings.java | 30 +++++++++++++++--------------- 1 file changed, 15 insertions(+), 15 deletions(-) diff --git a/src/jalview/gui/FeatureSettings.java b/src/jalview/gui/FeatureSettings.java index 9a0114a..33ab037 100644 --- a/src/jalview/gui/FeatureSettings.java +++ b/src/jalview/gui/FeatureSettings.java @@ -1158,22 +1158,22 @@ public class FeatureSettings extends JPanel */ private void repaintTable() { - 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$(); - */ - { 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() -- 1.7.10.2