src/Tools/GraphBrowser/GraphBrowser/NormalVertex.java
changeset 74015 12b1f4649ab1
parent 74014 3b8b1da2ff29
child 74016 027fb21bdd5d
equal deleted inserted replaced
74014:3b8b1da2ff29 74015:12b1f4649ab1
     1 /***************************************************************************
       
     2   Title:      GraphBrowser/NormalVertex.java
       
     3   Author:     Stefan Berghofer, TU Muenchen
       
     4   Options:    :tabSize=4:
       
     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()-box_width2(); }
       
    63 
       
    64 	public int rightX() { return getX()+box_width2(); }
       
    65 
       
    66 	public void drawBox(Graphics g,Color boxColor) {
       
    67 		FontMetrics fm = g.getFontMetrics(g.getFont());
       
    68 		int h=fm.getAscent()+fm.getDescent();
       
    69 
       
    70 		g.setColor(boxColor);
       
    71 		g.fillRect(getX()-box_width2(),getY(),box_width(),gra.box_height);
       
    72 		g.setColor(Color.black);
       
    73 		g.drawRect(getX()-box_width2(),getY(),box_width(),gra.box_height);
       
    74 		if (getNumber()<0)
       
    75 			g.setColor(Color.red);
       
    76 
       
    77 		g.drawString(label,
       
    78 		             (int)Math.round((box_width()-fm.stringWidth(label))/2.0)+getX()-box_width2(),
       
    79 				fm.getAscent()+(int)Math.round((gra.box_height-h)/2.0)+getY());
       
    80 	}
       
    81 
       
    82 	public void removeButtons(Graphics g) {
       
    83 		drawBox(g,Color.lightGray);
       
    84 	}
       
    85 
       
    86 	public void draw(Graphics g) {
       
    87 		drawBox(g,Color.lightGray);
       
    88 		g.setColor(Color.black);
       
    89 		Enumeration e1=getChildren();
       
    90 		while (e1.hasMoreElements()) {
       
    91 			Vertex v=(Vertex)(e1.nextElement());
       
    92 			if (!v.isDummy())
       
    93 				g.drawLine(getX(),getY()+gra.box_height,v.getX(),v.getY());
       
    94 		}
       
    95 	}
       
    96 
       
    97 	public boolean contains(int x,int y) {
       
    98 		return (x>=leftX() && x<=rightX() && y>=getY() &&
       
    99                         y<=getY()+gra.box_height);
       
   100 	}
       
   101 
       
   102 	public boolean leftButton(int x,int y) {
       
   103 		return contains(x,y) && x<=leftX()+gra.box_height && getParents().hasMoreElements() && getNumber()>=0;
       
   104 	}
       
   105 
       
   106 	public boolean rightButton(int x,int y) {
       
   107 		return contains(x,y) && x>=rightX()-gra.box_height && getChildren().hasMoreElements() && getNumber()>=0;
       
   108 	}
       
   109 
       
   110 	public void drawButtons(Graphics g) {
       
   111 		if (getNumber()<0) return;
       
   112 
       
   113 		int l=gra.box_height*2/3,d=gra.box_height/6;
       
   114 		int up_x[] = { leftX()+d , leftX()+d+l/2 , leftX()+d+l };
       
   115 		int up_y[] = { getY()+d+l , getY()+d , getY()+d+l };
       
   116 		int down_x[] = { rightX()-d-l , rightX()-d-l/2 , rightX()-d };
       
   117 		int down_y[] = { getY()+d , getY()+d+l , getY()+d };
       
   118 
       
   119 		if (getParents().hasMoreElements()) {
       
   120 			g.setColor(Color.gray);
       
   121 			g.fillRect(leftX()+1,getY()+1,gra.box_height-1,gra.box_height-1);
       
   122 			g.setColor(getUp()!=null ? Color.red : Color.green);
       
   123 			g.fillPolygon(up_x,up_y,3);
       
   124 		}
       
   125 		if (getChildren().hasMoreElements()) {
       
   126 			g.setColor(Color.gray);
       
   127 			g.fillRect(rightX()+1-gra.box_height,getY()+1,gra.box_height,gra.box_height-1);
       
   128 			g.setColor(getDown()!=null ? Color.red : Color.green);
       
   129 			g.fillPolygon(down_x,down_y,3);
       
   130 		}
       
   131 		g.setColor(Color.black);
       
   132 	}
       
   133 
       
   134 	public void PS(PrintWriter p) {
       
   135 		p.print(leftX()+" "+getY()+" "+box_width()+" "+
       
   136 		        gra.box_height+" (");
       
   137 		for (int i=0;i<label.length();i++)
       
   138 		{
       
   139 			if (("()\\").indexOf(label.charAt(i))>=0)
       
   140 				p.print("\\");
       
   141 			p.print(label.charAt(i));
       
   142 		}
       
   143 		p.println(") b");
       
   144 
       
   145 		Enumeration e1=getChildren();
       
   146 		while (e1.hasMoreElements()) {
       
   147 			Vertex v=(Vertex)(e1.nextElement());
       
   148 			if (!v.isDummy())
       
   149 				p.println("n "+getX()+" "+(getY()+gra.box_height)+
       
   150 				" m "+v.getX()+" "+v.getY()+" l s");
       
   151 		}
       
   152 	}	
       
   153 }
       
   154