1/***************************************************************************
2  Title:      GraphBrowser/TreeBrowser.java
3  Author:     Stefan Berghofer, TU Muenchen
4  Options:    :tabSize=4:
5
6  This class defines the browser window which is used to display directory
7  trees. It contains methods for handling events.
8***************************************************************************/
9
10package GraphBrowser;
11
12import java.awt.*;
13import java.awt.event.*;
14import java.util.*;
15
16
17public class TreeBrowser extends Canvas implements MouseListener
18{
19	TreeNode t;
20	TreeNode selected;
21	GraphView gv;
22	long timestamp;
23	Dimension size;
24	boolean parent_needs_layout;
25	Font font;
26
27	public TreeBrowser(TreeNode tn, GraphView gr, Font f) {
28		t = tn; gv = gr; font = f;
29		size = new Dimension(0, 0);
30		parent_needs_layout = true;
31		addMouseListener(this);
32	}
33
34	public Dimension getPreferredSize() {
35		return size;
36	}
37
38	public void mouseEntered(MouseEvent evt) {}
39
40	public void mouseExited(MouseEvent evt) {}
41
42	public void mouseReleased(MouseEvent evt) {}
43
44	public void mousePressed(MouseEvent evt) {}
45
46	public void mouseClicked(MouseEvent e)
47	{
48		TreeNode l=t.lookup(e.getY());
49
50		if (l!=null)
51		{
52			if (l.select()) {
53				Vector v=new Vector(10,10);
54				t.collapsedDirectories(v);
55				gv.collapseDir(v);
56				gv.relayout();
57			} else {
58				Vertex vx=gv.getGraph().getVertexByNum(l.getNumber());
59				gv.focusToVertex(l.getNumber());
60				vx=gv.getOriginalGraph().getVertexByNum(l.getNumber());
61				if (e.getWhen()-timestamp < 400 && !(vx.getPath().equals("")))
62					gv.getBrowser().viewFile(vx.getPath());
63				timestamp=e.getWhen();
64
65			}
66			selected=l;
67			parent_needs_layout = true;
68			repaint();
69		}
70	}
71
72	public void selectNode(TreeNode nd) {
73		Vector v=new Vector(10,10);
74		nd.select();
75		t.collapsedDirectories(v);
76		gv.collapseDir(v);
77		gv.relayout();
78		selected=nd;
79		parent_needs_layout = true;
80		repaint();
81	}
82
83	public void paint(Graphics g)
84	{
85		g.setFont(font);
86		Dimension d = t.draw(g,5,5,selected);
87		if (parent_needs_layout) {
88			size = new Dimension(5+d.width, 5+d.height);
89			parent_needs_layout = false;
90			getParent().doLayout();
91		}
92	}
93}
94
95