lib/browser/GraphBrowser/GraphView.java
changeset 6541 d3ac35b2bfbf
parent 3599 89cbba12863d
child 11811 38721b2c6f57
equal deleted inserted replaced
6540:eaf90f6806df 6541:d3ac35b2bfbf
    10 ***************************************************************************/
    10 ***************************************************************************/
    11 
    11 
    12 package GraphBrowser;
    12 package GraphBrowser;
    13 
    13 
    14 import java.awt.*;
    14 import java.awt.*;
       
    15 import java.awt.event.*;
    15 import java.io.*;
    16 import java.io.*;
    16 import java.util.*;
    17 import java.util.*;
    17 import awtUtilities.*;
    18 import awtUtilities.*;
    18 
    19 
    19 public class GraphView extends ScrollCanvas {
    20 public class GraphView extends Canvas implements MouseListener, MouseMotionListener {
    20 	Graph gra,gra2;
    21 	Graph gra, gra2;
    21 	GraphBrowser parent;
    22 	GraphBrowser browser;
    22 	Vertex v=null;
    23 	Vertex v = null;
    23 	Vector collapsed=new Vector(10,10);
    24 	Vector collapsed = new Vector(10,10);
    24 	Vector collapsedDirs=new Vector(10,10);
    25 	Vector collapsedDirs = new Vector(10,10);
    25 	TreeBrowser tb;
    26 	TreeBrowser tb;
    26 	long timestamp;
    27 	long timestamp;
    27 	Vertex highlighted=null;
    28 	Vertex highlighted = null;
       
    29 	Dimension size;
       
    30 	boolean parent_needs_layout;
    28 
    31 
    29 	public void setTreeBrowser(TreeBrowser br) {
    32 	public void setTreeBrowser(TreeBrowser br) {
    30 		tb=br;
    33 		tb=br;
    31 	}
    34 	}
    32 
    35 
    33 	public GraphBrowser getBrowser() { return parent; }
    36 	public GraphBrowser getBrowser() { return browser; }
    34 
    37 
    35 	public Graph getGraph() { return gra; }
    38 	public Graph getGraph() { return gra; }
    36 
    39 
    37 	public Graph getOriginalGraph() { return gra2; }
    40 	public Graph getOriginalGraph() { return gra2; }
    38 
    41 
    39 	public GraphView(Graph gr,GraphBrowser br) {
    42 	public GraphView(Graph gr,GraphBrowser br) {
    40 		gra2=gr;
    43 		gra2=gr;
    41 		parent=br;
    44 		browser=br;
    42 		gra=(Graph)(gra2.clone());
    45 		gra=(Graph)(gra2.clone());
       
    46 		parent_needs_layout = true;
       
    47 		size = new Dimension(0, 0);
       
    48 		addMouseListener(this);
       
    49 		addMouseMotionListener(this);
    43 	}
    50 	}
    44 
    51 
    45 	public void PS(String fname,boolean printable) throws IOException {
    52 	public void PS(String fname,boolean printable) throws IOException {
    46 		gra.PS(fname,printable);
    53 		gra.PS(fname,printable);
    47 	}
    54 	}
    48 
    55 
    49 	public void paintCanvas(Graphics g)
    56 	public void paint(Graphics g) {
    50 	{
       
    51 		set_size(gra.max_x-gra.min_x,gra.max_y-gra.min_y);
       
    52 		gra.draw(g);
    57 		gra.draw(g);
    53 	}
    58 		if (highlighted!=null) highlighted.drawBox(g,Color.white);
    54 
    59 		size = new Dimension(gra.max_x-gra.min_x, gra.max_y-gra.min_y);
    55 	public boolean mouseMove(Event evt,int x,int y) {
    60 		if (parent_needs_layout) {
    56 		x+=gra.min_x;
    61 			parent_needs_layout = false;
    57 		y+=gra.min_y;
    62 			getParent().doLayout();
       
    63 		}
       
    64 	}
       
    65 
       
    66 	public Dimension getPreferredSize() {
       
    67 		return size;
       
    68 	}
       
    69 
       
    70 	public void mouseMoved(MouseEvent evt) {
       
    71 		int x = evt.getX() + gra.min_x;
       
    72 		int y = evt.getY() + gra.min_y;
    58 
    73 
    59 		Vertex v2=gra.vertexAt(x,y);
    74 		Vertex v2=gra.vertexAt(x,y);
    60 		Graphics g=getGraphics();
    75 		Graphics g=getGraphics();
    61 		g.translate(-gra.min_x,-gra.min_y);
    76 		g.translate(-gra.min_x,-gra.min_y);
    62 		if (highlighted!=null) {
    77 		if (highlighted!=null) {
    66 		if (v2!=v) {
    81 		if (v2!=v) {
    67 			if (v!=null) v.removeButtons(g);
    82 			if (v!=null) v.removeButtons(g);
    68 			if (v2!=null) v2.drawButtons(g);
    83 			if (v2!=null) v2.drawButtons(g);
    69 			v=v2;
    84 			v=v2;
    70 		}
    85 		}
    71 		return true;
    86 	}
    72 	}
    87 
       
    88 	public void mouseDragged(MouseEvent evt) {}
    73 
    89 
    74 	/*****************************************************************/
    90 	/*****************************************************************/
    75 	/* This method is called if successor / predecessor nodes (whose */
    91 	/* This method is called if successor / predecessor nodes (whose */
    76 	/* numbers are stored in Vector c) of a certain node should be   */
    92 	/* numbers are stored in Vector c) of a certain node should be   */
    77         /* displayed again                                               */
    93         /* displayed again                                               */
   120 		collapseNodes();
   136 		collapseNodes();
   121 		relayout();
   137 		relayout();
   122 	}
   138 	}
   123 
   139 
   124 	public void relayout() {
   140 	public void relayout() {
   125 		parent.showWaitMessage();
   141 		browser.showWaitMessage();
   126 		highlighted=null;
   142 		highlighted=null;
   127 		gra.layout(getGraphics());
   143 		gra.layout(getGraphics());
   128 		v=null;
   144 		v=null;
       
   145 		parent_needs_layout = true;
   129 		update(getGraphics());
   146 		update(getGraphics());
   130 		parent.showReadyMessage();
   147 		browser.showReadyMessage();
   131 	}
   148 	}
   132 
   149 
   133 	public void focusToVertex(int n) {
   150 	public void focusToVertex(int n) {
   134 		Vertex vx=gra.getVertexByNum(n);
   151 		Vertex vx=gra.getVertexByNum(n);
   135 		if (vx!=null) {
   152 		if (vx!=null) {
   136 			focus_to(vx.getX()-gra.min_x,vx.getY()-gra.min_y);
   153 			ScrollPane scrollp = (ScrollPane)(getParent());
   137 			highlighted=vx;
   154 			Dimension vpsize = scrollp.getViewportSize();
       
   155 
       
   156                         int x = vx.getX()-gra.min_x;
       
   157                         int y = vx.getY()-gra.min_y;
       
   158 			int offset_x = Math.min(scrollp.getHAdjustable().getMaximum(),
       
   159 				Math.max(0,x-vpsize.width/2));
       
   160 			int offset_y = Math.min(scrollp.getVAdjustable().getMaximum(),
       
   161 				Math.max(0,y-vpsize.height/2));
       
   162 
   138 			Graphics g=getGraphics();
   163 			Graphics g=getGraphics();
   139 			g.translate(-gra.min_x,-gra.min_y);
   164 			g.translate(-gra.min_x,-gra.min_y);
       
   165 			if (highlighted!=null) highlighted.drawBox(g,Color.lightGray);
   140 			vx.drawBox(g,Color.white);
   166 			vx.drawBox(g,Color.white);
       
   167 			highlighted=vx;
       
   168 			scrollp.setScrollPosition(offset_x, offset_y);
   141 		}
   169 		}
   142 	}
   170 	}
   143 
   171 
   144 	/*****************************************************************/
   172 	/*****************************************************************/
   145 	/*             Create new graph with collapsed nodes             */
   173 	/*             Create new graph with collapsed nodes             */
   163 			if (!v.isEmpty())
   191 			if (!v.isEmpty())
   164 				gra.collapse(v,"["+d.getName()+"]",d.getCollapsed());
   192 				gra.collapse(v,"["+d.getName()+"]",d.getCollapsed());
   165 		}
   193 		}
   166 	}
   194 	}
   167 
   195 
   168 	public boolean mouseDown(Event evt,int x,int y) {
   196 	public void mouseClicked(MouseEvent evt) {
   169 		Vector code=null;
   197 		Vector code = null;
   170 		Vertex v2;
   198 		Vertex v2;
   171 		x+=gra.min_x;
   199 		int x = evt.getX() + gra.min_x;
   172 		y+=gra.min_y;
   200 		int y = evt.getY() + gra.min_y;
   173 
   201 
   174 		if (v!=null) {
   202 		if (v!=null) {
   175 			int num=v.getNumber();
   203 			int num=v.getNumber();
   176 			v2=gra2.getVertexByNum(num);
   204 			v2=gra2.getVertexByNum(num);
   177 			if (v.leftButton(x,y)) {
   205 			if (v.leftButton(x,y)) {
   212 				}
   240 				}
   213 			} else if (v.getInflate()!=null) {
   241 			} else if (v.getInflate()!=null) {
   214 				inflateNode(v.getInflate());
   242 				inflateNode(v.getInflate());
   215 				v=null;
   243 				v=null;
   216 			} else {
   244 			} else {
   217 				if (evt.when-timestamp < 400 && !(v.getPath().equals("")))
   245 				if (evt.getWhen()-timestamp < 400 && !(v.getPath().equals("")))
   218 					parent.viewFile(v.getPath());
   246 					browser.viewFile(v.getPath());
   219 				timestamp=evt.when;
   247 				timestamp=evt.getWhen();
   220 			}
   248 			}
   221 		}
   249 		}
   222 		return true;
   250 	}
   223 	}
   251 
   224 
   252 	public void mouseExited(MouseEvent evt) {
   225 	public boolean mouseExit(Event evt,int x,int y) {
       
   226 		Graphics g=getGraphics();
   253 		Graphics g=getGraphics();
   227 		g.translate(-gra.min_x,-gra.min_y);
   254 		g.translate(-gra.min_x,-gra.min_y);
   228 		if (highlighted!=null) {
   255 		if (highlighted!=null) {
   229 			highlighted.drawBox(g,Color.lightGray);
   256 			highlighted.drawBox(g,Color.lightGray);
   230 			highlighted=null;
   257 			highlighted=null;
   231 		}
   258 		}
   232 		if (v!=null) v.removeButtons(g);
   259 		if (v!=null) v.removeButtons(g);
   233 		v=null;
   260 		v=null;
   234 		return true;
   261 	}
   235 	}
   262 
       
   263 	public void mouseEntered(MouseEvent evt) {}
       
   264 
       
   265 	public void mousePressed(MouseEvent evt) {}
       
   266 
       
   267 	public void mouseReleased(MouseEvent evt) {}
   236 }
   268 }