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