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