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