lib/browser/GraphBrowser/GraphView.java
author wenzelm
Sun, 28 Nov 2010 14:01:20 +0100
changeset 40781 ba5be5c3d477
parent 33686 8e33ca8832b1
child 50473 ca4088bf8365
permissions -rw-r--r--
updated versions;
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/GraphView.java
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
     3
  Author:     Stefan Berghofer, TU Muenchen
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
     4
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
     5
  This class defines the window in which the graph is displayed. It
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
     6
  contains methods for handling events such as collapsing / uncollapsing
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
     7
  nodes of the graph.
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
     8
***************************************************************************/
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
package GraphBrowser;
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    11
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    12
import java.awt.*;
6541
d3ac35b2bfbf Updated to JDK 1.1.x
berghofe
parents: 3599
diff changeset
    13
import java.awt.event.*;
3599
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    14
import java.io.*;
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
6541
d3ac35b2bfbf Updated to JDK 1.1.x
berghofe
parents: 3599
diff changeset
    17
public class GraphView extends Canvas implements MouseListener, MouseMotionListener {
d3ac35b2bfbf Updated to JDK 1.1.x
berghofe
parents: 3599
diff changeset
    18
	Graph gra, gra2;
d3ac35b2bfbf Updated to JDK 1.1.x
berghofe
parents: 3599
diff changeset
    19
	GraphBrowser browser;
d3ac35b2bfbf Updated to JDK 1.1.x
berghofe
parents: 3599
diff changeset
    20
	Vertex v = null;
d3ac35b2bfbf Updated to JDK 1.1.x
berghofe
parents: 3599
diff changeset
    21
	Vector collapsed = new Vector(10,10);
d3ac35b2bfbf Updated to JDK 1.1.x
berghofe
parents: 3599
diff changeset
    22
	Vector collapsedDirs = new Vector(10,10);
3599
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    23
	TreeBrowser tb;
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    24
	long timestamp;
6541
d3ac35b2bfbf Updated to JDK 1.1.x
berghofe
parents: 3599
diff changeset
    25
	Vertex highlighted = null;
d3ac35b2bfbf Updated to JDK 1.1.x
berghofe
parents: 3599
diff changeset
    26
	Dimension size;
d3ac35b2bfbf Updated to JDK 1.1.x
berghofe
parents: 3599
diff changeset
    27
	boolean parent_needs_layout;
11872
4f24fd4dbcf5 Moved font settings from Vertex to GraphView.
berghofe
parents: 11811
diff changeset
    28
	Font font;
3599
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    29
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    30
	public void setTreeBrowser(TreeBrowser br) {
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    31
		tb=br;
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    32
	}
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    33
6541
d3ac35b2bfbf Updated to JDK 1.1.x
berghofe
parents: 3599
diff changeset
    34
	public GraphBrowser getBrowser() { return browser; }
3599
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    35
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    36
	public Graph getGraph() { return gra; }
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    37
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    38
	public Graph getOriginalGraph() { return gra2; }
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    39
11872
4f24fd4dbcf5 Moved font settings from Vertex to GraphView.
berghofe
parents: 11811
diff changeset
    40
	public GraphView(Graph gr, GraphBrowser br, Font f) {
3599
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    41
		gra2=gr;
6541
d3ac35b2bfbf Updated to JDK 1.1.x
berghofe
parents: 3599
diff changeset
    42
		browser=br;
3599
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    43
		gra=(Graph)(gra2.clone());
6541
d3ac35b2bfbf Updated to JDK 1.1.x
berghofe
parents: 3599
diff changeset
    44
		parent_needs_layout = true;
d3ac35b2bfbf Updated to JDK 1.1.x
berghofe
parents: 3599
diff changeset
    45
		size = new Dimension(0, 0);
11872
4f24fd4dbcf5 Moved font settings from Vertex to GraphView.
berghofe
parents: 11811
diff changeset
    46
		font = f;
6541
d3ac35b2bfbf Updated to JDK 1.1.x
berghofe
parents: 3599
diff changeset
    47
		addMouseListener(this);
d3ac35b2bfbf Updated to JDK 1.1.x
berghofe
parents: 3599
diff changeset
    48
		addMouseMotionListener(this);
3599
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    49
	}
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
	public void PS(String fname,boolean printable) throws IOException {
11811
38721b2c6f57 PS method now calculates layout using default font metrics.
berghofe
parents: 6541
diff changeset
    52
	    Graph gra3 = (Graph)gra.clone();
38721b2c6f57 PS method now calculates layout using default font metrics.
berghofe
parents: 6541
diff changeset
    53
	    gra3.layout(null);
38721b2c6f57 PS method now calculates layout using default font metrics.
berghofe
parents: 6541
diff changeset
    54
	    gra3.PS(fname,printable);
3599
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    55
	}
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    56
6541
d3ac35b2bfbf Updated to JDK 1.1.x
berghofe
parents: 3599
diff changeset
    57
	public void paint(Graphics g) {
11872
4f24fd4dbcf5 Moved font settings from Vertex to GraphView.
berghofe
parents: 11811
diff changeset
    58
		g.setFont(font);
3599
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    59
		gra.draw(g);
6541
d3ac35b2bfbf Updated to JDK 1.1.x
berghofe
parents: 3599
diff changeset
    60
		if (highlighted!=null) highlighted.drawBox(g,Color.white);
d3ac35b2bfbf Updated to JDK 1.1.x
berghofe
parents: 3599
diff changeset
    61
		size = new Dimension(gra.max_x-gra.min_x, gra.max_y-gra.min_y);
d3ac35b2bfbf Updated to JDK 1.1.x
berghofe
parents: 3599
diff changeset
    62
		if (parent_needs_layout) {
d3ac35b2bfbf Updated to JDK 1.1.x
berghofe
parents: 3599
diff changeset
    63
			parent_needs_layout = false;
d3ac35b2bfbf Updated to JDK 1.1.x
berghofe
parents: 3599
diff changeset
    64
			getParent().doLayout();
d3ac35b2bfbf Updated to JDK 1.1.x
berghofe
parents: 3599
diff changeset
    65
		}
3599
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    66
	}
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    67
6541
d3ac35b2bfbf Updated to JDK 1.1.x
berghofe
parents: 3599
diff changeset
    68
	public Dimension getPreferredSize() {
d3ac35b2bfbf Updated to JDK 1.1.x
berghofe
parents: 3599
diff changeset
    69
		return size;
d3ac35b2bfbf Updated to JDK 1.1.x
berghofe
parents: 3599
diff changeset
    70
	}
d3ac35b2bfbf Updated to JDK 1.1.x
berghofe
parents: 3599
diff changeset
    71
d3ac35b2bfbf Updated to JDK 1.1.x
berghofe
parents: 3599
diff changeset
    72
	public void mouseMoved(MouseEvent evt) {
d3ac35b2bfbf Updated to JDK 1.1.x
berghofe
parents: 3599
diff changeset
    73
		int x = evt.getX() + gra.min_x;
d3ac35b2bfbf Updated to JDK 1.1.x
berghofe
parents: 3599
diff changeset
    74
		int y = evt.getY() + gra.min_y;
3599
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    75
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    76
		Vertex v2=gra.vertexAt(x,y);
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    77
		Graphics g=getGraphics();
11872
4f24fd4dbcf5 Moved font settings from Vertex to GraphView.
berghofe
parents: 11811
diff changeset
    78
		g.setFont(font);
3599
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    79
		g.translate(-gra.min_x,-gra.min_y);
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    80
		if (highlighted!=null) {
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    81
			highlighted.drawBox(g,Color.lightGray);
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    82
			highlighted=null;
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    83
		}
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    84
		if (v2!=v) {
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    85
			if (v!=null) v.removeButtons(g);
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    86
			if (v2!=null) v2.drawButtons(g);
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    87
			v=v2;
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    88
		}
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    89
	}
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    90
6541
d3ac35b2bfbf Updated to JDK 1.1.x
berghofe
parents: 3599
diff changeset
    91
	public void mouseDragged(MouseEvent evt) {}
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
	/* This method is called if successor / predecessor nodes (whose */
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    95
	/* numbers are stored in Vector c) of a certain node should be   */
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    96
        /* displayed again                                               */
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    97
	/*****************************************************************/
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    98
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    99
	void uncollapse(Vector c) {
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   100
		collapsed.removeElement(c);
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   101
		collapseNodes();
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   102
	}
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   103
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   104
	/*****************************************************************/
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   105
	/* This method is called by class TreeBrowser when directories   */
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   106
	/* are collapsed / uncollapsed by the user                       */
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   107
	/*****************************************************************/
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   108
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   109
	public void collapseDir(Vector v) {
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   110
		collapsedDirs=v;
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   111
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   112
		collapseNodes();
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   113
	}
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   114
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   115
	/*****************************************************************/
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   116
	/*                      Inflate node again                       */
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   117
	/*****************************************************************/
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   118
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   119
	public void inflateNode(Vector c) {
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   120
		Enumeration e1;
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   121
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   122
		e1=collapsedDirs.elements();
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   123
		while (e1.hasMoreElements()) {
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   124
			Directory d=(Directory)(e1.nextElement());
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   125
			if (d.collapsed==c) {
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   126
				tb.selectNode(d.getNode());
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   127
				return;
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   128
			}
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   129
		}
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   130
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   131
		collapsed.removeElement(c);
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   132
		e1=gra2.getVertices();
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   133
		while (e1.hasMoreElements()) {
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   134
			Vertex vx=(Vertex)(e1.nextElement());
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   135
			if (vx.getUp()==c) vx.setUp(null);
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   136
			if (vx.getDown()==c) vx.setDown(null);
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   137
		}
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   138
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   139
		collapseNodes();
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   140
		relayout();
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   141
	}
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   142
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   143
	public void relayout() {
11872
4f24fd4dbcf5 Moved font settings from Vertex to GraphView.
berghofe
parents: 11811
diff changeset
   144
		Graphics g = getGraphics();
4f24fd4dbcf5 Moved font settings from Vertex to GraphView.
berghofe
parents: 11811
diff changeset
   145
		g.setFont(font);
6541
d3ac35b2bfbf Updated to JDK 1.1.x
berghofe
parents: 3599
diff changeset
   146
		browser.showWaitMessage();
3599
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   147
		highlighted=null;
11872
4f24fd4dbcf5 Moved font settings from Vertex to GraphView.
berghofe
parents: 11811
diff changeset
   148
		gra.layout(g);
3599
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   149
		v=null;
6541
d3ac35b2bfbf Updated to JDK 1.1.x
berghofe
parents: 3599
diff changeset
   150
		parent_needs_layout = true;
11872
4f24fd4dbcf5 Moved font settings from Vertex to GraphView.
berghofe
parents: 11811
diff changeset
   151
		update(g);
6541
d3ac35b2bfbf Updated to JDK 1.1.x
berghofe
parents: 3599
diff changeset
   152
		browser.showReadyMessage();
3599
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   153
	}
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   154
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   155
	public void focusToVertex(int n) {
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   156
		Vertex vx=gra.getVertexByNum(n);
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   157
		if (vx!=null) {
6541
d3ac35b2bfbf Updated to JDK 1.1.x
berghofe
parents: 3599
diff changeset
   158
			ScrollPane scrollp = (ScrollPane)(getParent());
d3ac35b2bfbf Updated to JDK 1.1.x
berghofe
parents: 3599
diff changeset
   159
			Dimension vpsize = scrollp.getViewportSize();
d3ac35b2bfbf Updated to JDK 1.1.x
berghofe
parents: 3599
diff changeset
   160
d3ac35b2bfbf Updated to JDK 1.1.x
berghofe
parents: 3599
diff changeset
   161
                        int x = vx.getX()-gra.min_x;
d3ac35b2bfbf Updated to JDK 1.1.x
berghofe
parents: 3599
diff changeset
   162
                        int y = vx.getY()-gra.min_y;
d3ac35b2bfbf Updated to JDK 1.1.x
berghofe
parents: 3599
diff changeset
   163
			int offset_x = Math.min(scrollp.getHAdjustable().getMaximum(),
d3ac35b2bfbf Updated to JDK 1.1.x
berghofe
parents: 3599
diff changeset
   164
				Math.max(0,x-vpsize.width/2));
d3ac35b2bfbf Updated to JDK 1.1.x
berghofe
parents: 3599
diff changeset
   165
			int offset_y = Math.min(scrollp.getVAdjustable().getMaximum(),
d3ac35b2bfbf Updated to JDK 1.1.x
berghofe
parents: 3599
diff changeset
   166
				Math.max(0,y-vpsize.height/2));
d3ac35b2bfbf Updated to JDK 1.1.x
berghofe
parents: 3599
diff changeset
   167
3599
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   168
			Graphics g=getGraphics();
11872
4f24fd4dbcf5 Moved font settings from Vertex to GraphView.
berghofe
parents: 11811
diff changeset
   169
			g.setFont(font);
3599
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   170
			g.translate(-gra.min_x,-gra.min_y);
6541
d3ac35b2bfbf Updated to JDK 1.1.x
berghofe
parents: 3599
diff changeset
   171
			if (highlighted!=null) highlighted.drawBox(g,Color.lightGray);
3599
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   172
			vx.drawBox(g,Color.white);
6541
d3ac35b2bfbf Updated to JDK 1.1.x
berghofe
parents: 3599
diff changeset
   173
			highlighted=vx;
d3ac35b2bfbf Updated to JDK 1.1.x
berghofe
parents: 3599
diff changeset
   174
			scrollp.setScrollPosition(offset_x, offset_y);
3599
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   175
		}
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   176
	}
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   177
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   178
	/*****************************************************************/
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   179
	/*             Create new graph with collapsed nodes             */
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   180
	/*****************************************************************/
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   181
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   182
	public void collapseNodes() {
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   183
		Enumeration e1=collapsed.elements();
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   184
		gra=(Graph)(gra2.clone());
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   185
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   186
		while (e1.hasMoreElements()) {
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   187
			Vector v1=(Vector)(e1.nextElement());
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   188
			Vector v2=gra.decode(v1);
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   189
			if (!v2.isEmpty()) gra.collapse(v2,"[. . . .]",v1);
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   190
		}
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   191
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   192
		e1=collapsedDirs.elements();
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   193
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   194
		while (e1.hasMoreElements()) {
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   195
			Directory d=(Directory)(e1.nextElement());
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   196
			Vector v=gra.decode(d.getCollapsed());
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   197
			if (!v.isEmpty())
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   198
				gra.collapse(v,"["+d.getName()+"]",d.getCollapsed());
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   199
		}
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   200
	}
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   201
6541
d3ac35b2bfbf Updated to JDK 1.1.x
berghofe
parents: 3599
diff changeset
   202
	public void mouseClicked(MouseEvent evt) {
d3ac35b2bfbf Updated to JDK 1.1.x
berghofe
parents: 3599
diff changeset
   203
		Vector code = null;
3599
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   204
		Vertex v2;
6541
d3ac35b2bfbf Updated to JDK 1.1.x
berghofe
parents: 3599
diff changeset
   205
		int x = evt.getX() + gra.min_x;
d3ac35b2bfbf Updated to JDK 1.1.x
berghofe
parents: 3599
diff changeset
   206
		int y = evt.getY() + gra.min_y;
3599
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   207
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   208
		if (v!=null) {
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   209
			int num=v.getNumber();
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   210
			v2=gra2.getVertexByNum(num);
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   211
			if (v.leftButton(x,y)) {
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   212
				if (v.getUp()!=null) {
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   213
					code=v.getUp();
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   214
					v2.setUp(null);
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   215
					v=null;
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   216
					uncollapse(code);
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   217
					relayout();
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   218
					focusToVertex(num);
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   219
				} else {
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   220
					Vector vs=v2.getPreds();
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   221
					code=gra2.encode(vs);
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   222
					v.setUp(code);v2.setUp(code);
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   223
					v=null;
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   224
					collapsed.insertElementAt(code,0);
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   225
					collapseNodes();
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   226
					relayout();
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   227
					focusToVertex(num);
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   228
				}
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   229
			} else if (v.rightButton(x,y)) {
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   230
				if (v.getDown()!=null) {
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   231
					code=v.getDown();
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   232
					v2.setDown(null);
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   233
					v=null;
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   234
					uncollapse(code);
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   235
					relayout();
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   236
					focusToVertex(num);
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   237
				} else {
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   238
					Vector vs=v2.getSuccs();
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   239
					code=gra2.encode(vs);
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   240
					v.setDown(code);v2.setDown(code);
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   241
					v=null;
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   242
					collapsed.insertElementAt(code,0);
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   243
					collapseNodes();
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   244
					relayout();
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   245
					focusToVertex(num);
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   246
				}
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   247
			} else if (v.getInflate()!=null) {
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   248
				inflateNode(v.getInflate());
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   249
				v=null;
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   250
			} else {
6541
d3ac35b2bfbf Updated to JDK 1.1.x
berghofe
parents: 3599
diff changeset
   251
				if (evt.getWhen()-timestamp < 400 && !(v.getPath().equals("")))
d3ac35b2bfbf Updated to JDK 1.1.x
berghofe
parents: 3599
diff changeset
   252
					browser.viewFile(v.getPath());
d3ac35b2bfbf Updated to JDK 1.1.x
berghofe
parents: 3599
diff changeset
   253
				timestamp=evt.getWhen();
3599
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   254
			}
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   255
		}
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   256
	}
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   257
6541
d3ac35b2bfbf Updated to JDK 1.1.x
berghofe
parents: 3599
diff changeset
   258
	public void mouseExited(MouseEvent evt) {
3599
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   259
		Graphics g=getGraphics();
11872
4f24fd4dbcf5 Moved font settings from Vertex to GraphView.
berghofe
parents: 11811
diff changeset
   260
		g.setFont(font);
3599
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   261
		g.translate(-gra.min_x,-gra.min_y);
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   262
		if (highlighted!=null) {
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   263
			highlighted.drawBox(g,Color.lightGray);
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   264
			highlighted=null;
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   265
		}
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   266
		if (v!=null) v.removeButtons(g);
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   267
		v=null;
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   268
	}
6541
d3ac35b2bfbf Updated to JDK 1.1.x
berghofe
parents: 3599
diff changeset
   269
d3ac35b2bfbf Updated to JDK 1.1.x
berghofe
parents: 3599
diff changeset
   270
	public void mouseEntered(MouseEvent evt) {}
d3ac35b2bfbf Updated to JDK 1.1.x
berghofe
parents: 3599
diff changeset
   271
d3ac35b2bfbf Updated to JDK 1.1.x
berghofe
parents: 3599
diff changeset
   272
	public void mousePressed(MouseEvent evt) {}
d3ac35b2bfbf Updated to JDK 1.1.x
berghofe
parents: 3599
diff changeset
   273
d3ac35b2bfbf Updated to JDK 1.1.x
berghofe
parents: 3599
diff changeset
   274
	public void mouseReleased(MouseEvent evt) {}
3599
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   275
}