Boxes may now have different widths.

--- a/lib/browser/GraphBrowser/Graph.java	Wed Jul 07 09:26:54 2010 +0200
+++ b/lib/browser/GraphBrowser/Graph.java	Wed Jul 07 18:17:23 2010 +0200
@@ -17,9 +17,7 @@
 
 	public int box_height=0;
 	public int box_height2;
-	public int box_width;
-	public int box_width2;
-	public int box_hspace;
+	public Graphics gfx;
 
 	Vector vertices=new Vector(10,10);
 	Vector splines=new Vector(10,10);
@@ -185,19 +183,16 @@
 
 	public void setParameters(Graphics g) {
 		Enumeration e1=vertices.elements();
-		int h,w;
-		h=w=Integer.MIN_VALUE;
+		int h;
+		h=Integer.MIN_VALUE;
 
 		while (e1.hasMoreElements()) {
 		  Box dim=((Vertex)(e1.nextElement())).getLabelSize(g);
 			h=Math.max(h,dim.height);
-			w=Math.max(w,dim.width);
 		}
 		box_height=h+4;
 		box_height2=box_height/2;
-		box_width=w+8;
-		box_width2=box_width/2;
-		box_hspace=box_width+20;
+		gfx=g;
 	}
 
 	/********************************************************************/
@@ -538,12 +533,12 @@
 		while (e1.hasMoreElements()) {
 			Vector v1=(Vector)(e1.nextElement());
 			Enumeration e2=v1.elements();
-			int x=box_width2;
+			int x=0;
 			while (e2.hasMoreElements()) {
 				Vertex ve=(Vertex)(e2.nextElement());
-				ve.setX(x);
+				ve.setX(x+ve.box_width2());
 				ve.setY(y);
-				x+=box_hspace;
+				x+=ve.box_width()+20;
 			}
 			y+=box_height+Math.max(35,7*(((Integer)(e3.nextElement())).intValue()));
 		}
@@ -638,8 +633,8 @@
 					}
 					d2=(n!=0?d/n:0);
 
-					if (d<0 && (i==0 || ((Vertex)(v.elementAt(i-1))).rightX()+box_hspace-box_width < vx.leftX()+d2) ||
-						d>0 && (i==v.size()-1 || ((Vertex)(v.elementAt(i+1))).leftX()-box_hspace+box_width > vx.rightX()+d2))
+					if (d<0 && (i==0 || ((Vertex)(v.elementAt(i-1))).rightX()+20 < vx.leftX()+d2) ||
+						d>0 && (i==v.size()-1 || ((Vertex)(v.elementAt(i+1))).leftX()-20 > vx.rightX()+d2))
 						vx.setX(vx.getX()+d2);
 				}
 			}
@@ -743,8 +738,6 @@
 							vx2=(Vertex)((vx2.getChildren()).nextElement());
 							x3=vx2.getX();
 							y3=vx2.getY();
-							// spc=(box_hspace-box_width)/3;
-							// spc=box_height*3/4;
 							spc=0;
 							leftx = k==0 /* || ((Vertex)(layer.elementAt(k-1))).isDummy() */ ?
 								Integer.MIN_VALUE:

--- a/lib/browser/GraphBrowser/NormalVertex.java	Wed Jul 07 09:26:54 2010 +0200
+++ b/lib/browser/GraphBrowser/NormalVertex.java	Wed Jul 07 18:17:23 2010 +0200
@@ -58,28 +58,23 @@
 
 	public void setDir(String d) { dir=d; }
 
-	public int leftX() { return getX()-gra.box_width2; }
+	public int leftX() { return getX()-box_width2(); }
 
-	public int rightX() { return getX()+gra.box_width2; }
+	public int rightX() { return getX()+box_width2(); }
 
 	public void drawBox(Graphics g,Color boxColor) {
 		FontMetrics fm = g.getFontMetrics(g.getFont());
 		int h=fm.getAscent()+fm.getDescent();
 
 		g.setColor(boxColor);
-		g.fillRect(getX()-gra.box_width2,getY(),gra.box_width,gra.box_height);
+		g.fillRect(getX()-box_width2(),getY(),box_width(),gra.box_height);
 		g.setColor(Color.black);
-		g.drawRect(getX()-gra.box_width2,getY(),gra.box_width,gra.box_height);
-		if (getNumber()<0) {
+		g.drawRect(getX()-box_width2(),getY(),box_width(),gra.box_height);
+		if (getNumber()<0)
 			g.setColor(Color.red);
-			label=label.substring(1,label.length()-1);
-			while (label.length()>0 && fm.stringWidth("["+label+"]")>gra.box_width-8)
-					label=label.substring(0,label.length()-1);
-			label="["+label+"]";
-		}
 
 		g.drawString(label,
-		             (int)Math.round((gra.box_width-fm.stringWidth(label))/2.0)+getX()-gra.box_width2,
+		             (int)Math.round((box_width()-fm.stringWidth(label))/2.0)+getX()-box_width2(),
 				fm.getAscent()+(int)Math.round((gra.box_height-h)/2.0)+getY());
 	}
 
@@ -136,7 +131,7 @@
 	}
 
 	public void PS(PrintWriter p) {
-		p.print(leftX()+" "+getY()+" "+gra.box_width+" "+
+		p.print(leftX()+" "+getY()+" "+box_width()+" "+
 		        gra.box_height+" (");
 		for (int i=0;i<label.length();i++)
 		{

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

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