lib/browser/GraphBrowser/NormalVertex.java
author blanchet
Wed, 04 Aug 2010 23:27:27 +0200
changeset 38195 a8cef06e0480
parent 37738 7bf3ec9e7b0c
child 50473 ca4088bf8365
permissions -rw-r--r--
Cycle breaking in the bounds takes care of singly recursive datatypes, so we don't need to do it again; the effect of removing the constraint varies on problem to problem, but it tends to be overwhelmingly negative in conjuction with the new datatype sym breaking stuff at high cardinalities
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
3599
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
     1
/***************************************************************************
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
     2
  Title:      GraphBrowser/NormalVertex.java
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
     3
  Author:     Stefan Berghofer, TU Muenchen
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
     4
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
     5
  This class represents an ordinary vertex. It contains methods for
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
     6
  drawing and PostScript output.
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
     7
***************************************************************************/
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
     8
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
     9
package GraphBrowser;
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    10
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    11
import java.util.*;
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    12
import java.awt.*;
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    13
import java.io.*;
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    14
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    15
class NormalVertex extends Vertex {
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    16
	String label="",path="",dir="",ID="";
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    17
	Vector up,down,inflate=null;
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    18
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    19
	public Object clone() {
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    20
		Vertex ve=new NormalVertex(label);
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    21
                ve.setID(ID);
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    22
		ve.setNumber(getNumber());
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    23
		ve.setUp(getUp());ve.setDown(getDown());
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    24
		ve.setX(getX());ve.setY(getY());
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    25
		ve.setPath(getPath());
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    26
		return ve;
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    27
	}
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    28
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    29
	/*** Constructor ***/
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    30
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    31
	public NormalVertex(String s) { label=s; }
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    32
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    33
	public void setInflate(Vector v) { inflate=v; }
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    34
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    35
	public Vector getInflate() { return inflate; }
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    36
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    37
	public Vector getUp() { return up; }
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    38
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    39
	public void setUp(Vector v) { up=v; }
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    40
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    41
	public Vector getDown() { return down; }
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    42
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    43
	public void setDown(Vector v) { down=v; }
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    44
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    45
	public String getLabel() {return label;}
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    46
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    47
	public void setLabel(String s) {label=s;}
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    48
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    49
	public void setID(String s) { ID=s; }
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    50
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    51
        public String getID() { return ID; }
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    52
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    53
	public String getPath() { return path;}
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    54
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    55
	public void setPath(String p) { path=p; }
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    56
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    57
	public String getDir() { return dir; }
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    58
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    59
	public void setDir(String d) { dir=d; }
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    60
37738
7bf3ec9e7b0c Boxes may now have different widths.
berghofe
parents: 33686
diff changeset
    61
	public int leftX() { return getX()-box_width2(); }
3599
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    62
37738
7bf3ec9e7b0c Boxes may now have different widths.
berghofe
parents: 33686
diff changeset
    63
	public int rightX() { return getX()+box_width2(); }
3599
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    64
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    65
	public void drawBox(Graphics g,Color boxColor) {
11872
4f24fd4dbcf5 Moved font settings from Vertex to GraphView.
berghofe
parents: 6541
diff changeset
    66
		FontMetrics fm = g.getFontMetrics(g.getFont());
3599
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    67
		int h=fm.getAscent()+fm.getDescent();
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    68
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    69
		g.setColor(boxColor);
37738
7bf3ec9e7b0c Boxes may now have different widths.
berghofe
parents: 33686
diff changeset
    70
		g.fillRect(getX()-box_width2(),getY(),box_width(),gra.box_height);
3599
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    71
		g.setColor(Color.black);
37738
7bf3ec9e7b0c Boxes may now have different widths.
berghofe
parents: 33686
diff changeset
    72
		g.drawRect(getX()-box_width2(),getY(),box_width(),gra.box_height);
7bf3ec9e7b0c Boxes may now have different widths.
berghofe
parents: 33686
diff changeset
    73
		if (getNumber()<0)
3599
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    74
			g.setColor(Color.red);
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    75
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    76
		g.drawString(label,
37738
7bf3ec9e7b0c Boxes may now have different widths.
berghofe
parents: 33686
diff changeset
    77
		             (int)Math.round((box_width()-fm.stringWidth(label))/2.0)+getX()-box_width2(),
3599
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    78
				fm.getAscent()+(int)Math.round((gra.box_height-h)/2.0)+getY());
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    79
	}
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    80
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    81
	public void removeButtons(Graphics g) {
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    82
		drawBox(g,Color.lightGray);
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    83
	}
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    84
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    85
	public void draw(Graphics g) {
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    86
		drawBox(g,Color.lightGray);
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    87
		g.setColor(Color.black);
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    88
		Enumeration e1=getChildren();
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    89
		while (e1.hasMoreElements()) {
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    90
			Vertex v=(Vertex)(e1.nextElement());
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    91
			if (!v.isDummy())
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    92
				g.drawLine(getX(),getY()+gra.box_height,v.getX(),v.getY());
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    93
		}
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    94
	}
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    95
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    96
	public boolean contains(int x,int y) {
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    97
		return (x>=leftX() && x<=rightX() && y>=getY() &&
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    98
                        y<=getY()+gra.box_height);
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    99
	}
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   100
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   101
	public boolean leftButton(int x,int y) {
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   102
		return contains(x,y) && x<=leftX()+gra.box_height && getParents().hasMoreElements() && getNumber()>=0;
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   103
	}
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   104
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   105
	public boolean rightButton(int x,int y) {
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   106
		return contains(x,y) && x>=rightX()-gra.box_height && getChildren().hasMoreElements() && getNumber()>=0;
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   107
	}
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   108
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   109
	public void drawButtons(Graphics g) {
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   110
		if (getNumber()<0) return;
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   111
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   112
		int l=gra.box_height*2/3,d=gra.box_height/6;
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   113
		int up_x[] = { leftX()+d , leftX()+d+l/2 , leftX()+d+l };
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   114
		int up_y[] = { getY()+d+l , getY()+d , getY()+d+l };
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   115
		int down_x[] = { rightX()-d-l , rightX()-d-l/2 , rightX()-d };
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   116
		int down_y[] = { getY()+d , getY()+d+l , getY()+d };
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   117
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   118
		if (getParents().hasMoreElements()) {
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   119
			g.setColor(Color.gray);
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   120
			g.fillRect(leftX()+1,getY()+1,gra.box_height-1,gra.box_height-1);
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   121
			g.setColor(getUp()!=null ? Color.red : Color.green);
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   122
			g.fillPolygon(up_x,up_y,3);
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   123
		}
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   124
		if (getChildren().hasMoreElements()) {
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   125
			g.setColor(Color.gray);
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   126
			g.fillRect(rightX()+1-gra.box_height,getY()+1,gra.box_height,gra.box_height-1);
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   127
			g.setColor(getDown()!=null ? Color.red : Color.green);
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   128
			g.fillPolygon(down_x,down_y,3);
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   129
		}
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   130
		g.setColor(Color.black);
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   131
	}
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   132
6541
d3ac35b2bfbf Updated to JDK 1.1.x
berghofe
parents: 3599
diff changeset
   133
	public void PS(PrintWriter p) {
37738
7bf3ec9e7b0c Boxes may now have different widths.
berghofe
parents: 33686
diff changeset
   134
		p.print(leftX()+" "+getY()+" "+box_width()+" "+
3599
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   135
		        gra.box_height+" (");
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   136
		for (int i=0;i<label.length();i++)
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   137
		{
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   138
			if (("()\\").indexOf(label.charAt(i))>=0)
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   139
				p.print("\\");
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   140
			p.print(label.charAt(i));
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   141
		}
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   142
		p.println(") b");
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   143
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   144
		Enumeration e1=getChildren();
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   145
		while (e1.hasMoreElements()) {
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   146
			Vertex v=(Vertex)(e1.nextElement());
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   147
			if (!v.isDummy())
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   148
				p.println("n "+getX()+" "+(getY()+gra.box_height)+
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   149
				" m "+v.getX()+" "+v.getY()+" l s");
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   150
		}
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   151
	}	
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   152
}
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   153