src/jalview/gui/PaintRefresher.java

   1 package jalview.gui;\r
   2 import java.awt.*;\r
   3 import java.util.*;\r
   4 \r
   5 public class PaintRefresher\r
   6 {\r
   7   static Vector containers = new Vector();\r
   8 \r
   9   public static void Register(Container c)\r
  10   {\r
  11     if(!containers.contains(c))\r
  12       containers.add(c);\r
  13     else\r
  14       containers.remove(c);\r
  15   }\r
  16 \r
  17   public static void Refresh(Container c)\r
  18   {\r
  19     Container temp;\r
  20     Enumeration e = containers.elements();\r
  21     while( e.hasMoreElements() )\r
  22     {\r
  23       temp = (Container)e.nextElement();\r
  24 \r
  25       if(!temp.isValid())\r
  26         containers.removeElement( temp );\r
  27       else if( temp == c )\r
  28            continue;\r
  29 \r
  30       temp.repaint();\r
  31     }\r
  32 \r
  33   }\r
  34 \r
  35 }\r