*/
public void updateLayout()
{
- fontChanged();
+ fontChanged(); // fires repaint
setAnnotationVisible(av.isShowAnnotation());
boolean wrap = av.getWrapAlignment();
ViewportRanges ranges = av.getRanges();
@Override
public void paintComponent(Graphics g)
{
+
invalidate(); // needed so that the id width adjuster works correctly
Dimension d = getIdPanel().getIdCanvas().getPreferredSize();
overviewPanel.canvas.finalizeDraw(miniMe);
}
+
+ private boolean holdRepaint = false;
+
+ public boolean getHoldRepaint()
+ {
+ return holdRepaint;
+ }
+
+ public void setHoldRepaint(boolean b)
+ {
+ if (holdRepaint == b)
+ {
+ return;
+ }
+ holdRepaint = b;
+ if (!b)
+ {
+ repaint();
+ }
+ }
+
+ @Override
+ public void repaint()
+ {
+ if (holdRepaint)
+ {
+ // System.out.println("AP repaint holding");
+ // Platform.stackTrace();
+ return;
+ }
+ super.repaint();
+ }
+
}