lib/browser/GraphBrowser/Vertex.java
changeset 11798 fbab70de9b0d
parent 6541 d3ac35b2bfbf
child 11872 4f24fd4dbcf5
equal deleted inserted replaced
11797:1e29b79db3dc 11798:fbab70de9b0d
    67 	public String getID() {return "";}
    67 	public String getID() {return "";}
    68 
    68 
    69 	public void setID(String s) {}
    69 	public void setID(String s) {}
    70 
    70 
    71 	public Dimension getLabelSize(Graphics g) {
    71 	public Dimension getLabelSize(Graphics g) {
    72 		FontMetrics fm=g.getFontMetrics(font);
    72 		FontMetrics fm = g == null ? 
       
    73 		    new DefaultFontMetrics(font) : g.getFontMetrics(font);
    73 		
    74 		
    74 		return new Dimension(
    75 		return new Dimension(
    75 		        Math.max(fm.stringWidth("[. . . .]"),fm.stringWidth(getLabel())),
    76 		        Math.max(fm.stringWidth("[. . . .]"),fm.stringWidth(getLabel())),
    76 			fm.getAscent()+fm.getDescent());
    77 			fm.getAscent()+fm.getDescent());
    77 	}
    78 	}