| 3599 |      1 | /***************************************************************************
 | 
|  |      2 |   Title:      GraphBrowser/NormalVertex.java
 | 
|  |      3 |   ID:         $Id$
 | 
|  |      4 |   Author:     Stefan Berghofer, TU Muenchen
 | 
|  |      5 | 
 | 
|  |      6 |   This class represents an ordinary vertex. It contains methods for
 | 
|  |      7 |   drawing and PostScript output.
 | 
|  |      8 | ***************************************************************************/
 | 
|  |      9 | 
 | 
|  |     10 | package GraphBrowser;
 | 
|  |     11 | 
 | 
|  |     12 | import java.util.*;
 | 
|  |     13 | import java.awt.*;
 | 
|  |     14 | import java.io.*;
 | 
|  |     15 | 
 | 
|  |     16 | class NormalVertex extends Vertex {
 | 
|  |     17 | 	String label="",path="",dir="",ID="";
 | 
|  |     18 | 	Vector up,down,inflate=null;
 | 
|  |     19 | 
 | 
|  |     20 | 	public Object clone() {
 | 
|  |     21 | 		Vertex ve=new NormalVertex(label);
 | 
|  |     22 |                 ve.setID(ID);
 | 
|  |     23 | 		ve.setNumber(getNumber());
 | 
|  |     24 | 		ve.setUp(getUp());ve.setDown(getDown());
 | 
|  |     25 | 		ve.setX(getX());ve.setY(getY());
 | 
|  |     26 | 		ve.setPath(getPath());
 | 
|  |     27 | 		return ve;
 | 
|  |     28 | 	}
 | 
|  |     29 | 
 | 
|  |     30 | 	/*** Constructor ***/
 | 
|  |     31 | 
 | 
|  |     32 | 	public NormalVertex(String s) { label=s; }
 | 
|  |     33 | 
 | 
|  |     34 | 	public void setInflate(Vector v) { inflate=v; }
 | 
|  |     35 | 
 | 
|  |     36 | 	public Vector getInflate() { return inflate; }
 | 
|  |     37 | 
 | 
|  |     38 | 	public Vector getUp() { return up; }
 | 
|  |     39 | 
 | 
|  |     40 | 	public void setUp(Vector v) { up=v; }
 | 
|  |     41 | 
 | 
|  |     42 | 	public Vector getDown() { return down; }
 | 
|  |     43 | 
 | 
|  |     44 | 	public void setDown(Vector v) { down=v; }
 | 
|  |     45 | 
 | 
|  |     46 | 	public String getLabel() {return label;}
 | 
|  |     47 | 
 | 
|  |     48 | 	public void setLabel(String s) {label=s;}
 | 
|  |     49 | 
 | 
|  |     50 | 	public void setID(String s) { ID=s; }
 | 
|  |     51 | 
 | 
|  |     52 |         public String getID() { return ID; }
 | 
|  |     53 | 
 | 
|  |     54 | 	public String getPath() { return path;}
 | 
|  |     55 | 
 | 
|  |     56 | 	public void setPath(String p) { path=p; }
 | 
|  |     57 | 
 | 
|  |     58 | 	public String getDir() { return dir; }
 | 
|  |     59 | 
 | 
|  |     60 | 	public void setDir(String d) { dir=d; }
 | 
|  |     61 | 
 | 
|  |     62 | 	public int leftX() { return getX()-gra.box_width2; }
 | 
|  |     63 | 
 | 
|  |     64 | 	public int rightX() { return getX()+gra.box_width2; }
 | 
|  |     65 | 
 | 
|  |     66 | 	public void drawBox(Graphics g,Color boxColor) {
 | 
| 11872 |     67 | 		FontMetrics fm = g.getFontMetrics(g.getFont());
 | 
| 3599 |     68 | 		int h=fm.getAscent()+fm.getDescent();
 | 
|  |     69 | 
 | 
|  |     70 | 		g.setColor(boxColor);
 | 
|  |     71 | 		g.fillRect(getX()-gra.box_width2,getY(),gra.box_width,gra.box_height);
 | 
|  |     72 | 		g.setColor(Color.black);
 | 
|  |     73 | 		g.drawRect(getX()-gra.box_width2,getY(),gra.box_width,gra.box_height);
 | 
|  |     74 | 		if (getNumber()<0) {
 | 
|  |     75 | 			g.setColor(Color.red);
 | 
|  |     76 | 			label=label.substring(1,label.length()-1);
 | 
|  |     77 | 			while (label.length()>0 && fm.stringWidth("["+label+"]")>gra.box_width-8)
 | 
|  |     78 | 					label=label.substring(0,label.length()-1);
 | 
|  |     79 | 			label="["+label+"]";
 | 
|  |     80 | 		}
 | 
|  |     81 | 
 | 
|  |     82 | 		g.drawString(label,
 | 
|  |     83 | 		             (int)Math.round((gra.box_width-fm.stringWidth(label))/2.0)+getX()-gra.box_width2,
 | 
|  |     84 | 				fm.getAscent()+(int)Math.round((gra.box_height-h)/2.0)+getY());
 | 
|  |     85 | 	}
 | 
|  |     86 | 
 | 
|  |     87 | 	public void removeButtons(Graphics g) {
 | 
|  |     88 | 		drawBox(g,Color.lightGray);
 | 
|  |     89 | 	}
 | 
|  |     90 | 
 | 
|  |     91 | 	public void draw(Graphics g) {
 | 
|  |     92 | 		drawBox(g,Color.lightGray);
 | 
|  |     93 | 		g.setColor(Color.black);
 | 
|  |     94 | 		Enumeration e1=getChildren();
 | 
|  |     95 | 		while (e1.hasMoreElements()) {
 | 
|  |     96 | 			Vertex v=(Vertex)(e1.nextElement());
 | 
|  |     97 | 			if (!v.isDummy())
 | 
|  |     98 | 				g.drawLine(getX(),getY()+gra.box_height,v.getX(),v.getY());
 | 
|  |     99 | 		}
 | 
|  |    100 | 	}
 | 
|  |    101 | 
 | 
|  |    102 | 	public boolean contains(int x,int y) {
 | 
|  |    103 | 		return (x>=leftX() && x<=rightX() && y>=getY() &&
 | 
|  |    104 |                         y<=getY()+gra.box_height);
 | 
|  |    105 | 	}
 | 
|  |    106 | 
 | 
|  |    107 | 	public boolean leftButton(int x,int y) {
 | 
|  |    108 | 		return contains(x,y) && x<=leftX()+gra.box_height && getParents().hasMoreElements() && getNumber()>=0;
 | 
|  |    109 | 	}
 | 
|  |    110 | 
 | 
|  |    111 | 	public boolean rightButton(int x,int y) {
 | 
|  |    112 | 		return contains(x,y) && x>=rightX()-gra.box_height && getChildren().hasMoreElements() && getNumber()>=0;
 | 
|  |    113 | 	}
 | 
|  |    114 | 
 | 
|  |    115 | 	public void drawButtons(Graphics g) {
 | 
|  |    116 | 		if (getNumber()<0) return;
 | 
|  |    117 | 
 | 
|  |    118 | 		int l=gra.box_height*2/3,d=gra.box_height/6;
 | 
|  |    119 | 		int up_x[] = { leftX()+d , leftX()+d+l/2 , leftX()+d+l };
 | 
|  |    120 | 		int up_y[] = { getY()+d+l , getY()+d , getY()+d+l };
 | 
|  |    121 | 		int down_x[] = { rightX()-d-l , rightX()-d-l/2 , rightX()-d };
 | 
|  |    122 | 		int down_y[] = { getY()+d , getY()+d+l , getY()+d };
 | 
|  |    123 | 
 | 
|  |    124 | 		if (getParents().hasMoreElements()) {
 | 
|  |    125 | 			g.setColor(Color.gray);
 | 
|  |    126 | 			g.fillRect(leftX()+1,getY()+1,gra.box_height-1,gra.box_height-1);
 | 
|  |    127 | 			g.setColor(getUp()!=null ? Color.red : Color.green);
 | 
|  |    128 | 			g.fillPolygon(up_x,up_y,3);
 | 
|  |    129 | 		}
 | 
|  |    130 | 		if (getChildren().hasMoreElements()) {
 | 
|  |    131 | 			g.setColor(Color.gray);
 | 
|  |    132 | 			g.fillRect(rightX()+1-gra.box_height,getY()+1,gra.box_height,gra.box_height-1);
 | 
|  |    133 | 			g.setColor(getDown()!=null ? Color.red : Color.green);
 | 
|  |    134 | 			g.fillPolygon(down_x,down_y,3);
 | 
|  |    135 | 		}
 | 
|  |    136 | 		g.setColor(Color.black);
 | 
|  |    137 | 	}
 | 
|  |    138 | 
 | 
| 6541 |    139 | 	public void PS(PrintWriter p) {
 | 
| 3599 |    140 | 		p.print(leftX()+" "+getY()+" "+gra.box_width+" "+
 | 
|  |    141 | 		        gra.box_height+" (");
 | 
|  |    142 | 		for (int i=0;i<label.length();i++)
 | 
|  |    143 | 		{
 | 
|  |    144 | 			if (("()\\").indexOf(label.charAt(i))>=0)
 | 
|  |    145 | 				p.print("\\");
 | 
|  |    146 | 			p.print(label.charAt(i));
 | 
|  |    147 | 		}
 | 
|  |    148 | 		p.println(") b");
 | 
|  |    149 | 
 | 
|  |    150 | 		Enumeration e1=getChildren();
 | 
|  |    151 | 		while (e1.hasMoreElements()) {
 | 
|  |    152 | 			Vertex v=(Vertex)(e1.nextElement());
 | 
|  |    153 | 			if (!v.isDummy())
 | 
|  |    154 | 				p.println("n "+getX()+" "+(getY()+gra.box_height)+
 | 
|  |    155 | 				" m "+v.getX()+" "+v.getY()+" l s");
 | 
|  |    156 | 		}
 | 
|  |    157 | 	}	
 | 
|  |    158 | }
 | 
|  |    159 | 		
 |