lib/browser/GraphBrowser/NormalVertex.java
author eberlm <eberlm@in.tum.de>
Thu, 30 Nov 2017 16:59:59 +0100
changeset 67107 cef76a19125e
parent 50473 ca4088bf8365
permissions -rw-r--r--
Existence of a holomorphic logarithm
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
50473
ca4088bf8365 added speculative options for jEdit;
wenzelm
parents: 37738
diff changeset
     4
  Options:    :tabSize=4:
3599
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
     5
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
     6
  This class represents an ordinary vertex. It contains methods for
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
     7
  drawing and PostScript output.
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
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    10
package GraphBrowser;
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    11
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    12
import java.util.*;
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    13
import java.awt.*;
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    14
import java.io.*;
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    15
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    16
class NormalVertex extends Vertex {
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    17
	String label="",path="",dir="",ID="";
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    18
	Vector up,down,inflate=null;
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    19
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    20
	public Object clone() {
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    21
		Vertex ve=new NormalVertex(label);
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    22
                ve.setID(ID);
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    23
		ve.setNumber(getNumber());
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    24
		ve.setUp(getUp());ve.setDown(getDown());
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    25
		ve.setX(getX());ve.setY(getY());
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    26
		ve.setPath(getPath());
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    27
		return ve;
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
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    30
	/*** Constructor ***/
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    31
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    32
	public NormalVertex(String s) { label=s; }
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    33
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    34
	public void setInflate(Vector v) { inflate=v; }
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    35
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    36
	public Vector getInflate() { return inflate; }
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    37
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    38
	public Vector getUp() { return up; }
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    39
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    40
	public void setUp(Vector v) { up=v; }
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    41
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    42
	public Vector getDown() { return down; }
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    43
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    44
	public void setDown(Vector v) { down=v; }
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    45
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    46
	public String getLabel() {return label;}
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    47
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    48
	public void setLabel(String s) {label=s;}
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    49
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    50
	public void setID(String s) { ID=s; }
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    51
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    52
        public String getID() { return ID; }
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    53
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    54
	public String getPath() { return path;}
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    55
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    56
	public void setPath(String p) { path=p; }
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    57
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    58
	public String getDir() { return dir; }
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    59
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    60
	public void setDir(String d) { dir=d; }
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    61
37738
7bf3ec9e7b0c Boxes may now have different widths.
berghofe
parents: 33686
diff changeset
    62
	public int leftX() { return getX()-box_width2(); }
3599
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    63
37738
7bf3ec9e7b0c Boxes may now have different widths.
berghofe
parents: 33686
diff changeset
    64
	public int rightX() { return getX()+box_width2(); }
3599
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    65
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    66
	public void drawBox(Graphics g,Color boxColor) {
11872
4f24fd4dbcf5 Moved font settings from Vertex to GraphView.
berghofe
parents: 6541
diff changeset
    67
		FontMetrics fm = g.getFontMetrics(g.getFont());
3599
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    68
		int h=fm.getAscent()+fm.getDescent();
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    69
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    70
		g.setColor(boxColor);
37738
7bf3ec9e7b0c Boxes may now have different widths.
berghofe
parents: 33686
diff changeset
    71
		g.fillRect(getX()-box_width2(),getY(),box_width(),gra.box_height);
3599
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    72
		g.setColor(Color.black);
37738
7bf3ec9e7b0c Boxes may now have different widths.
berghofe
parents: 33686
diff changeset
    73
		g.drawRect(getX()-box_width2(),getY(),box_width(),gra.box_height);
7bf3ec9e7b0c Boxes may now have different widths.
berghofe
parents: 33686
diff changeset
    74
		if (getNumber()<0)
3599
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    75
			g.setColor(Color.red);
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    76
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    77
		g.drawString(label,
37738
7bf3ec9e7b0c Boxes may now have different widths.
berghofe
parents: 33686
diff changeset
    78
		             (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
    79
				fm.getAscent()+(int)Math.round((gra.box_height-h)/2.0)+getY());
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
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    82
	public void removeButtons(Graphics g) {
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    83
		drawBox(g,Color.lightGray);
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
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    86
	public void draw(Graphics g) {
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    87
		drawBox(g,Color.lightGray);
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    88
		g.setColor(Color.black);
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    89
		Enumeration e1=getChildren();
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    90
		while (e1.hasMoreElements()) {
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    91
			Vertex v=(Vertex)(e1.nextElement());
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    92
			if (!v.isDummy())
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    93
				g.drawLine(getX(),getY()+gra.box_height,v.getX(),v.getY());
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
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    97
	public boolean contains(int x,int y) {
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    98
		return (x>=leftX() && x<=rightX() && y>=getY() &&
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    99
                        y<=getY()+gra.box_height);
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
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   102
	public boolean leftButton(int x,int y) {
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   103
		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
   104
	}
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   105
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   106
	public boolean rightButton(int x,int y) {
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   107
		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
   108
	}
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   109
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   110
	public void drawButtons(Graphics g) {
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   111
		if (getNumber()<0) return;
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   112
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   113
		int l=gra.box_height*2/3,d=gra.box_height/6;
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   114
		int up_x[] = { leftX()+d , leftX()+d+l/2 , leftX()+d+l };
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   115
		int up_y[] = { getY()+d+l , getY()+d , getY()+d+l };
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   116
		int down_x[] = { rightX()-d-l , rightX()-d-l/2 , rightX()-d };
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   117
		int down_y[] = { getY()+d , getY()+d+l , getY()+d };
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   118
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   119
		if (getParents().hasMoreElements()) {
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   120
			g.setColor(Color.gray);
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   121
			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
   122
			g.setColor(getUp()!=null ? Color.red : Color.green);
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   123
			g.fillPolygon(up_x,up_y,3);
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   124
		}
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   125
		if (getChildren().hasMoreElements()) {
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   126
			g.setColor(Color.gray);
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   127
			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
   128
			g.setColor(getDown()!=null ? Color.red : Color.green);
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   129
			g.fillPolygon(down_x,down_y,3);
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   130
		}
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   131
		g.setColor(Color.black);
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   132
	}
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   133
6541
d3ac35b2bfbf Updated to JDK 1.1.x
berghofe
parents: 3599
diff changeset
   134
	public void PS(PrintWriter p) {
37738
7bf3ec9e7b0c Boxes may now have different widths.
berghofe
parents: 33686
diff changeset
   135
		p.print(leftX()+" "+getY()+" "+box_width()+" "+
3599
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   136
		        gra.box_height+" (");
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   137
		for (int i=0;i<label.length();i++)
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   138
		{
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   139
			if (("()\\").indexOf(label.charAt(i))>=0)
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   140
				p.print("\\");
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   141
			p.print(label.charAt(i));
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   142
		}
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   143
		p.println(") b");
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   144
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   145
		Enumeration e1=getChildren();
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   146
		while (e1.hasMoreElements()) {
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   147
			Vertex v=(Vertex)(e1.nextElement());
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   148
			if (!v.isDummy())
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   149
				p.println("n "+getX()+" "+(getY()+gra.box_height)+
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   150
				" m "+v.getX()+" "+v.getY()+" l s");
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
}
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   154