src/Tools/GraphBrowser/graphbrowser/NormalVertex.java

clarified names;

/***************************************************************************
  Title:      graphbrowser/NormalVertex.java
  Author:     Stefan Berghofer, TU Muenchen
  Options:    :tabSize=4:

  This class represents an ordinary vertex. It contains methods for
  drawing and PostScript output.
***************************************************************************/

package isabelle.graphbrowser;

import java.util.*;
import java.awt.*;
import java.io.*;

class NormalVertex extends Vertex {
	String label="",path="",dir="",ID="";
	Vector up,down,inflate=null;

	public Object clone() {
		Vertex ve=new NormalVertex(label);
                ve.setID(ID);
		ve.setNumber(getNumber());
		ve.setUp(getUp());ve.setDown(getDown());
		ve.setX(getX());ve.setY(getY());
		ve.setPath(getPath());
		return ve;
	}

	/*** Constructor ***/

	public NormalVertex(String s) { label=s; }

	public void setInflate(Vector v) { inflate=v; }

	public Vector getInflate() { return inflate; }

	public Vector getUp() { return up; }

	public void setUp(Vector v) { up=v; }

	public Vector getDown() { return down; }

	public void setDown(Vector v) { down=v; }

	public String getLabel() {return label;}

	public void setLabel(String s) {label=s;}

	public void setID(String s) { ID=s; }

        public String getID() { return ID; }

	public String getPath() { return path;}

	public void setPath(String p) { path=p; }

	public String getDir() { return dir; }

	public void setDir(String d) { dir=d; }

	public int leftX() { return getX()-box_width2(); }

	public int rightX() { return getX()+box_width2(); }

	public void drawBox(Graphics g,Color boxColor) {
		FontMetrics fm = g.getFontMetrics(g.getFont());
		int h=fm.getAscent()+fm.getDescent();

		g.setColor(boxColor);
		g.fillRect(getX()-box_width2(),getY(),box_width(),gra.box_height);
		g.setColor(Color.black);
		g.drawRect(getX()-box_width2(),getY(),box_width(),gra.box_height);
		if (getNumber()<0)
			g.setColor(Color.red);

		g.drawString(label,
		             (int)Math.round((box_width()-fm.stringWidth(label))/2.0)+getX()-box_width2(),
				fm.getAscent()+(int)Math.round((gra.box_height-h)/2.0)+getY());
	}

	public void removeButtons(Graphics g) {
		drawBox(g,Color.lightGray);
	}

	public void draw(Graphics g) {
		drawBox(g,Color.lightGray);
		g.setColor(Color.black);
		Enumeration e1=getChildren();
		while (e1.hasMoreElements()) {
			Vertex v=(Vertex)(e1.nextElement());
			if (!v.isDummy())
				g.drawLine(getX(),getY()+gra.box_height,v.getX(),v.getY());
		}
	}

	public boolean contains(int x,int y) {
		return (x>=leftX() && x<=rightX() && y>=getY() &&
                        y<=getY()+gra.box_height);
	}

	public boolean leftButton(int x,int y) {
		return contains(x,y) && x<=leftX()+gra.box_height && getParents().hasMoreElements() && getNumber()>=0;
	}

	public boolean rightButton(int x,int y) {
		return contains(x,y) && x>=rightX()-gra.box_height && getChildren().hasMoreElements() && getNumber()>=0;
	}

	public void drawButtons(Graphics g) {
		if (getNumber()<0) return;

		int l=gra.box_height*2/3,d=gra.box_height/6;
		int up_x[] = { leftX()+d , leftX()+d+l/2 , leftX()+d+l };
		int up_y[] = { getY()+d+l , getY()+d , getY()+d+l };
		int down_x[] = { rightX()-d-l , rightX()-d-l/2 , rightX()-d };
		int down_y[] = { getY()+d , getY()+d+l , getY()+d };

		if (getParents().hasMoreElements()) {
			g.setColor(Color.gray);
			g.fillRect(leftX()+1,getY()+1,gra.box_height-1,gra.box_height-1);
			g.setColor(getUp()!=null ? Color.red : Color.green);
			g.fillPolygon(up_x,up_y,3);
		}
		if (getChildren().hasMoreElements()) {
			g.setColor(Color.gray);
			g.fillRect(rightX()+1-gra.box_height,getY()+1,gra.box_height,gra.box_height-1);
			g.setColor(getDown()!=null ? Color.red : Color.green);
			g.fillPolygon(down_x,down_y,3);
		}
		g.setColor(Color.black);
	}

	public void PS(PrintWriter p) {
		p.print(leftX()+" "+getY()+" "+box_width()+" "+
		        gra.box_height+" (");
		for (int i=0;i<label.length();i++)
		{
			if (("()\\").indexOf(label.charAt(i))>=0)
				p.print("\\");
			p.print(label.charAt(i));
		}
		p.println(") b");

		Enumeration e1=getChildren();
		while (e1.hasMoreElements()) {
			Vertex v=(Vertex)(e1.nextElement());
			if (!v.isDummy())
				p.println("n "+getX()+" "+(getY()+gra.box_height)+
				" m "+v.getX()+" "+v.getY()+" l s");
		}
	}	
}