lib/browser/GraphBrowser/Graph.java
author blanchet
Wed, 04 Aug 2010 23:27:27 +0200
changeset 38195 a8cef06e0480
parent 37738 7bf3ec9e7b0c
child 50473 ca4088bf8365
permissions -rw-r--r--
Cycle breaking in the bounds takes care of singly recursive datatypes, so we don't need to do it again; the effect of removing the constraint varies on problem to problem, but it tends to be overwhelmingly negative in conjuction with the new datatype sym breaking stuff at high cardinalities
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
3599
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
     1
/***************************************************************************
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
     2
  Title:      GraphBrowser/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