1.1 --- a/lib/browser/GraphBrowser/Graph.java	Wed Jul 07 09:26:54 2010 +0200
     1.2 +++ b/lib/browser/GraphBrowser/Graph.java	Wed Jul 07 18:17:23 2010 +0200
     1.3 @@ -17,9 +17,7 @@
     1.4  
     1.5  	public int box_height=0;
     1.6  	public int box_height2;
     1.7 -	public int box_width;
     1.8 -	public int box_width2;
     1.9 -	public int box_hspace;
    1.10 +	public Graphics gfx;
    1.11  
    1.12  	Vector vertices=new Vector(10,10);
    1.13  	Vector splines=new Vector(10,10);
    1.14 @@ -185,19 +183,16 @@
    1.15  
    1.16  	public void setParameters(Graphics g) {
    1.17  		Enumeration e1=vertices.elements();
    1.18 -		int h,w;
    1.19 -		h=w=Integer.MIN_VALUE;
    1.20 +		int h;
    1.21 +		h=Integer.MIN_VALUE;
    1.22  
    1.23  		while (e1.hasMoreElements()) {
    1.24  		  Box dim=((Vertex)(e1.nextElement())).getLabelSize(g);
    1.25  			h=Math.max(h,dim.height);
    1.26 -			w=Math.max(w,dim.width);
    1.27  		}
    1.28  		box_height=h+4;
    1.29  		box_height2=box_height/2;
    1.30 -		box_width=w+8;
    1.31 -		box_width2=box_width/2;
    1.32 -		box_hspace=box_width+20;
    1.33 +		gfx=g;
    1.34  	}
    1.35  
    1.36  	/********************************************************************/
    1.37 @@ -538,12 +533,12 @@
    1.38  		while (e1.hasMoreElements()) {
    1.39  			Vector v1=(Vector)(e1.nextElement());
    1.40  			Enumeration e2=v1.elements();
    1.41 -			int x=box_width2;
    1.42 +			int x=0;
    1.43  			while (e2.hasMoreElements()) {
    1.44  				Vertex ve=(Vertex)(e2.nextElement());
    1.45 -				ve.setX(x);
    1.46 +				ve.setX(x+ve.box_width2());
    1.47  				ve.setY(y);
    1.48 -				x+=box_hspace;
    1.49 +				x+=ve.box_width()+20;
    1.50  			}
    1.51  			y+=box_height+Math.max(35,7*(((Integer)(e3.nextElement())).intValue()));
    1.52  		}
    1.53 @@ -638,8 +633,8 @@
    1.54  					}
    1.55  					d2=(n!=0?d/n:0);
    1.56  
    1.57 -					if (d<0 && (i==0 || ((Vertex)(v.elementAt(i-1))).rightX()+box_hspace-box_width < vx.leftX()+d2) ||
    1.58 -						d>0 && (i==v.size()-1 || ((Vertex)(v.elementAt(i+1))).leftX()-box_hspace+box_width > vx.rightX()+d2))
    1.59 +					if (d<0 && (i==0 || ((Vertex)(v.elementAt(i-1))).rightX()+20 < vx.leftX()+d2) ||
    1.60 +						d>0 && (i==v.size()-1 || ((Vertex)(v.elementAt(i+1))).leftX()-20 > vx.rightX()+d2))
    1.61  						vx.setX(vx.getX()+d2);
    1.62  				}
    1.63  			}
    1.64 @@ -743,8 +738,6 @@
    1.65  							vx2=(Vertex)((vx2.getChildren()).nextElement());
    1.66  							x3=vx2.getX();
    1.67  							y3=vx2.getY();
    1.68 -							// spc=(box_hspace-box_width)/3;
    1.69 -							// spc=box_height*3/4;
    1.70  							spc=0;
    1.71  							leftx = k==0 /* || ((Vertex)(layer.elementAt(k-1))).isDummy() */ ?
    1.72  								Integer.MIN_VALUE:

     2.1 --- a/lib/browser/GraphBrowser/NormalVertex.java	Wed Jul 07 09:26:54 2010 +0200
     2.2 +++ b/lib/browser/GraphBrowser/NormalVertex.java	Wed Jul 07 18:17:23 2010 +0200
     2.3 @@ -58,28 +58,23 @@
     2.4  
     2.5  	public void setDir(String d) { dir=d; }
     2.6  
     2.7 -	public int leftX() { return getX()-gra.box_width2; }
     2.8 +	public int leftX() { return getX()-box_width2(); }
     2.9  
    2.10 -	public int rightX() { return getX()+gra.box_width2; }
    2.11 +	public int rightX() { return getX()+box_width2(); }
    2.12  
    2.13  	public void drawBox(Graphics g,Color boxColor) {
    2.14  		FontMetrics fm = g.getFontMetrics(g.getFont());
    2.15  		int h=fm.getAscent()+fm.getDescent();
    2.16  
    2.17  		g.setColor(boxColor);
    2.18 -		g.fillRect(getX()-gra.box_width2,getY(),gra.box_width,gra.box_height);
    2.19 +		g.fillRect(getX()-box_width2(),getY(),box_width(),gra.box_height);
    2.20  		g.setColor(Color.black);
    2.21 -		g.drawRect(getX()-gra.box_width2,getY(),gra.box_width,gra.box_height);
    2.22 -		if (getNumber()<0) {
    2.23 +		g.drawRect(getX()-box_width2(),getY(),box_width(),gra.box_height);
    2.24 +		if (getNumber()<0)
    2.25  			g.setColor(Color.red);
    2.26 -			label=label.substring(1,label.length()-1);
    2.27 -			while (label.length()>0 && fm.stringWidth("["+label+"]")>gra.box_width-8)
    2.28 -					label=label.substring(0,label.length()-1);
    2.29 -			label="["+label+"]";
    2.30 -		}
    2.31  
    2.32  		g.drawString(label,
    2.33 -		             (int)Math.round((gra.box_width-fm.stringWidth(label))/2.0)+getX()-gra.box_width2,
    2.34 +		             (int)Math.round((box_width()-fm.stringWidth(label))/2.0)+getX()-box_width2(),
    2.35  				fm.getAscent()+(int)Math.round((gra.box_height-h)/2.0)+getY());
    2.36  	}
    2.37  
    2.38 @@ -136,7 +131,7 @@
    2.39  	}
    2.40  
    2.41  	public void PS(PrintWriter p) {
    2.42 -		p.print(leftX()+" "+getY()+" "+gra.box_width+" "+
    2.43 +		p.print(leftX()+" "+getY()+" "+box_width()+" "+
    2.44  		        gra.box_height+" (");
    2.45  		for (int i=0;i<label.length();i++)
    2.46  		{

     3.1 --- a/lib/browser/GraphBrowser/Region.java	Wed Jul 07 09:26:54 2010 +0200
     3.2 +++ b/lib/browser/GraphBrowser/Region.java	Wed Jul 07 18:17:23 2010 +0200
     3.3 @@ -79,7 +79,7 @@
     3.4  	public int spaceBetween(Region r2) {
     3.5  		return ((Vertex)(r2.getVertices().nextElement())).leftX()-
     3.6  			((Vertex)(vertices.lastElement())).rightX()-
     3.7 -			gra.box_hspace+gra.box_width;
     3.8 +			20;
     3.9  	}
    3.10  
    3.11  	public boolean touching(Region r2) {

     4.1 --- a/lib/browser/GraphBrowser/Vertex.java	Wed Jul 07 09:26:54 2010 +0200
     4.2 +++ b/lib/browser/GraphBrowser/Vertex.java	Wed Jul 07 18:17:23 2010 +0200
     4.3 @@ -178,6 +178,10 @@
     4.4  	    return succs;
     4.5  	}
     4.6  
     4.7 +	public int box_width() { return getLabelSize(gra.gfx).width+8; }
     4.8 +
     4.9 +	public int box_width2() { return box_width()/2; }
    4.10 +
    4.11  	public void setX(int x) {this.x=x;}
    4.12  
    4.13  	public void setY(int y) {this.y=y;}