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