equal
deleted
inserted
replaced
64 |
64 |
65 public String getID() {return "";} |
65 public String getID() {return "";} |
66 |
66 |
67 public void setID(String s) {} |
67 public void setID(String s) {} |
68 |
68 |
69 public Dimension getLabelSize(Graphics g) { |
69 public Box getLabelSize(Graphics g) { |
70 FontMetrics fm = g == null ? |
70 AbstractFontMetrics fm = g == null ? |
71 new DefaultFontMetrics(12) : g.getFontMetrics(g.getFont()); |
71 (AbstractFontMetrics) new DefaultFontMetrics(12) : |
|
72 (AbstractFontMetrics) new AWTFontMetrics(g.getFontMetrics(g.getFont())); |
72 |
73 |
73 return new Dimension( |
74 return new Box(Math.max(fm.stringWidth("[. . . .]"), |
74 Math.max(fm.stringWidth("[. . . .]"),fm.stringWidth(getLabel())), |
75 fm.stringWidth(getLabel())), |
75 fm.getAscent()+fm.getDescent()); |
76 fm.getAscent()+fm.getDescent()); |
76 } |
77 } |
77 |
78 |
78 public String getPath() { return "";} |
79 public String getPath() { return "";} |
79 |
80 |
80 public void setPath(String p) {} |
81 public void setPath(String p) {} |