| changeset 37738 | 7bf3ec9e7b0c |
| parent 33686 | 8e33ca8832b1 |
| child 50473 | ca4088bf8365 |
--- 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;}