lib/browser/GraphBrowser/NormalVertex.java
changeset 11872 4f24fd4dbcf5
parent 6541 d3ac35b2bfbf
child 14981 e73f8140af78
equal deleted inserted replaced
11871:0493188cff42 11872:4f24fd4dbcf5
     1 /***************************************************************************
     1 /***************************************************************************
     2   Title:      GraphBrowser/NormalVertex.java
     2   Title:      GraphBrowser/NormalVertex.java
     3   ID:         $Id$
     3   ID:         $Id$
     4   Author:     Stefan Berghofer, TU Muenchen
     4   Author:     Stefan Berghofer, TU Muenchen
     5   Copyright   1997  TU Muenchen
     5   License:    GPL (GNU GENERAL PUBLIC LICENSE)
     6 
     6 
     7   This class represents an ordinary vertex. It contains methods for
     7   This class represents an ordinary vertex. It contains methods for
     8   drawing and PostScript output.
     8   drawing and PostScript output.
     9 ***************************************************************************/
     9 ***************************************************************************/
    10 
    10 
    63 	public int leftX() { return getX()-gra.box_width2; }
    63 	public int leftX() { return getX()-gra.box_width2; }
    64 
    64 
    65 	public int rightX() { return getX()+gra.box_width2; }
    65 	public int rightX() { return getX()+gra.box_width2; }
    66 
    66 
    67 	public void drawBox(Graphics g,Color boxColor) {
    67 	public void drawBox(Graphics g,Color boxColor) {
    68 		FontMetrics fm=g.getFontMetrics(font);
    68 		FontMetrics fm = g.getFontMetrics(g.getFont());
    69 		g.setFont(font);
       
    70 		int h=fm.getAscent()+fm.getDescent();
    69 		int h=fm.getAscent()+fm.getDescent();
    71 
    70 
    72 		g.setColor(boxColor);
    71 		g.setColor(boxColor);
    73 		g.fillRect(getX()-gra.box_width2,getY(),gra.box_width,gra.box_height);
    72 		g.fillRect(getX()-gra.box_width2,getY(),gra.box_width,gra.box_height);
    74 		g.setColor(Color.black);
    73 		g.setColor(Color.black);