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