renamed "Directories" to "Sessions";
authorwenzelm
Sun Jul 23 11:59:21 2000 +0200 (2000-07-23)
changeset 9407e8f6d918fde9
parent 9406 d505b11ce30d
child 9408 d3d56e1d2ec1
renamed "Directories" to "Sessions";
lib/browser/GraphBrowser/GraphBrowser.java
lib/browser/GraphBrowser/TreeNode.java
     1.1 --- a/lib/browser/GraphBrowser/GraphBrowser.java	Sun Jul 23 11:58:30 2000 +0200
     1.2 +++ b/lib/browser/GraphBrowser/GraphBrowser.java	Sun Jul 23 11:59:21 2000 +0200
     1.3 @@ -129,7 +129,7 @@
     1.4  
     1.5  	public void initBrowser(InputStream is) {
     1.6  		try {
     1.7 -			TreeNode tn=new TreeNode("Directories","",-1,true);
     1.8 +			TreeNode tn=new TreeNode("Sessions","",-1,true);
     1.9  			gv=new GraphView(new Graph(is,tn),this);
    1.10  			tb=new TreeBrowser(tn,gv);
    1.11  			gv.setTreeBrowser(tb);
     2.1 --- a/lib/browser/GraphBrowser/TreeNode.java	Sun Jul 23 11:58:30 2000 +0200
     2.2 +++ b/lib/browser/GraphBrowser/TreeNode.java	Sun Jul 23 11:59:21 2000 +0200
     2.3 @@ -143,10 +143,11 @@
     2.4  		FontMetrics fm=g.getFontMetrics(f);
     2.5  		g.setFont(f);
     2.6  		int h=fm.getHeight();
     2.7 -		int down_x[]={x, x + h, x + (int)(h / 2)};
     2.8 -		int down_y[]={y, y, y + (int)(3 * h / 4)};
     2.9 -		int right_x[]={2 + x, 2 + x + (int)(3 * h / 4), 2 + x};
    2.10 -		int right_y[]={y, y + (int)(h / 2), y + h};
    2.11 +		int e=(int) (h / 10) + 1;
    2.12 +		int down_x[]={x + e, x + h - e, x + (int)(h / 2)};
    2.13 +		int down_y[]={y + e, y + e, y + (int)(3 * h / 4) - e};
    2.14 +		int right_x[]={x + e, x + (int)(3 * h / 4) - e, x + e};
    2.15 +		int right_y[]={y + e, y + (int)(h / 2), y + h - e};
    2.16  		int dx=0;
    2.17  
    2.18  		if (unfold)