lib/browser/GraphBrowser/NormalVertex.java
changeset 37737 7bf3ec9e7b0c
parent 33686 8e33ca8832b1
child 51488 ca4088bf8365
equal deleted inserted replaced
37736:243ea7885e05 37737:7bf3ec9e7b0c
    56 
    56 
    57 	public String getDir() { return dir; }
    57 	public String getDir() { return dir; }
    58 
    58 
    59 	public void setDir(String d) { dir=d; }
    59 	public void setDir(String d) { dir=d; }
    60 
    60 
    61 	public int leftX() { return getX()-gra.box_width2; }
    61 	public int leftX() { return getX()-box_width2(); }
    62 
    62 
    63 	public int rightX() { return getX()+gra.box_width2; }
    63 	public int rightX() { return getX()+box_width2(); }
    64 
    64 
    65 	public void drawBox(Graphics g,Color boxColor) {
    65 	public void drawBox(Graphics g,Color boxColor) {
    66 		FontMetrics fm = g.getFontMetrics(g.getFont());
    66 		FontMetrics fm = g.getFontMetrics(g.getFont());
    67 		int h=fm.getAscent()+fm.getDescent();
    67 		int h=fm.getAscent()+fm.getDescent();
    68 
    68 
    69 		g.setColor(boxColor);
    69 		g.setColor(boxColor);
    70 		g.fillRect(getX()-gra.box_width2,getY(),gra.box_width,gra.box_height);
    70 		g.fillRect(getX()-box_width2(),getY(),box_width(),gra.box_height);
    71 		g.setColor(Color.black);
    71 		g.setColor(Color.black);
    72 		g.drawRect(getX()-gra.box_width2,getY(),gra.box_width,gra.box_height);
    72 		g.drawRect(getX()-box_width2(),getY(),box_width(),gra.box_height);
    73 		if (getNumber()<0) {
    73 		if (getNumber()<0)
    74 			g.setColor(Color.red);
    74 			g.setColor(Color.red);
    75 			label=label.substring(1,label.length()-1);
       
    76 			while (label.length()>0 && fm.stringWidth("["+label+"]")>gra.box_width-8)
       
    77 					label=label.substring(0,label.length()-1);
       
    78 			label="["+label+"]";
       
    79 		}
       
    80 
    75 
    81 		g.drawString(label,
    76 		g.drawString(label,
    82 		             (int)Math.round((gra.box_width-fm.stringWidth(label))/2.0)+getX()-gra.box_width2,
    77 		             (int)Math.round((box_width()-fm.stringWidth(label))/2.0)+getX()-box_width2(),
    83 				fm.getAscent()+(int)Math.round((gra.box_height-h)/2.0)+getY());
    78 				fm.getAscent()+(int)Math.round((gra.box_height-h)/2.0)+getY());
    84 	}
    79 	}
    85 
    80 
    86 	public void removeButtons(Graphics g) {
    81 	public void removeButtons(Graphics g) {
    87 		drawBox(g,Color.lightGray);
    82 		drawBox(g,Color.lightGray);
   134 		}
   129 		}
   135 		g.setColor(Color.black);
   130 		g.setColor(Color.black);
   136 	}
   131 	}
   137 
   132 
   138 	public void PS(PrintWriter p) {
   133 	public void PS(PrintWriter p) {
   139 		p.print(leftX()+" "+getY()+" "+gra.box_width+" "+
   134 		p.print(leftX()+" "+getY()+" "+box_width()+" "+
   140 		        gra.box_height+" (");
   135 		        gra.box_height+" (");
   141 		for (int i=0;i<label.length();i++)
   136 		for (int i=0;i<label.length();i++)
   142 		{
   137 		{
   143 			if (("()\\").indexOf(label.charAt(i))>=0)
   138 			if (("()\\").indexOf(label.charAt(i))>=0)
   144 				p.print("\\");
   139 				p.print("\\");