lib/browser/GraphBrowser/TreeBrowser.java
author wenzelm
Fri, 16 Nov 2001 22:11:19 +0100
changeset 12229 bfba0eb5124b
parent 11873 38dc46b55d7e
child 14981 e73f8140af78
permissions -rw-r--r--
Ntree and Brouwer converted and moved to ZF/Induct;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
3599
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
     1
/***************************************************************************
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
     2
  Title:      GraphBrowser/TreeBrowser.java
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
     3
  ID:         $Id$
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
     4
  Author:     Stefan Berghofer, TU Muenchen
11873
38dc46b55d7e Moved font settings from TreeNode to TreeBrowser.
berghofe
parents: 6541
diff changeset
     5
  License:    GPL (GNU GENERAL PUBLIC LICENSE)
3599
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
     6
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
     7
  This class defines the browser window which is used to display directory
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
     8
  trees. It contains methods for handling events.
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
     9
***************************************************************************/
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    10
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    11
package GraphBrowser;
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    12
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    13
import java.awt.*;
6541
d3ac35b2bfbf Updated to JDK 1.1.x
berghofe
parents: 3599
diff changeset
    14
import java.awt.event.*;
3599
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    15
import java.util.*;
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    16
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    17
6541
d3ac35b2bfbf Updated to JDK 1.1.x
berghofe
parents: 3599
diff changeset
    18
