lib/browser/GraphBrowser/Graph.java
author wenzelm
Sun, 28 Nov 2010 14:01:20 +0100
changeset 40781 ba5be5c3d477
parent 37738 7bf3ec9e7b0c
child 50473 ca4088bf8365
permissions -rw-r--r--
updated versions;
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/Graph.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 contains the core of the layout algorithm and 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
public class Graph {
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    16
	/**** parameters for layout ****/
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    17
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    18
	public int box_height=0;
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    19
	public int box_height2;
37738
7bf3ec9e7b0c Boxes may now have different widths.
berghofe
parents: 33686
diff changeset
    20
	public Graphics gfx;
3599
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    21
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    22
	Vector vertices=new Vector(10,10);
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    23
	Vector splines=new Vector(10,10);
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    24
	Vector numEdges=new Vector(10,10);
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    25
	Vertex []vertices2;
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    26
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    27
	public int min_x=0,min_y=0,max_x=10,max_y=10;
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
	/*                         clone graph object                       */
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
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    33
	public Object clone() {
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    34
		Graph gr=new Graph();
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    35
		Enumeration e1;
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    36
		int i;
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
		gr.splines=(Vector)(splines.clone());
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
		e1=vertices.elements();
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    41
		while (e1.hasMoreElements())
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    42
			gr.addVertex((Vertex)(((Vertex)(e1.nextElement())).clone()));
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
		for (i=0;i<vertices.size();i++) {
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    45
			Vertex vx1=(Vertex)(gr.vertices.elementAt(i));
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    46
			e1=((Vertex)(vertices.elementAt(i))).getChildren();
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    47
			while (e1.hasMoreElements()) {
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    48
				Vertex vx2=(Vertex)(gr.vertices.elementAt(vertices.indexOf(e1.nextElement())));
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    49
				vx1.addChild(vx2);
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
		}
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
		gr.vertices2 = new Vertex[vertices.size()];
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    54
		gr.vertices.copyInto(gr.vertices2);
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
		gr.min_x=min_x;gr.max_x=max_x;
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    57
		gr.min_y=min_y;gr.max_y=max_y;
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
		return gr;
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    60
	}
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    61
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    62
	Graph() {}
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    63
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
	/*                      Read graph from stream                      */
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    66
	/********************************************************************/
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    67
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    68
	public Graph(InputStream s,TreeNode tn) throws IOException, ParseError {
6541
d3ac35b2bfbf Updated to JDK 1.1.x
berghofe
parents: 3599
diff changeset
    69
		StreamTokenizer tok=new StreamTokenizer(new InputStreamReader(s));
3599
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    70
		String name,dir,vertexID;
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    71
		Vertex ve1,ve2;
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    72
		boolean children,unfoldDir;
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    73
		int index=0;
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    74
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    75
		tok.nextToken();
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    76
		while (tok.ttype!=StreamTokenizer.TT_EOF) {
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    77
			if (tok.ttype!=StreamTokenizer.TT_WORD && tok.ttype!='"')
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    78
				throw new ParseError("expected: vertex name\nfound   : "+tok.toString());
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    79
			name=tok.sval;
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    80
                        tok.nextToken();
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    81
			if (tok.ttype!=StreamTokenizer.TT_WORD && tok.ttype!='"')
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    82
				throw new ParseError("expected: vertex identifier\nfound   : "+tok.toString());
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    83
			vertexID=tok.sval;
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    84
			tok.nextToken();
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    85
			if (tok.ttype!=StreamTokenizer.TT_WORD && tok.ttype!='"')
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    86
				throw new ParseError("expected: directory name\nfound   : "+tok.toString());
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    87
			dir=tok.sval;
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    88
			tok.nextToken();
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    89
			if (tok.ttype=='+') {
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    90
				unfoldDir=true;
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    91
				tok.nextToken();
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    92
			} else
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    93
				unfoldDir=false;
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    94
			if (tok.ttype!=StreamTokenizer.TT_WORD && tok.ttype!='"')
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    95
				throw new ParseError("expected: path name\nfound   : "+tok.toString());
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    96
			ve1=findVertex(vertexID);
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    97
			if (ve1==null) {
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    98
				ve1=new NormalVertex("");
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    99
				ve1.setID(vertexID);
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   100
				ve1.setNumber(index++);
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   101
				addVertex(ve1);
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   102
			}
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   103
			ve1.setPath(tok.sval);
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   104
			ve1.setDir(dir);
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   105
                        ve1.setLabel(name);
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   106
			tn.insertNode(name,dir,tok.sval,ve1.getNumber(),unfoldDir);
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   107
			tok.nextToken();
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   108
			if (tok.ttype=='<') {
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   109
				children=true;
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   110
				tok.nextToken();
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   111
			} else if (tok.ttype=='>') {
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   112
					children=false;
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   113
					tok.nextToken();
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   114
			} else children=true;
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   115
			while (tok.ttype!=';') {
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   116
				if (tok.ttype!=StreamTokenizer.TT_WORD && tok.ttype!='"')
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   117
					throw new ParseError("expected: child vertex identifier or ';'\nfound   : "+tok.toString());				
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   118
				ve2=findVertex(tok.sval);
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   119
				if (ve2==null) {
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   120
					ve2=new NormalVertex("");
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   121
					ve2.setID(tok.sval);
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   122
					ve2.setNumber(index++);
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   123
					addVertex(ve2);
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 (children)
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   126
					ve1.addChild(ve2);
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   127
				else
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   128
					ve1.addParent(ve2);
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   129
				tok.nextToken();
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
			tok.nextToken();
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
		vertices2 = new Vertex[vertices.size()];
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   134
		vertices.copyInto(vertices2);
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   135
	}
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   136
	
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   137
	/*** Find vertex with identifier vertexID ***/
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
	public Vertex findVertex(String vertexID) {
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   140
		Enumeration e1=vertices.elements();
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   141
		Vertex v1;
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
		while (e1.hasMoreElements()) {
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   144
			v1=(Vertex)(e1.nextElement());
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   145
			if ((v1.getID()).equals(vertexID))
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   146
				return v1;
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   147
		}
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   148
		return null;
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   149
	}
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
	public void addVertex(Vertex v) {
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   152
		vertices.addElement(v);
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   153
		v.setGraph(this);
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   154
	}
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   155
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   156
	public void removeVertex(Vertex v) {
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   157
		vertices.removeElement(v);
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   158
	}
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   159
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   160
	public Enumeration getVertices() {
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   161
		return vertices.elements();
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   162
	}
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   163
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   164
	/********************************************************************/
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   165
	/*                          graph layout                            */
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   166
	/********************************************************************/
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   167
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   168
	public void layout(Graphics g) {
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   169
		splines.removeAllElements();
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   170
		hasseDiagram();
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   171
		Vector layers=min_crossings(insert_dummies((Vector)(sort().elementAt(0))));
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   172
		setParameters(g);
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   173
		init_coordinates(layers);
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   174
		pendulum(layers);
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   175
		rubberband(layers);
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   176
		calcSplines(layers);
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   177
		calcBoundingBox();
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   178
	}
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   179
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   180
	/********************************************************************/
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   181
	/*                      set layout parameters                       */
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   182
	/********************************************************************/
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   183
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   184
	public void setParameters(Graphics g) {
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   185
		Enumeration e1=vertices.elements();
37738
7bf3ec9e7b0c Boxes may now have different widths.
berghofe
parents: 33686
diff changeset
   186
		int h;
7bf3ec9e7b0c Boxes may now have different widths.
berghofe
parents: 33686
diff changeset
   187
		h=Integer.MIN_VALUE;
3599
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   188
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   189
		while (e1.hasMoreElements()) {
13968
689868b99bde eliminated dependencies on AWT for batch mode
kleing
parents: 6541
diff changeset
   190
		  Box dim=((Vertex)(e1.nextElement())).getLabelSize(g);
3599
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   191
			h=Math.max(h,dim.height);
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   192
		}
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   193
		box_height=h+4;
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   194
		box_height2=box_height/2;
37738
7bf3ec9e7b0c Boxes may now have different widths.
berghofe
parents: 33686
diff changeset
   195
		gfx=g;
3599
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   196
	}
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   197
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   198
	/********************************************************************/
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   199
	/*                       topological sorting                        */
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   200
	/********************************************************************/
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   201
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   202
	public Vector sort() {
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   203
		Vector todo=(Vector)(vertices.clone());
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   204
		Vector layers=new Vector(10,10);
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   205
		Vector todo2;
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   206
		Enumeration e1,e2;
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   207
		Vertex v,v2;
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   208
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   209
		e1=vertices.elements();
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   210
		while (e1.hasMoreElements())
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   211
			((Vertex)(e1.nextElement())).setDegree(0);
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   212
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   213
		e1=vertices.elements();
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   214
		while (e1.hasMoreElements()) {
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   215
			v=(Vertex)(e1.nextElement());
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   216
			e2=v.getChildren();
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   217
			while (e2.hasMoreElements()) {
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   218
				v2=(Vertex)(e2.nextElement());
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   219
				todo.removeElement(v2);
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   220
				v2.setDegree(1+v2.getDegree());
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   221
			}
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   222
		}
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   223
		while (!todo.isEmpty()) {
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   224
			layers.addElement(todo);
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   225
			todo2=new Vector(10,10);
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   226
			e1=todo.elements();
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   227
			while (e1.hasMoreElements()) {
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   228
				e2=((Vertex)(e1.nextElement())).getChildren();
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   229
				while (e2.hasMoreElements()) {
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   230
					v=(Vertex)(e2.nextElement());
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   231
					v.setDegree(v.getDegree()-1);
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   232
					if (v.getDegree()==0) {
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   233
						todo2.addElement(v);
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   234
						v.setDegree(layers.size());
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   235
					}
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   236
				}
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   237
			}
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   238
			todo=todo2;
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   239
		}
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   240
		return layers;
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   241
	}
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   242
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   243
	/********************************************************************/
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   244
	/*                      compute hasse diagram                       */
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   245
	/********************************************************************/
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   246
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   247
	public void hasseDiagram() {
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   248
		Enumeration e1,e2;
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   249
		Vertex vx1,vx2;
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   250
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   251
		/** construct adjacence matrix **/
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   252
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   253
		int vs=vertices.size();
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   254
		boolean adj[][]=new boolean[vs][vs];
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   255
		boolean adj2[][]=new boolean[vs][vs];
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   256
		int i,j,k;
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   257
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   258
		e1=getVertices();
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   259
		for (i=0;i<vs;i++) {
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   260
			vx1=(Vertex)(e1.nextElement());
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   261
			e2=vx1.getChildren();
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   262
			while (e2.hasMoreElements()) {
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   263
				vx2=(Vertex)(e2.nextElement());
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   264
				j=vertices.indexOf(vx2);
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   265
				adj[i][j]=true;
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   266
				adj2[i][j]=true;
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   267
			}
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   268
		}
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   269
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   270
		/** compute transitive closure R+ **/
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   271
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   272
		for (k=0;k<vs;k++)
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   273
			for (i=0;i<vs;i++)
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   274
				if (adj[i][k])
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   275
					for (j=0;j<vs;j++)
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   276
						adj[i][j] = adj[i][j] || adj[k][j];
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   277
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   278
		/** compute R \ (R+)^2 **/
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   279
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   280
		for (i=0;i<vs;i++)
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   281
			for (j=0;j<vs;j++)
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   282
				if (adj2[i][j]) {
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   283
					vx1=(Vertex)(vertices.elementAt(i));
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   284
					vx2=(Vertex)(vertices.elementAt(j));
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   285
					for (k=0;k<vs;k++)
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   286
						if (adj[i][k] && adj[k][j]) {
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   287
							vx1.removeChild(vx2);
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   288
							break;
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   289
						}
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   290
				}
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   291
	}
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   292
				
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   293
	/********************************************************************/
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   294
	/*                      insert dummy vertices                       */
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   295
	/********************************************************************/
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   296
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   297
	public Vector insert_dummies(Vector v) {
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   298
		Vector layers2=new Vector(10,10);
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   299
		int n_edges;
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   300
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   301
		do {
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   302
			Enumeration e1=v.elements(),e2;
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   303
			Vector next=new Vector(10,10);
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   304
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   305
			layers2.addElement(v);
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   306
			n_edges=0;
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   307
			while (e1.hasMoreElements()) {
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   308
				Vertex v1=(Vertex)(e1.nextElement());
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   309
				e2=v1.getChildren();
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   310
				while (e2.hasMoreElements()) {
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   311
					n_edges++;
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   312
					Vertex v2=(Vertex)(e2.nextElement());
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   313
					if (v2.getDegree()!=v1.getDegree()+1) {
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   314
						Vertex v3=new DummyVertex();
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   315
						v3.addChild(v2);
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   316
						v3.setDegree(v1.getDegree()+1);
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   317
						v1.removeChild(v2);
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   318
						v1.addChild(v3);
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   319
						next.addElement(v3);
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   320
						addVertex(v3);
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   321
					} else if (next.indexOf(v2)<0) next.addElement(v2);
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   322
				}
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   323
			}
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   324
			v=next;
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   325
			numEdges.addElement(new Integer(n_edges));
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   326
		} while (!v.isEmpty());
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   327
		return layers2;
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   328
	}
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   329
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   330
	/********************************************************************/
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   331
	/*                     calculation of crossings                     */
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   332
	/********************************************************************/
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   333
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   334
	public int count_crossings(Vector layers,int oldcr) {
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   335
		int i,j,y1,y2,cr=0,l;
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   336
		for (l=0;l<layers.size()-1;l++) {
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   337
			Vector v1=(Vector)(layers.elementAt(l));
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   338
			for (i=0;i<v1.size();i++) {
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   339
				Enumeration e2=((Vertex)(v1.elementAt(i))).getChildren();
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   340
				while (e2.hasMoreElements()) {
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   341
					y1=((Vector)(layers.elementAt(l+1))).indexOf(e2.nextElement());
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   342
					for (j=0;j<i;j++) {
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   343
						Enumeration e3=((Vertex)(v1.elementAt(j))).getChildren();
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   344
						while (e3.hasMoreElements()) {
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   345
							y2=((Vector)(layers.elementAt(l+1))).indexOf(e3.nextElement());
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   346
							if (y1<y2) {
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   347
								cr++;
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   348
								if (cr>=oldcr) return cr;
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   349
							}
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   350
						}
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   351
					}
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   352
				}
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   353
			}
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   354
		}
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   355
		return cr;
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   356
	}
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   357
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   358
	/********************************************************************/
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   359
	/* calculation of crossings where vertices vx1 and vx2 are involved */
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   360
	/* vx1 and vx2 must be in same layer and vx1 is left from vx2       */
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   361
	/********************************************************************/
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   362
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   363
	public int count_crossings_2(Vector layers,Vertex vx1,Vertex vx2,int oldcr) {
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   364
		int i,cr=0,l=vx1.getDegree();
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   365
		Vertex va,vb;
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   366
		Vector layer;
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   367
		Enumeration e1,e2;
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   368
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   369
		if (l>0) {
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   370
			layer=(Vector)(layers.elementAt(l-1));
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   371
			e1=vx1.getParents();
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   372
			while (e1.hasMoreElements()) {
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   373
				va=(Vertex)(e1.nextElement());
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   374
				i=layer.indexOf(va);
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   375
				e2=vx2.getParents();
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   376
				while (e2.hasMoreElements()) {
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   377
					vb=(Vertex)(e2.nextElement());
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   378
					if (layer.indexOf(vb)<i) {
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   379
						cr++;
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   380
						if (cr>=oldcr) return cr;
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   381
					}
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   382
				}
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   383
			}
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   384
		}
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   385
		if (l<layers.size()-1) {
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   386
			layer=(Vector)(layers.elementAt(l+1));
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   387
			e1=vx1.getChildren();
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   388
			while (e1.hasMoreElements()) {
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   389
				va=(Vertex)(e1.nextElement());
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   390
				i=layer.indexOf(va);
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   391
				e2=vx2.getChildren();
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   392
				while (e2.hasMoreElements()) {
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   393
					vb=(Vertex)(e2.nextElement());
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   394
					if (layer.indexOf(vb)<i) {
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   395
						cr++;
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   396
						if (cr>=oldcr) return cr;
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   397
					}
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   398
				}
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   399
			}
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   400
		}
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   401
		return cr;
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   402
	}
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   403
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   404
	/********************************************************************/
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   405
	/*       reduction of crossings by exchanging adjacent vertices     */
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   406
	/********************************************************************/
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   407
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   408
	public void exchangeVertices(Vector layers,int oldcr) {
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   409
		int i,l,c1,c2;
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   410
		Vertex vx1,vx2;
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   411
		Vector v1;
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   412
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   413
		for (l=0;l<layers.size();l++) {
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   414
			v1=(Vector)(layers.elementAt(l));
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   415
			for (i=0;i<v1.size()-1;i++) {
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   416
				vx1=(Vertex)(v1.elementAt(i));
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   417
				vx2=(Vertex)(v1.elementAt(i+1));
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   418
				c1=count_crossings_2(layers,vx1,vx2,oldcr);
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   419
				c2=count_crossings_2(layers,vx2,vx1,c1);
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   420
				if (c2<c1) {
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   421
					v1.setElementAt(vx2,i);
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   422
					v1.setElementAt(vx1,i+1);
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   423
				}
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   424
			}
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   425
		}
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   426
	}
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   427
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   428
	/********************************************************************/
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   429
	/*                    minimization of crossings                     */
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   430
	/********************************************************************/
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   431
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   432
	public Vector min_crossings(Vector layers) {
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   433
		int n,i,l,k,z=0,cr2,cr=count_crossings(layers,Integer.MAX_VALUE);
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   434
		boolean topdown=true,first=true;
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   435
		Enumeration e1,e2;
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   436
		Vector v1,v2,layers2=null,best=layers;
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   437
		Vertex vx1,vx2;
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   438
		n=0;
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   439
		while (n<3 && cr>0) {
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   440
			if (topdown) {
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   441
				/** top-down-traversal **/
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   442
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   443
				layers2=new Vector(10,10);
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   444
				for (l=0;l<layers.size();l++) {
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   445
					v1=(Vector)(layers.elementAt(l));
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   446
					if (l==0) layers2.addElement(v1.clone());
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   447
					else {
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   448
						v2=new Vector(10,10);
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   449
						layers2.addElement(v2);
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   450
						e1=v1.elements();
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   451
						while (e1.hasMoreElements()) {
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   452
							vx1=(Vertex)(e1.nextElement());
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   453
							k=0;z=0;
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   454
							e2=vx1.getParents();
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   455
							while (e2.hasMoreElements()) {
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   456
								k+=((Vector)(layers2.elementAt(l-1))).indexOf(e2.nextElement());
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   457
								z++;
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   458
							}
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   459
							if (z>0)
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   460
								vx1.setWeight(((double)(k))/z);
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   461
							else if (first)
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   462
								vx1.setWeight(Double.MAX_VALUE);
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   463
							for (i=0;i<v2.size();i++)
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   464
								if (vx1.getWeight()<((Vertex)(v2.elementAt(i))).getWeight()) break;
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   465
							if (i==v2.size()) v2.addElement(vx1);
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   466
							else v2.insertElementAt(vx1,i);
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   467
						}
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   468
					}
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   469
				}
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   470
			} else {
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   471
				/** bottom-up-traversal **/
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   472
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   473
				layers2=new Vector(10,10);
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   474
				for (l=layers.size()-1;l>=0;l--) {
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   475
					v1=(Vector)(layers.elementAt(l));
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   476
					if (l==layers.size()-1) layers2.addElement(v1.clone());
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   477
					else {
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   478
						v2=new Vector(10,10);
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   479
						layers2.insertElementAt(v2,0);
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   480
						e1=v1.elements();
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   481
						while (e1.hasMoreElements()) {
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   482
							vx1=(Vertex)(e1.nextElement());
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   483
							k=0;z=0;
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   484
							e2=vx1.getChildren();
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   485
							while (e2.hasMoreElements()) {
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   486
								k+=((Vector)(layers2.elementAt(1))).indexOf(e2.nextElement());
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   487
								z++;
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   488
							}
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   489
							if (z>0)
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   490
								vx1.setWeight(((double)(k))/z);
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   491
							else if (first)
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   492
								vx1.setWeight(Double.MAX_VALUE);
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   493
							for (i=0;i<v2.size();i++)
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   494
								if (vx1.getWeight()<((Vertex)(v2.elementAt(i))).getWeight()) break;
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   495
							if (i==v2.size()) v2.addElement(vx1);
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   496
							else v2.insertElementAt(vx1,i);
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   497
						}
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   498
					}
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   499
				}
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   500
			}
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   501
			//exchangeVertices(layers2,cr);
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   502
			topdown=!topdown;
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   503
			first=false;
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   504
			layers=layers2;
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   505
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   506
			cr2=count_crossings(layers2,cr);
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   507
			if (cr2<cr) {
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   508
				best=layers2;
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   509
				cr=cr2;					
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   510
			} else n++;
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   511
		}
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   512
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   513
		while (true) {
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   514
			exchangeVertices(best,cr);
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   515
			cr2=count_crossings(best,cr);
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   516
			if (cr2<cr)
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   517
				cr=cr2;
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   518
			else
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   519
				break;
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   520
		}
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   521
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   522
		return best;
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   523
	}
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   524
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   525
	/********************************************************************/
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   526
	/*                   set initial coordinates                        */
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   527
	/********************************************************************/
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   528
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   529
	public void init_coordinates(Vector layers) {
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   530
		int y=0;
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   531
		Enumeration e1=layers.elements();
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   532
		Enumeration e3=numEdges.elements();
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   533
		while (e1.hasMoreElements()) {
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   534
			Vector v1=(Vector)(e1.nextElement());
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   535
			Enumeration e2=v1.elements();
37738
7bf3ec9e7b0c Boxes may now have different widths.
berghofe
parents: 33686
diff changeset
   536
			int x=0;
3599
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   537
			while (e2.hasMoreElements()) {
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   538
				Vertex ve=(Vertex)(e2.nextElement());
37738
7bf3ec9e7b0c Boxes may now have different widths.
berghofe
parents: 33686
diff changeset
   539
				ve.setX(x+ve.box_width2());
3599
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   540
				ve.setY(y);
37738
7bf3ec9e7b0c Boxes may now have different widths.
berghofe
parents: 33686
diff changeset
   541
				x+=ve.box_width()+20;
3599
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   542
			}
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   543
			y+=box_height+Math.max(35,7*(((Integer)(e3.nextElement())).intValue()));
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   544
		}
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   545
	}
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   546
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   547
	/********************************************************************/
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   548
	/*                       pendulum method                            */
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   549
	/********************************************************************/
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   550
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   551
	public void pendulum(Vector layers) {
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   552
		Vector layers2=new Vector(10,10);
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   553
		Enumeration e1=layers.elements(),e2;
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   554
		int i,j,d1,d2,k,offset,dsum;
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   555
		Region r1,r2;
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   556
		boolean change;
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   557
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   558
		while (e1.hasMoreElements()) {
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   559
			e2=((Vector)(e1.nextElement())).elements();
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   560
			Vector layer=new Vector(10,10);
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   561
			layers2.addElement(layer);
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   562
			while (e2.hasMoreElements()) {
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   563
				Region r=new Region(this);
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   564
				r.addVertex((Vertex)(e2.nextElement()));
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   565
				layer.addElement(r);
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   566
			}
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   567
		}
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   568
		for (k=0;k<10;k++) {
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   569
			dsum=0;
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   570
			for (j=1;j<layers2.size();j++) {
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   571
				Vector l=(Vector)(layers2.elementAt(j));
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   572
				if (l.size()>=2) {
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   573
					do {
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   574
						change=false;
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   575
						d1=((Region)(l.firstElement())).pred_deflection();
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   576
						for (i=0;i<l.size()-1;i++) {
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   577
							r1=(Region)(l.elementAt(i));
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   578
							r2=(Region)(l.elementAt(i+1));
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   579
							d2=r2.pred_deflection();
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   580
							if (r1.touching(r2) && (d1 <= 0 && d2 < d1 ||
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   581
								d2 > 0 && d1 > d2 || d1 > 0 && d2 < 0)) {
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   582
								r1.combine(r2);
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   583
								l.removeElement(r2);
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   584
								change=true;
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   585
								d2=r1.pred_deflection();
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   586
							}
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   587
							d1=d2;
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   588
						}
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   589
					} while (change);
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   590
				}
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   591
				for (i=0;i<l.size();i++) {
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   592
					r1=(Region)(l.elementAt(i));
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   593
					d1=r1.pred_deflection();
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   594
					offset=d1;
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   595
					if (d1<0 && i>0) offset=-Math.min(
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   596
						((Region)(l.elementAt(i-1))).spaceBetween(r1),-d1);
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   597
					if (d1>=0 && i<l.size()-1) offset=Math.min(
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   598
						r1.spaceBetween((Region)(l.elementAt(i+1))),d1);
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   599
					r1.move(offset);
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   600
					dsum+=Math.abs(d1);
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   601
				}		
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   602
			}
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   603
			if (dsum==0) break;
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   604
		}
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   605
	}		
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   606
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   607
	/********************************************************************/
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   608
	/*                      rubberband method                           */
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   609
	/********************************************************************/
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   610
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   611
	public void rubberband(Vector layers) {
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   612
		Enumeration e1,e2;
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   613
		int i,n,k,d,d2;
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   614
		Vector v;
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   615
		Vertex vx;
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   616
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   617
		for (k=0;k<10;k++) {
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   618
			e1=layers.elements();
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   619
			while (e1.hasMoreElements()) {
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   620
				v=(Vector)(e1.nextElement());
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   621
				for (i=0;i<v.size();i++) {
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   622
					n=0;d=0;
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   623
					vx=(Vertex)(v.elementAt(i));
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   624
					e2=vx.getChildren();
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   625
					while (e2.hasMoreElements()) {
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   626
						d+=((Vertex)(e2.nextElement())).getX()-vx.getX();
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   627
						n++;
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   628
					}
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   629
					e2=vx.getParents();
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   630
					while (e2.hasMoreElements()) {
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   631
						d+=((Vertex)(e2.nextElement())).getX()-vx.getX();
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   632
						n++;
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   633
					}
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   634
					d2=(n!=0?d/n:0);
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   635
37738
7bf3ec9e7b0c Boxes may now have different widths.
berghofe
parents: 33686
diff changeset
   636
					if (d<0 && (i==0 || ((Vertex)(v.elementAt(i-1))).rightX()+20 < vx.leftX()+d2) ||
7bf3ec9e7b0c Boxes may now have different widths.
berghofe
parents: 33686
diff changeset
   637
						d>0 && (i==v.size()-1 || ((Vertex)(v.elementAt(i+1))).leftX()-20 > vx.rightX()+d2))
3599
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   638
						vx.setX(vx.getX()+d2);
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   639
				}
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   640
			}
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   641
		}
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   642
	}
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   643
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   644
	/**** Intersection point of two lines (auxiliary function for calcSplines)   ****/
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   645
	/**** Calculate intersection point of line which is parallel to line (p1,p2) ****/
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   646
	/**** and leads through p5, with line (p3,p4)                                ****/
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   647
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   648
	Point intersect(Point p1,Point p2,Point p3,Point p4,Point p5) {
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   649
		float x=0,y=0,s1=0,s2=0;
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   650
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   651
		if (p1.x!=p2.x)
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   652
			s1=((float)(p2.y-p1.y))/(p2.x-p1.x);
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   653
		if (p3.x!=p4.x)
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   654
			s2=((float)(p4.y-p3.y))/(p4.x-p3.x);
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   655
		if (p1.x==p2.x) {
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   656
			x=p5.x;
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   657
			y=s2*(p5.x-p3.x)+p3.y;
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   658
		} else if (p3.x==p4.x) {
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   659
			x=p3.x;
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   660
			y=s1*(p3.x-p5.x)+p5.y;
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   661
		} else {
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   662
			x=(p5.x*s1-p3.x*s2+p3.y-p5.y)/(s1-s2);
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   663
			y=s2*(x-p3.x)+p3.y;
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   664
		}
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   665
		return new Point(Math.round(x),Math.round(y));
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   666
	}
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   667
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   668
	/**** Calculate control points (auxiliary function for calcSplines) ****/
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   669
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   670
	Points calcPoint(Point p1,Point p2,Point p3,int lboxx,int rboxx,int boxy) {
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   671
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   672
		/*** Points p1 , p2 , p3 define a triangle which encloses the spline.  ***/
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   673
		/*** Check if adjacent boxes (specified by lboxx,rboxx and boxy)       ***/
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   674
		/*** collide with the spline. In this case p1 and p3 are shifted by an ***/
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   675
		/*** appropriate offset before they are returned                       ***/
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   676
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   677
		int xh1,xh2,bx=0,by=0;
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   678
		boolean pt1 = boxy >= p1.y && boxy <= p3.y || boxy >= p3.y && boxy <= p1.y;
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   679
		boolean pt2 = boxy+box_height >= p1.y && boxy+box_height <= p3.y ||
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   680
                              boxy+box_height >= p3.y && boxy+box_height <= p1.y;
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   681
		boolean move = false;
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   682
		Point b;
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   683
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   684
		xh1 = p1.x+(boxy-p1.y)*(p3.x-p1.x)/(p3.y-p1.y);
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   685
		xh2 = p1.x+(boxy+box_height-p1.y)*(p3.x-p1.x)/(p3.y-p1.y);
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   686
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   687
		if (xh1 <= lboxx && pt1 && xh2 <= lboxx && pt2) {
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   688
			move = true;
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   689
			bx = lboxx;
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   690
			by = boxy + (xh1 < xh2 ? 0 : box_height ) ;
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   691
		} else if (xh1 >= rboxx && pt1 && xh2 >= rboxx && pt2) {
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   692
			move = true;
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   693
			bx = rboxx;
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   694
			by = boxy + (xh1 > xh2 ? 0 : box_height ) ;
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   695
		} else if ( (xh1 <= lboxx || xh1 >= rboxx) && pt1) {
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   696
			move = true;
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   697
			bx = (xh1 <= lboxx ? lboxx : rboxx ) ;
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   698
			by = boxy;
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   699
		} else if ( (xh2 <= lboxx || xh2 >= rboxx) && pt2) {
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   700
			move = true;
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   701
			bx = (xh2 <= lboxx ? lboxx : rboxx ) ;
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   702
			by = boxy+box_height;
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   703
		}
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   704
		b=new Point(bx,by);
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   705
		if (move) return new Points(intersect(p1,p3,p1,p2,b),intersect(p1,p3,p2,p3,b));
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   706
		else return new Points(p1,p3);
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   707
	}
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   708
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   709
	/********************************************************************/
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   710
	/*                        calculate splines                         */
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   711
	/********************************************************************/
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   712
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   713
	public void calcSplines(Vector layers) {
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   714
		Enumeration e2,e1=vertices.elements();
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   715
		Vertex vx1,vx2,vx3;
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   716
		Vector pos,layer;
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   717
		int x1,y1,x2,y2,x3,y3,xh,k,leftx,rightx,spc;
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   718
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   719
		while (e1.hasMoreElements()) {
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   720
			vx1=(Vertex)(e1.nextElement());
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   721
			if (!vx1.isDummy()) {
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   722
				e2=vx1.getChildren();
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   723
				while (e2.hasMoreElements()) {
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   724
					vx2=(Vertex)(e2.nextElement());
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   725
					if (vx2.isDummy()) {
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   726
						vx3=vx2;
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   727
						/**** convert edge to spline ****/
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   728
						pos=new Vector(10,10);
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   729
						x1=vx1.getX();
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   730
						y1=vx1.getY()+box_height;
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   731
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   732
						do {
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   733
							/*** calculate position of control points ***/
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   734
							x2=vx2.getX();
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   735
							y2=vx2.getY();
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   736
							layer=(Vector)(layers.elementAt(vx2.getDegree()));
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   737
							k=layer.indexOf(vx2);
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   738
							vx2=(Vertex)((vx2.getChildren()).nextElement());
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   739
							x3=vx2.getX();
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   740
							y3=vx2.getY();
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   741
							spc=0;
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   742
							leftx = k==0 /* || ((Vertex)(layer.elementAt(k-1))).isDummy() */ ?
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   743
								Integer.MIN_VALUE:
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   744
								((Vertex)(layer.elementAt(k-1))).rightX()+spc;
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   745
							rightx = k==layer.size()-1 /* || ((Vertex)(layer.elementAt(k+1))).isDummy() */ ?
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   746
								Integer.MAX_VALUE:
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   747
								((Vertex)(layer.elementAt(k+1))).leftX()-spc;
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   748
							xh=x2+box_height*(x3-x2)/(y3-y2);
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   749
							if (!(x2<=x3 && xh>=rightx || x2>x3 && xh<=leftx)) {
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   750
								/* top control point */
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   751
								pos.addElement(new Integer(1));
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   752
								y1=y2;
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   753
							} else {
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   754
								xh=x1+(y2-y1)*(x2-x1)/(y2+box_height-y1);
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   755
								if (!(x2<=x1 && xh>=rightx || x2>x1 && xh<=leftx))
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   756
									/* bottom control point */
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   757
									pos.addElement(new Integer(2));
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   758
								else
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   759
									/* two control points needed */
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   760
									pos.addElement(new Integer(3));
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   761
								y1=y2+box_height;
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   762
							}
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   763
							x1=x2;
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   764
						} while (vx2.isDummy());
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   765
						pos.addElement(new Integer(1));
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   766
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   767
						/**** calculate triangles ****/
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   768
						vx2=vx3;
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   769
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   770
						int pos1,pos2,i=0;
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   771
						Vector pts=new Vector(10,10);
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   772
						int lboxx,rboxx,boxy;
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   773
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   774
						x1=vx1.getX();
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   775
						y1=vx1.getY()+box_height;
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   776
						pts.addElement(new Point(x1,y1)); /** edge starting point **/
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   777
						do {
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   778
							x2=vx2.getX();
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   779
							y2=vx2.getY();
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   780
							pos1=((Integer)(pos.elementAt(i))).intValue();
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   781
							pos2=((Integer)(pos.elementAt(i+1))).intValue();
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   782
							i++;
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   783
							layer=(Vector)(layers.elementAt(vx2.getDegree()));
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   784
							k=layer.indexOf(vx2);
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   785
							boxy=vx2.getY();
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   786
							vx2=(Vertex)((vx2.getChildren()).nextElement());
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   787
							x3=vx2.getX();
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   788
							y3=vx2.getY();
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   789
							if (pos1==2) y2+=box_height;
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   790
							if (pos2==2) y3+=box_height;
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   791
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   792
							lboxx = (k==0 /* || ((Vertex)(layer.elementAt(k-1))).isDummy() */ ) ?
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   793
								Integer.MIN_VALUE :
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   794
								((Vertex)(layer.elementAt(k-1))).rightX();
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   795
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   796
							rboxx = (k==layer.size()-1 /* || ((Vertex)(layer.elementAt(k+1))).isDummy() */ ) ?
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   797
								Integer.MAX_VALUE :
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   798
								((Vertex)(layer.elementAt(k+1))).leftX();
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   799
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   800
							Point p1,p2,p3;
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   801
							Points ps;
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   802
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   803
							p1 = new Point((x1+x2)/2,(y1+y2)/2);
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   804
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   805
							if (pos1<=2) {
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   806
								/** one control point **/
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   807
								p2 = new Point(x2,y2);
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   808
								ps = calcPoint(p1,p2,new Point((x2+x3)/2,(y2+y3)/2),lboxx,rboxx,boxy);
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   809
								pts.addElement(ps.p);
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   810
								pts.addElement(p2);
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   811
								pts.addElement(ps.q);
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   812
							} else {
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   813
								/** two control points **/
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   814
								p2 = new Point(x2,y2-box_height);
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   815
								p3 = new Point(x2,y2+box_height2);
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   816
								ps = calcPoint(p1,p2,p3,lboxx,rboxx,boxy);
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   817
								pts.addElement(ps.p);
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   818
								pts.addElement(p2);
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   819
								pts.addElement(ps.q);
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   820
								p2 = new Point(x2,y2+box_height*2);
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   821
								ps = calcPoint(p3,p2,new Point((p2.x+x3)/2,(p2.y+y3)/2),
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   822
								               lboxx,rboxx,boxy);
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   823
								pts.addElement(ps.p);
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   824
								pts.addElement(p2);
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   825
								pts.addElement(ps.q);
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   826
							}
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   827
							x1=p2.x;
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   828
							y1=p2.y;
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   829
						} while (vx2.isDummy());
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   830
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   831
						pts.addElement(new Point(vx2.getX(),vx2.getY())); /** edge end point **/
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   832
						splines.addElement(new Spline(pts));
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   833
					}
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   834
				}
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   835
			}
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   836
		}
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   837
	}
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   838
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   839
	/********************************************************************/
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   840
	/*                      calculate bounding box                      */
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   841
	/********************************************************************/
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   842
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   843
	public void calcBoundingBox() {
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   844
		min_y=min_x=Integer.MAX_VALUE;
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   845
		max_y=max_x=Integer.MIN_VALUE;
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   846
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   847
		Enumeration e1=vertices.elements();
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   848
		Vertex v;
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   849
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   850
		while (e1.hasMoreElements()) {
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   851
			v=(Vertex)(e1.nextElement());
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   852
			min_x=Math.min(min_x,v.leftX());
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   853
			max_x=Math.max(max_x,v.rightX());
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   854
			min_y=Math.min(min_y,v.getY());
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   855
			max_y=Math.max(max_y,v.getY()+box_height);
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   856
		}
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   857
		min_x-=20;
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   858
		min_y-=20;
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   859
		max_x+=20;
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   860
		max_y+=20;
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   861
	}
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   862
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   863
	/********************************************************************/
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   864
	/*                           draw graph                             */
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   865
	/********************************************************************/
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   866
					 
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   867
	public void draw(Graphics g) {
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   868
		if (box_height==0) layout(g);
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   869
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   870
		g.translate(-min_x,-min_y);
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   871
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   872
		Enumeration e1=vertices.elements();
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   873
		while (e1.hasMoreElements())
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   874
			((Vertex)(e1.nextElement())).draw(g);
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   875
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   876
		e1=splines.elements();
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   877
		while (e1.hasMoreElements())
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   878
			((Spline)(e1.nextElement())).draw(g);
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   879
	}
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   880
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   881
	/********************************************************************/
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   882
	/*               return vertex at position (x,y)                    */
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   883
	/********************************************************************/
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   884
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   885
	public Vertex vertexAt(int x,int y) {
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   886
		Enumeration e1=vertices.elements();
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   887
		while (e1.hasMoreElements()) {
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   888
			Vertex v=(Vertex)(e1.nextElement());
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   889
			if (v.contains(x,y)) return v;
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   890
		}
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   891
		return null;
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   892
	}
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   893
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   894
	/********************************************************************/
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   895
	/*       encode list of vertices (as array of vertice numbers)      */
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   896
	/********************************************************************/
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   897
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   898
	public Vector encode(Vector v) {
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   899
		Vector code=new Vector(10,10);
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   900
		Enumeration e1=v.elements();
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   901
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   902
		while (e1.hasMoreElements()) {
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   903
			Vertex vx=(Vertex)(e1.nextElement());
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   904
			if (vx.getNumber()>=0)
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   905
				code.addElement(new Integer(vx.getNumber()));
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   906
		}
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   907
		return code;
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   908
	}
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   909
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   910
	/********************************************************************/
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   911
	/*                      get vertex with number n                    */
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   912
	/********************************************************************/
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   913
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   914
	public Vertex getVertexByNum(int x) {
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   915
		Enumeration e1=vertices.elements();
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   916
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   917
		while (e1.hasMoreElements()) {
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   918
			Vertex vx=(Vertex)(e1.nextElement());
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   919
			if (vx.getNumber()==x) return vx;
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   920
		}
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   921
		return null;
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   922
	}
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   923
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   924
	/********************************************************************/
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   925
	/*                      decode list of vertices                     */
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   926
	/********************************************************************/
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   927
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   928
	public Vector decode(Vector code) {
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   929
		Enumeration e1=code.elements();
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   930
		Vector vec=new Vector(10,10);
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   931
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   932
		while (e1.hasMoreElements()) {
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   933
			int i=((Integer)(e1.nextElement())).intValue();
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   934
			//Vertex vx=getVertexByNum(i);
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   935
			//if (vx!=null) vec.addElement(vx);
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   936
			vec.addElement(vertices2[i]);
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   937
		}
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   938
		return vec;
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   939
	}
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   940
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   941
	/********************************************************************/
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   942
	/*                       collapse vertices                          */
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   943
	/********************************************************************/
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   944
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   945
	public void collapse(Vector vs,String name,Vector inflate) {
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   946
		Enumeration e1,e2,e3;
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   947
		boolean nonempty=false;
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   948
		Vertex vx3,vx2,vx1;
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   949
		
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   950
		e1=vertices.elements();
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   951
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   952
		vx1=new NormalVertex(name);
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   953
		vx1.setInflate(inflate);
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   954
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   955
		while (e1.hasMoreElements()) {
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   956
			vx2=(Vertex)(e1.nextElement());
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   957
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   958
			if (vs.indexOf(vx2)<0) {
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   959
				e2=vx2.getParents();
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   960
				while (e2.hasMoreElements()) {
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   961
					vx3=(Vertex)(e2.nextElement());
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   962
					if (vs.indexOf(vx3)>=0) {
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   963
						if (!vx1.isChild(vx2))
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   964
							vx1.addChild(vx2);
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   965
						vx3.removeChild(vx2);
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   966
					}
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   967
				}
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   968
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   969
				e2=vx2.getChildren();
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   970
				while (e2.hasMoreElements()) {
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   971
					vx3=(Vertex)(e2.nextElement());
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   972
					if (vs.indexOf(vx3)>=0) {
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   973
						if (!vx2.isChild(vx1))
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   974
							vx2.addChild(vx1);
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   975
						vx2.removeChild(vx3);
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   976
					}
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   977
				}
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   978
			} else { nonempty=true; }
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   979
		}
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   980
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   981
		e1=vs.elements();
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   982
		while (e1.hasMoreElements())
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   983
			try {
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   984
				removeVertex((Vertex)(e1.nextElement()));
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   985
			} catch (NoSuchElementException exn) {}
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   986
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   987
		if (nonempty) addVertex(vx1);
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   988
	}
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   989
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   990
	/********************************************************************/
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   991
	/*                      PostScript output                           */
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   992
	/********************************************************************/
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   993
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   994
	public void PS(String fname,boolean printable) throws IOException {
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   995
		FileOutputStream f = new FileOutputStream(fname);
6541
d3ac35b2bfbf Updated to JDK 1.1.x
berghofe
parents: 3599
diff changeset
   996
		PrintWriter p = new PrintWriter(f, true);
3599
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   997
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   998
		if (printable)
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   999
			p.println("%!PS-Adobe-2.0\n\n%%BeginProlog");
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
  1000
		else {
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
  1001
			p.println("%!PS-Adobe-2.0 EPSF-2.0\n%%Orientation: Portrait");
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
  1002
			p.println("%%BoundingBox: "+min_x+" "+min_y+" "+max_x+" "+max_y);
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
  1003
			p.println("%%EndComments\n\n%%BeginProlog");
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
  1004
		}
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
  1005
		p.println("/m { moveto } def /l { lineto } def /n { newpath } def");
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
  1006
		p.println("/s { stroke } def /c { curveto } def");
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
  1007
		p.println("/b { n 0 0 m dup true charpath pathbbox 1 index 4 index sub");
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
  1008
		p.println("7 index exch sub 2 div 9 index add 1 index 4 index sub 7 index exch sub");
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
  1009
		p.println("2 div 9 index add 2 index add m pop pop pop pop");
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
  1010
		p.println("1 -1 scale show 1 -1 scale n 3 index 3 index m 1 index 0 rlineto");
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
  1011
		p.println("0 exch rlineto neg 0 rlineto closepath s pop pop } def");
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
  1012
		p.println("%%EndProlog\n");
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
  1013
		if (printable) {
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
  1014
			int hsize=max_x-min_x;
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
  1015
			int vsize=max_y-min_y;
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
  1016
			if (hsize>vsize) {
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
  1017
				// Landscape output
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
  1018
				double scale=Math.min(1,Math.min(750.0/hsize,500.0/vsize));
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
  1019
				double trans_x=50+max_y*scale+(500-scale*vsize)/2.0;
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
  1020
				double trans_y=50+max_x*scale+(750-scale*hsize)/2.0;
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
  1021
				p.println(trans_x+" "+trans_y+" translate");
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
  1022
				p.println("-90 rotate");
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
  1023
				p.println(scale+" "+(-scale)+" scale");
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
  1024
			} else {
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
  1025
				// Portrait output
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
  1026
				double scale=Math.min(1,Math.min(500.0/hsize,750.0/vsize));
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
  1027
				double trans_x=50-min_x*scale+(500-scale*hsize)/2.0;
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
  1028
				double trans_y=50+max_y*scale+(750-scale*vsize)/2.0;
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
  1029
				p.println(trans_x+" "+trans_y+" translate");
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
  1030
				p.println(scale+" "+(-scale)+" scale");
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
  1031
			}
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
  1032
		} else
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
  1033
			p.println("0 "+(max_y+min_y)+" translate\n1 -1 scale");
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
  1034
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
  1035
		p.println("/Helvetica findfont 12 scalefont setfont");
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
  1036
		p.println("0.5 setlinewidth");
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
  1037
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
  1038
		Enumeration e1=vertices.elements();
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
  1039
		while (e1.hasMoreElements())
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
  1040
			((Vertex)(e1.nextElement())).PS(p);
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
  1041
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
  1042
		e1=splines.elements();
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
  1043
		while (e1.hasMoreElements())
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
  1044
			((Spline)(e1.nextElement())).PS(p);
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
  1045
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
  1046
		if (printable) p.println("showpage");
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
  1047
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
  1048
		f.close();
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
  1049
	}
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
  1050
}
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
  1051
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
  1052
/**** Return value of function calcPoint ****/
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
  1053
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
  1054
class Points {
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
  1055
	public Point p,q;
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
  1056
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
  1057
	public Points(Point p1,Point p2) {
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
  1058
		p=p1;q=p2;
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
  1059
	}
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
  1060
}
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
  1061