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