public class TreeBrowser extends Canvas implements MouseListener
3599
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    19
{
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    20
	TreeNode t;
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    21
	TreeNode selected;
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    22
	GraphView gv;
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    23
	long timestamp;
6541
d3ac35b2bfbf Updated to JDK 1.1.x
berghofe
parents: 3599
diff changeset
    24
	Dimension size;
d3ac35b2bfbf Updated to JDK 1.1.x
berghofe
parents: 3599
diff changeset
    25
	boolean parent_needs_layout;
11873
38dc46b55d7e Moved font settings from TreeNode to TreeBrowser.
berghofe
parents: 6541
diff changeset
    26
	Font font;
3599
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    27
11873
38dc46b55d7e Moved font settings from TreeNode to TreeBrowser.
berghofe
parents: 6541
diff changeset
    28
	public TreeBrowser(TreeNode tn, GraphView gr, Font f) {
38dc46b55d7e Moved font settings from TreeNode to TreeBrowser.
berghofe
parents: 6541
diff changeset
    29
		t = tn; gv = gr; font = f;
6541
d3ac35b2bfbf Updated to JDK 1.1.x
berghofe
parents: 3599
diff changeset
    30
		size = new Dimension(0, 0);
d3ac35b2bfbf Updated to JDK 1.1.x
berghofe
parents: 3599
diff changeset
    31
		parent_needs_layout = true;
d3ac35b2bfbf Updated to JDK 1.1.x
berghofe
parents: 3599
diff changeset
    32
		addMouseListener(this);
3599
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    33
	}
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    34
6541
d3ac35b2bfbf Updated to JDK 1.1.x
berghofe
parents: 3599
diff changeset
    35
	public Dimension getPreferredSize() {
d3ac35b2bfbf Updated to JDK 1.1.x
berghofe
parents: 3599
diff changeset
    36
		return size;
d3ac35b2bfbf Updated to JDK 1.1.x
berghofe
parents: 3599
diff changeset
    37
	}
d3ac35b2bfbf Updated to JDK 1.1.x
berghofe
parents: 3599
diff changeset
    38
d3ac35b2bfbf Updated to JDK 1.1.x
berghofe
parents: 3599
diff changeset
    39
	public void mouseEntered(MouseEvent evt) {}
d3ac35b2bfbf Updated to JDK 1.1.x
berghofe
parents: 3599
diff changeset
    40
d3ac35b2bfbf Updated to JDK 1.1.x
berghofe
parents: 3599
diff changeset
    41
	public void mouseExited(MouseEvent evt) {}
d3ac35b2bfbf Updated to JDK 1.1.x
berghofe
parents: 3599
diff changeset
    42
d3ac35b2bfbf Updated to JDK 1.1.x
berghofe
parents: 3599
diff changeset
    43
	public void mouseReleased(MouseEvent evt) {}
d3ac35b2bfbf Updated to JDK 1.1.x
berghofe
parents: 3599
diff changeset
    44
d3ac35b2bfbf Updated to JDK 1.1.x
berghofe
parents: 3599
diff changeset
    45
	public void mousePressed(MouseEvent evt) {}
d3ac35b2bfbf Updated to JDK 1.1.x
berghofe
parents: 3599
diff changeset
    46
d3ac35b2bfbf Updated to JDK 1.1.x
berghofe
parents: 3599
diff changeset
    47
	public void mouseClicked(MouseEvent e)
3599
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    48
	{
6541
d3ac35b2bfbf Updated to JDK 1.1.x
berghofe
parents: 3599
diff changeset
    49
		TreeNode l=t.lookup(e.getY());
3599
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    50
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    51
		if (l!=null)
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    52
		{
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    53
			if (l.select()) {
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    54
				Vector v=new Vector(10,10);
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    55
				t.collapsedDirectories(v);
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    56
				gv.collapseDir(v);
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    57
				gv.relayout();
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    58
			} else {
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    59
				Vertex vx=gv.getGraph().getVertexByNum(l.getNumber());
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    60
				gv.focusToVertex(l.getNumber());
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    61
				vx=gv.getOriginalGraph().getVertexByNum(l.getNumber());
6541
d3ac35b2bfbf Updated to JDK 1.1.x
berghofe
parents: 3599
diff changeset
    62
				if (e.getWhen()-timestamp < 400 && !(vx.getPath().equals("")))
3599
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    63
					gv.getBrowser().viewFile(vx.getPath());
6541
d3ac35b2bfbf Updated to JDK 1.1.x
berghofe
parents: 3599
diff changeset
    64
				timestamp=e.getWhen();
3599
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    65
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    66
			}
6541
d3ac35b2bfbf Updated to JDK 1.1.x
berghofe
parents: 3599
diff changeset
    67
			selected=l;
d3ac35b2bfbf Updated to JDK 1.1.x
berghofe
parents: 3599
diff changeset
    68
			parent_needs_layout = true;
d3ac35b2bfbf Updated to JDK 1.1.x
berghofe
parents: 3599
diff changeset
    69
			repaint();
3599
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    70
		}
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    71
	}
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    72
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    73
	public void selectNode(TreeNode nd) {
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    74
		Vector v=new Vector(10,10);
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    75
		nd.select();
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    76
		t.collapsedDirectories(v);
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    77
		gv.collapseDir(v);
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    78
		gv.relayout();
6541
d3ac35b2bfbf Updated to JDK 1.1.x
berghofe
parents: 3599
diff changeset
    79
		selected=nd;
d3ac35b2bfbf Updated to JDK 1.1.x
berghofe
parents: 3599
diff changeset
    80
		parent_needs_layout = true;
d3ac35b2bfbf Updated to JDK 1.1.x
berghofe
parents: 3599
diff changeset
    81
		repaint();
3599
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    82
	}
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    83
6541
d3ac35b2bfbf Updated to JDK 1.1.x
berghofe
parents: 3599
diff changeset
    84
	public void paint(Graphics g)
3599
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    85
	{
11873
38dc46b55d7e Moved font settings from TreeNode to TreeBrowser.
berghofe
parents: 6541
diff changeset
    86
		g.setFont(font);
6541
d3ac35b2bfbf Updated to JDK 1.1.x
berghofe
parents: 3599
diff changeset
    87
		Dimension d = t.draw(g,5,5,selected);
d3ac35b2bfbf Updated to JDK 1.1.x
berghofe
parents: 3599
diff changeset
    88
		if (parent_needs_layout) {
d3ac35b2bfbf Updated to JDK 1.1.x
berghofe
parents: 3599
diff changeset
    89
			size = new Dimension(5+d.width, 5+d.height);
d3ac35b2bfbf Updated to JDK 1.1.x
berghofe
parents: 3599
diff changeset
    90
			parent_needs_layout = false;
d3ac35b2bfbf Updated to JDK 1.1.x
berghofe
parents: 3599
diff changeset
    91
			getParent().doLayout();
d3ac35b2bfbf Updated to JDK 1.1.x
berghofe
parents: 3599
diff changeset
    92
		}
3599
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    93
	}
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    94
}
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    95