diff -r 243ea7885e05 -r 7bf3ec9e7b0c lib/browser/GraphBrowser/Vertex.java
--- 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;}