Source files for Isabelle theory graph browser.
authorberghofe
Wed Aug 06 00:06:47 1997 +0200 (1997-08-06)
changeset 359989cbba12863d
parent 3598 28b6670e415a
child 3600 5366dde08dba
Source files for Isabelle theory graph browser.
Initial revision.
lib/browser/GraphBrowser/DummyVertex.java
lib/browser/GraphBrowser/Graph.java
lib/browser/GraphBrowser/GraphBrowser.java
lib/browser/GraphBrowser/GraphBrowserFrame.java
lib/browser/GraphBrowser/GraphView.java
lib/browser/GraphBrowser/NormalVertex.java
lib/browser/GraphBrowser/Region.java
lib/browser/GraphBrowser/Spline.java
lib/browser/GraphBrowser/TreeBrowser.java
lib/browser/GraphBrowser/TreeNode.java
lib/browser/GraphBrowser/Vertex.java
lib/browser/awtUtilities/Border.java
lib/browser/awtUtilities/MessageDialog.java
lib/browser/awtUtilities/ScrollCanvas.java
lib/browser/awtUtilities/TextFrame.java
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/lib/browser/GraphBrowser/DummyVertex.java	Wed Aug 06 00:06:47 1997 +0200
     1.3 @@ -0,0 +1,31 @@
     1.4 +/***************************************************************************
     1.5 +  Title:      GraphBrowser/DummyVertex.java
     1.6 +  ID:         $Id$
     1.7 +  Author:     Stefan Berghofer, TU Muenchen
     1.8 +  Copyright   1997  TU Muenchen
     1.9 +
    1.10 +  This class represents a dummy vertex, which is used to simplify the
    1.11 +  layout algorithm.
    1.12 +***************************************************************************/
    1.13 +
    1.14 +package GraphBrowser;
    1.15 +
    1.16 +import java.util.*;
    1.17 +import java.awt.*;
    1.18 +
    1.19 +class DummyVertex extends Vertex {
    1.20 +	public boolean isDummy() {return true;}
    1.21 +
    1.22 +	public Object clone() {
    1.23 +		Vertex ve=new DummyVertex();
    1.24 +		ve.setX(getX());ve.setY(getY());
    1.25 +		return ve;
    1.26 +	}
    1.27 +
    1.28 +	public int leftX() { return getX(); }
    1.29 +
    1.30 +	public int rightX() { return getX(); }
    1.31 +
    1.32 +	public void draw(Graphics g) {}
    1.33 +}
    1.34 +
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/lib/browser/GraphBrowser/Graph.java	Wed Aug 06 00:06:47 1997 +0200
     2.3 @@ -0,0 +1,1074 @@
     2.4 +/***************************************************************************
     2.5 +  Title:      GraphBrowser/Graph.java
     2.6 +  ID:         $Id$
     2.7 +  Author:     Stefan Berghofer, TU Muenchen
     2.8 +  Copyright   1997  TU Muenchen
     2.9 +
    2.10 +  This class contains the core of the layout algorithm and methods for
    2.11 +  drawing and PostScript output.
    2.12 +***************************************************************************/
    2.13 +
    2.14 +package GraphBrowser;
    2.15 +
    2.16 +import java.util.*;
    2.17 +import java.awt.*;
    2.18 +import java.io.*;
    2.19 +
    2.20 +class ParseError extends Exception {
    2.21 +	public ParseError(String s) { super(s); }
    2.22 +}
    2.23 +
    2.24 +public class Graph {
    2.25 +	/**** parameters for layout ****/
    2.26 +
    2.27 +	public int box_height=0;
    2.28 +	public int box_height2;
    2.29 +	public int box_width;
    2.30 +	public int box_width2;
    2.31 +	public int box_hspace;
    2.32 +
    2.33 +	Vector vertices=new Vector(10,10);
    2.34 +	Vector splines=new Vector(10,10);
    2.35 +	Vector numEdges=new Vector(10,10);
    2.36 +	Vertex []vertices2;
    2.37 +
    2.38 +	public int min_x=0,min_y=0,max_x=10,max_y=10;
    2.39 +
    2.40 +	/********************************************************************/
    2.41 +	/*                         clone graph object                       */
    2.42 +	/********************************************************************/
    2.43 +
    2.44 +	public Object clone() {
    2.45 +		Graph gr=new Graph();
    2.46 +		Enumeration e1;
    2.47 +		int i;
    2.48 +
    2.49 +		gr.splines=(Vector)(splines.clone());
    2.50 +
    2.51 +		e1=vertices.elements();
    2.52 +		while (e1.hasMoreElements())
    2.53 +			gr.addVertex((Vertex)(((Vertex)(e1.nextElement())).clone()));
    2.54 +
    2.55 +		for (i=0;i<vertices.size();i++) {
    2.56 +			Vertex vx1=(Vertex)(gr.vertices.elementAt(i));
    2.57 +			e1=((Vertex)(vertices.elementAt(i))).getChildren();
    2.58 +			while (e1.hasMoreElements()) {
    2.59 +				Vertex vx2=(Vertex)(gr.vertices.elementAt(vertices.indexOf(e1.nextElement())));
    2.60 +				vx1.addChild(vx2);
    2.61 +			}
    2.62 +		}
    2.63 +
    2.64 +		gr.vertices2 = new Vertex[vertices.size()];
    2.65 +		gr.vertices.copyInto(gr.vertices2);
    2.66 +
    2.67 +		gr.min_x=min_x;gr.max_x=max_x;
    2.68 +		gr.min_y=min_y;gr.max_y=max_y;
    2.69 +
    2.70 +		return gr;
    2.71 +	}
    2.72 +
    2.73 +	Graph() {}
    2.74 +
    2.75 +	/********************************************************************/
    2.76 +	/*                      Read graph from stream                      */
    2.77 +	/********************************************************************/
    2.78 +
    2.79 +	public Graph(InputStream s,TreeNode tn) throws IOException, ParseError {
    2.80 +		StreamTokenizer tok=new StreamTokenizer(s);
    2.81 +		String name,dir,vertexID;
    2.82 +		Vertex ve1,ve2;
    2.83 +		boolean children,unfoldDir;
    2.84 +		int index=0;
    2.85 +
    2.86 +		tok.nextToken();
    2.87 +		while (tok.ttype!=StreamTokenizer.TT_EOF) {
    2.88 +			if (tok.ttype!=StreamTokenizer.TT_WORD && tok.ttype!='"')
    2.89 +				throw new ParseError("expected: vertex name\nfound   : "+tok.toString());
    2.90 +			name=tok.sval;
    2.91 +                        tok.nextToken();
    2.92 +			if (tok.ttype!=StreamTokenizer.TT_WORD && tok.ttype!='"')
    2.93 +				throw new ParseError("expected: vertex identifier\nfound   : "+tok.toString());
    2.94 +			vertexID=tok.sval;
    2.95 +			tok.nextToken();
    2.96 +			if (tok.ttype!=StreamTokenizer.TT_WORD && tok.ttype!='"')
    2.97 +				throw new ParseError("expected: directory name\nfound   : "+tok.toString());
    2.98 +			dir=tok.sval;
    2.99 +			tok.nextToken();
   2.100 +			if (tok.ttype=='+') {
   2.101 +				unfoldDir=true;
   2.102 +				tok.nextToken();
   2.103 +			} else
   2.104 +				unfoldDir=false;
   2.105 +			if (tok.ttype!=StreamTokenizer.TT_WORD && tok.ttype!='"')
   2.106 +				throw new ParseError("expected: path name\nfound   : "+tok.toString());
   2.107 +			ve1=findVertex(vertexID);
   2.108 +			if (ve1==null) {
   2.109 +				ve1=new NormalVertex("");
   2.110 +				ve1.setID(vertexID);
   2.111 +				ve1.setNumber(index++);
   2.112 +				addVertex(ve1);
   2.113 +			}
   2.114 +			ve1.setPath(tok.sval);
   2.115 +			ve1.setDir(dir);
   2.116 +                        ve1.setLabel(name);
   2.117 +			tn.insertNode(name,dir,tok.sval,ve1.getNumber(),unfoldDir);
   2.118 +			tok.nextToken();
   2.119 +			if (tok.ttype=='<') {
   2.120 +				children=true;
   2.121 +				tok.nextToken();
   2.122 +			} else if (tok.ttype=='>') {
   2.123 +					children=false;
   2.124 +					tok.nextToken();
   2.125 +			} else children=true;
   2.126 +			while (tok.ttype!=';') {
   2.127 +				if (tok.ttype!=StreamTokenizer.TT_WORD && tok.ttype!='"')
   2.128 +					throw new ParseError("expected: child vertex identifier or ';'\nfound   : "+tok.toString());				
   2.129 +				ve2=findVertex(tok.sval);
   2.130 +				if (ve2==null) {
   2.131 +					ve2=new NormalVertex("");
   2.132 +					ve2.setID(tok.sval);
   2.133 +					ve2.setNumber(index++);
   2.134 +					addVertex(ve2);
   2.135 +				}
   2.136 +				if (children)
   2.137 +					ve1.addChild(ve2);
   2.138 +				else
   2.139 +					ve1.addParent(ve2);
   2.140 +				tok.nextToken();
   2.141 +			}
   2.142 +			tok.nextToken();
   2.143 +		}
   2.144 +		vertices2 = new Vertex[vertices.size()];
   2.145 +		vertices.copyInto(vertices2);
   2.146 +	}
   2.147 +	
   2.148 +	/*** Find vertex with identifier vertexID ***/
   2.149 +
   2.150 +	public Vertex findVertex(String vertexID) {
   2.151 +		Enumeration e1=vertices.elements();
   2.152 +		Vertex v1;
   2.153 +
   2.154 +		while (e1.hasMoreElements()) {
   2.155 +			v1=(Vertex)(e1.nextElement());
   2.156 +			if ((v1.getID()).equals(vertexID))
   2.157 +				return v1;
   2.158 +		}
   2.159 +		return null;
   2.160 +	}
   2.161 +		 
   2.162 +	public void addVertex(Vertex v) {
   2.163 +		vertices.addElement(v);
   2.164 +		v.setGraph(this);
   2.165 +	}
   2.166 +
   2.167 +	public void removeVertex(Vertex v) {
   2.168 +		vertices.removeElement(v);
   2.169 +	}
   2.170 +
   2.171 +	public Enumeration getVertices() {
   2.172 +		return vertices.elements();
   2.173 +	}
   2.174 +
   2.175 +	/********************************************************************/
   2.176 +	/*                          graph layout                            */
   2.177 +	/********************************************************************/
   2.178 +
   2.179 +	public void layout(Graphics g) {
   2.180 +		splines.removeAllElements();
   2.181 +		hasseDiagram();
   2.182 +		Vector layers=min_crossings(insert_dummies((Vector)(sort().elementAt(0))));
   2.183 +		setParameters(g);
   2.184 +		init_coordinates(layers);
   2.185 +		pendulum(layers);
   2.186 +		rubberband(layers);
   2.187 +		calcSplines(layers);
   2.188 +		calcBoundingBox();
   2.189 +	}
   2.190 +
   2.191 +	/********************************************************************/
   2.192 +	/*                      set layout parameters                       */
   2.193 +	/********************************************************************/
   2.194 +
   2.195 +	public void setParameters(Graphics g) {
   2.196 +		Enumeration e1=vertices.elements();
   2.197 +		int h,w;
   2.198 +		h=w=Integer.MIN_VALUE;
   2.199 +
   2.200 +		while (e1.hasMoreElements()) {
   2.201 +			Dimension dim=((Vertex)(e1.nextElement())).getLabelSize(g);
   2.202 +			h=Math.max(h,dim.height);
   2.203 +			w=Math.max(w,dim.width);
   2.204 +		}
   2.205 +		box_height=h+4;
   2.206 +		box_height2=box_height/2;
   2.207 +		box_width=w+8;
   2.208 +		box_width2=box_width/2;
   2.209 +		box_hspace=box_width+20;
   2.210 +	}
   2.211 +
   2.212 +	/********************************************************************/
   2.213 +	/*                       topological sorting                        */
   2.214 +	/********************************************************************/
   2.215 +
   2.216 +	public Vector sort() {
   2.217 +		Vector todo=(Vector)(vertices.clone());
   2.218 +		Vector layers=new Vector(10,10);
   2.219 +		Vector todo2;
   2.220 +		Enumeration e1,e2;
   2.221 +		Vertex v,v2;
   2.222 +
   2.223 +		e1=vertices.elements();
   2.224 +		while (e1.hasMoreElements())
   2.225 +			((Vertex)(e1.nextElement())).setDegree(0);
   2.226 +
   2.227 +		e1=vertices.elements();
   2.228 +		while (e1.hasMoreElements()) {
   2.229 +			v=(Vertex)(e1.nextElement());
   2.230 +			e2=v.getChildren();
   2.231 +			while (e2.hasMoreElements()) {
   2.232 +				v2=(Vertex)(e2.nextElement());
   2.233 +				todo.removeElement(v2);
   2.234 +				v2.setDegree(1+v2.getDegree());
   2.235 +			}
   2.236 +		}
   2.237 +		while (!todo.isEmpty()) {
   2.238 +			layers.addElement(todo);
   2.239 +			todo2=new Vector(10,10);
   2.240 +			e1=todo.elements();
   2.241 +			while (e1.hasMoreElements()) {
   2.242 +				e2=((Vertex)(e1.nextElement())).getChildren();
   2.243 +				while (e2.hasMoreElements()) {
   2.244 +					v=(Vertex)(e2.nextElement());
   2.245 +					v.setDegree(v.getDegree()-1);
   2.246 +					if (v.getDegree()==0) {
   2.247 +						todo2.addElement(v);
   2.248 +						v.setDegree(layers.size());
   2.249 +					}
   2.250 +				}
   2.251 +			}
   2.252 +			todo=todo2;
   2.253 +		}
   2.254 +		return layers;
   2.255 +	}
   2.256 +
   2.257 +	/********************************************************************/
   2.258 +	/*                      compute hasse diagram                       */
   2.259 +	/********************************************************************/
   2.260 +
   2.261 +	public void hasseDiagram() {
   2.262 +		Enumeration e1,e2;
   2.263 +		Vertex vx1,vx2;
   2.264 +
   2.265 +		/** construct adjacence matrix **/
   2.266 +
   2.267 +		int vs=vertices.size();
   2.268 +		boolean adj[][]=new boolean[vs][vs];
   2.269 +		boolean adj2[][]=new boolean[vs][vs];
   2.270 +		int i,j,k;
   2.271 +
   2.272 +		e1=getVertices();
   2.273 +		for (i=0;i<vs;i++) {
   2.274 +			vx1=(Vertex)(e1.nextElement());
   2.275 +			e2=vx1.getChildren();
   2.276 +			while (e2.hasMoreElements()) {
   2.277 +				vx2=(Vertex)(e2.nextElement());
   2.278 +				j=vertices.indexOf(vx2);
   2.279 +				adj[i][j]=true;
   2.280 +				adj2[i][j]=true;
   2.281 +			}
   2.282 +		}
   2.283 +
   2.284 +		/** compute transitive closure R+ **/
   2.285 +
   2.286 +		for (k=0;k<vs;k++)
   2.287 +			for (i=0;i<vs;i++)
   2.288 +				if (adj[i][k])
   2.289 +					for (j=0;j<vs;j++)
   2.290 +						adj[i][j] = adj[i][j] || adj[k][j];
   2.291 +
   2.292 +		/** compute R \ (R+)^2 **/
   2.293 +
   2.294 +		for (i=0;i<vs;i++)
   2.295 +			for (j=0;j<vs;j++)
   2.296 +				if (adj2[i][j]) {
   2.297 +					vx1=(Vertex)(vertices.elementAt(i));
   2.298 +					vx2=(Vertex)(vertices.elementAt(j));
   2.299 +					for (k=0;k<vs;k++)
   2.300 +						if (adj[i][k] && adj[k][j]) {
   2.301 +							vx1.removeChild(vx2);
   2.302 +							break;
   2.303 +						}
   2.304 +				}
   2.305 +	}
   2.306 +				
   2.307 +	/********************************************************************/
   2.308 +	/*                      insert dummy vertices                       */
   2.309 +	/********************************************************************/
   2.310 +
   2.311 +	public Vector insert_dummies(Vector v) {
   2.312 +		Vector layers2=new Vector(10,10);
   2.313 +		int n_edges;
   2.314 +
   2.315 +		do {
   2.316 +			Enumeration e1=v.elements(),e2;
   2.317 +			Vector next=new Vector(10,10);
   2.318 +
   2.319 +			layers2.addElement(v);
   2.320 +			n_edges=0;
   2.321 +			while (e1.hasMoreElements()) {
   2.322 +				Vertex v1=(Vertex)(e1.nextElement());
   2.323 +				e2=v1.getChildren();
   2.324 +				while (e2.hasMoreElements()) {
   2.325 +					n_edges++;
   2.326 +					Vertex v2=(Vertex)(e2.nextElement());
   2.327 +					if (v2.getDegree()!=v1.getDegree()+1) {
   2.328 +						Vertex v3=new DummyVertex();
   2.329 +						v3.addChild(v2);
   2.330 +						v3.setDegree(v1.getDegree()+1);
   2.331 +						v1.removeChild(v2);
   2.332 +						v1.addChild(v3);
   2.333 +						next.addElement(v3);
   2.334 +						addVertex(v3);
   2.335 +					} else if (next.indexOf(v2)<0) next.addElement(v2);
   2.336 +				}
   2.337 +			}
   2.338 +			v=next;
   2.339 +			numEdges.addElement(new Integer(n_edges));
   2.340 +		} while (!v.isEmpty());
   2.341 +		return layers2;
   2.342 +	}
   2.343 +
   2.344 +	/********************************************************************/
   2.345 +	/*                     calculation of crossings                     */
   2.346 +	/********************************************************************/
   2.347 +
   2.348 +	public int count_crossings(Vector layers,int oldcr) {
   2.349 +		int i,j,y1,y2,cr=0,l;
   2.350 +		for (l=0;l<layers.size()-1;l++) {
   2.351 +			Vector v1=(Vector)(layers.elementAt(l));
   2.352 +			for (i=0;i<v1.size();i++) {
   2.353 +				Enumeration e2=((Vertex)(v1.elementAt(i))).getChildren();
   2.354 +				while (e2.hasMoreElements()) {
   2.355 +					y1=((Vector)(layers.elementAt(l+1))).indexOf(e2.nextElement());
   2.356 +					for (j=0;j<i;j++) {
   2.357 +						Enumeration e3=((Vertex)(v1.elementAt(j))).getChildren();
   2.358 +						while (e3.hasMoreElements()) {
   2.359 +							y2=((Vector)(layers.elementAt(l+1))).indexOf(e3.nextElement());
   2.360 +							if (y1<y2) {
   2.361 +								cr++;
   2.362 +								if (cr>=oldcr) return cr;
   2.363 +							}
   2.364 +						}
   2.365 +					}
   2.366 +				}
   2.367 +			}
   2.368 +		}
   2.369 +		return cr;
   2.370 +	}
   2.371 +
   2.372 +	/********************************************************************/
   2.373 +	/* calculation of crossings where vertices vx1 and vx2 are involved */
   2.374 +	/* vx1 and vx2 must be in same layer and vx1 is left from vx2       */
   2.375 +	/********************************************************************/
   2.376 +
   2.377 +	public int count_crossings_2(Vector layers,Vertex vx1,Vertex vx2,int oldcr) {
   2.378 +		int i,cr=0,l=vx1.getDegree();
   2.379 +		Vertex va,vb;
   2.380 +		Vector layer;
   2.381 +		Enumeration e1,e2;
   2.382 +
   2.383 +		if (l>0) {
   2.384 +			layer=(Vector)(layers.elementAt(l-1));
   2.385 +			e1=vx1.getParents();
   2.386 +			while (e1.hasMoreElements()) {
   2.387 +				va=(Vertex)(e1.nextElement());
   2.388 +				i=layer.indexOf(va);
   2.389 +				e2=vx2.getParents();
   2.390 +				while (e2.hasMoreElements()) {
   2.391 +					vb=(Vertex)(e2.nextElement());
   2.392 +					if (layer.indexOf(vb)<i) {
   2.393 +						cr++;
   2.394 +						if (cr>=oldcr) return cr;
   2.395 +					}
   2.396 +				}
   2.397 +			}
   2.398 +		}
   2.399 +		if (l<layers.size()-1) {
   2.400 +			layer=(Vector)(layers.elementAt(l+1));
   2.401 +			e1=vx1.getChildren();
   2.402 +			while (e1.hasMoreElements()) {
   2.403 +				va=(Vertex)(e1.nextElement());
   2.404 +				i=layer.indexOf(va);
   2.405 +				e2=vx2.getChildren();
   2.406 +				while (e2.hasMoreElements()) {
   2.407 +					vb=(Vertex)(e2.nextElement());
   2.408 +					if (layer.indexOf(vb)<i) {
   2.409 +						cr++;
   2.410 +						if (cr>=oldcr) return cr;
   2.411 +					}
   2.412 +				}
   2.413 +			}
   2.414 +		}
   2.415 +		return cr;
   2.416 +	}
   2.417 +
   2.418 +	/********************************************************************/
   2.419 +	/*       reduction of crossings by exchanging adjacent vertices     */
   2.420 +	/********************************************************************/
   2.421 +
   2.422 +	public void exchangeVertices(Vector layers,int oldcr) {
   2.423 +		int i,l,c1,c2;
   2.424 +		Vertex vx1,vx2;
   2.425 +		Vector v1;
   2.426 +
   2.427 +		for (l=0;l<layers.size();l++) {
   2.428 +			v1=(Vector)(layers.elementAt(l));
   2.429 +			for (i=0;i<v1.size()-1;i++) {
   2.430 +				vx1=(Vertex)(v1.elementAt(i));
   2.431 +				vx2=(Vertex)(v1.elementAt(i+1));
   2.432 +				c1=count_crossings_2(layers,vx1,vx2,oldcr);
   2.433 +				c2=count_crossings_2(layers,vx2,vx1,c1);
   2.434 +				if (c2<c1) {
   2.435 +					v1.setElementAt(vx2,i);
   2.436 +					v1.setElementAt(vx1,i+1);
   2.437 +				}
   2.438 +			}
   2.439 +		}
   2.440 +	}
   2.441 +
   2.442 +	/********************************************************************/
   2.443 +	/*                    minimization of crossings                     */
   2.444 +	/********************************************************************/
   2.445 +
   2.446 +	public Vector min_crossings(Vector layers) {
   2.447 +		int n,i,l,k,z=0,cr2,cr=count_crossings(layers,Integer.MAX_VALUE);
   2.448 +		boolean topdown=true,first=true;
   2.449 +		Enumeration e1,e2;
   2.450 +		Vector v1,v2,layers2=null,best=layers;
   2.451 +		Vertex vx1,vx2;
   2.452 +		n=0;
   2.453 +		while (n<3 && cr>0) {
   2.454 +			if (topdown) {
   2.455 +				/** top-down-traversal **/
   2.456 +
   2.457 +				layers2=new Vector(10,10);
   2.458 +				for (l=0;l<layers.size();l++) {
   2.459 +					v1=(Vector)(layers.elementAt(l));
   2.460 +					if (l==0) layers2.addElement(v1.clone());
   2.461 +					else {
   2.462 +						v2=new Vector(10,10);
   2.463 +						layers2.addElement(v2);
   2.464 +						e1=v1.elements();
   2.465 +						while (e1.hasMoreElements()) {
   2.466 +							vx1=(Vertex)(e1.nextElement());
   2.467 +							k=0;z=0;
   2.468 +							e2=vx1.getParents();
   2.469 +							while (e2.hasMoreElements()) {
   2.470 +								k+=((Vector)(layers2.elementAt(l-1))).indexOf(e2.nextElement());
   2.471 +								z++;
   2.472 +							}
   2.473 +							if (z>0)
   2.474 +								vx1.setWeight(((double)(k))/z);
   2.475 +							else if (first)
   2.476 +								vx1.setWeight(Double.MAX_VALUE);
   2.477 +							for (i=0;i<v2.size();i++)
   2.478 +								if (vx1.getWeight()<((Vertex)(v2.elementAt(i))).getWeight()) break;
   2.479 +							if (i==v2.size()) v2.addElement(vx1);
   2.480 +							else v2.insertElementAt(vx1,i);
   2.481 +						}
   2.482 +					}
   2.483 +				}
   2.484 +			} else {
   2.485 +				/** bottom-up-traversal **/
   2.486 +
   2.487 +				layers2=new Vector(10,10);
   2.488 +				for (l=layers.size()-1;l>=0;l--) {
   2.489 +					v1=(Vector)(layers.elementAt(l));
   2.490 +					if (l==layers.size()-1) layers2.addElement(v1.clone());
   2.491 +					else {
   2.492 +						v2=new Vector(10,10);
   2.493 +						layers2.insertElementAt(v2,0);
   2.494 +						e1=v1.elements();
   2.495 +						while (e1.hasMoreElements()) {
   2.496 +							vx1=(Vertex)(e1.nextElement());
   2.497 +							k=0;z=0;
   2.498 +							e2=vx1.getChildren();
   2.499 +							while (e2.hasMoreElements()) {
   2.500 +								k+=((Vector)(layers2.elementAt(1))).indexOf(e2.nextElement());
   2.501 +								z++;
   2.502 +							}
   2.503 +							if (z>0)
   2.504 +								vx1.setWeight(((double)(k))/z);
   2.505 +							else if (first)
   2.506 +								vx1.setWeight(Double.MAX_VALUE);
   2.507 +							for (i=0;i<v2.size();i++)
   2.508 +								if (vx1.getWeight()<((Vertex)(v2.elementAt(i))).getWeight()) break;
   2.509 +							if (i==v2.size()) v2.addElement(vx1);
   2.510 +							else v2.insertElementAt(vx1,i);
   2.511 +						}
   2.512 +					}
   2.513 +				}
   2.514 +			}
   2.515 +			//exchangeVertices(layers2,cr);
   2.516 +			topdown=!topdown;
   2.517 +			first=false;
   2.518 +			layers=layers2;
   2.519 +
   2.520 +			cr2=count_crossings(layers2,cr);
   2.521 +			if (cr2<cr) {
   2.522 +				best=layers2;
   2.523 +				cr=cr2;					
   2.524 +			} else n++;
   2.525 +		}
   2.526 +
   2.527 +		while (true) {
   2.528 +			exchangeVertices(best,cr);
   2.529 +			cr2=count_crossings(best,cr);
   2.530 +			if (cr2<cr)
   2.531 +				cr=cr2;
   2.532 +			else
   2.533 +				break;
   2.534 +		}
   2.535 +
   2.536 +		return best;
   2.537 +	}
   2.538 +
   2.539 +	/********************************************************************/
   2.540 +	/*                   set initial coordinates                        */
   2.541 +	/********************************************************************/
   2.542 +
   2.543 +	public void init_coordinates(Vector layers) {
   2.544 +		int y=0;
   2.545 +		Enumeration e1=layers.elements();
   2.546 +		Enumeration e3=numEdges.elements();
   2.547 +		while (e1.hasMoreElements()) {
   2.548 +			Vector v1=(Vector)(e1.nextElement());
   2.549 +			Enumeration e2=v1.elements();
   2.550 +			int x=box_width2;
   2.551 +			while (e2.hasMoreElements()) {
   2.552 +				Vertex ve=(Vertex)(e2.nextElement());
   2.553 +				ve.setX(x);
   2.554 +				ve.setY(y);
   2.555 +				x+=box_hspace;
   2.556 +			}
   2.557 +			y+=box_height+Math.max(35,7*(((Integer)(e3.nextElement())).intValue()));
   2.558 +		}
   2.559 +	}
   2.560 +
   2.561 +	/********************************************************************/
   2.562 +	/*                       pendulum method                            */
   2.563 +	/********************************************************************/
   2.564 +
   2.565 +	public void pendulum(Vector layers) {
   2.566 +		Vector layers2=new Vector(10,10);
   2.567 +		Enumeration e1=layers.elements(),e2;
   2.568 +		int i,j,d1,d2,k,offset,dsum;
   2.569 +		Region r1,r2;
   2.570 +		boolean change;
   2.571 +
   2.572 +		while (e1.hasMoreElements()) {
   2.573 +			e2=((Vector)(e1.nextElement())).elements();
   2.574 +			Vector layer=new Vector(10,10);
   2.575 +			layers2.addElement(layer);
   2.576 +			while (e2.hasMoreElements()) {
   2.577 +				Region r=new Region(this);
   2.578 +				r.addVertex((Vertex)(e2.nextElement()));
   2.579 +				layer.addElement(r);
   2.580 +			}
   2.581 +		}
   2.582 +		for (k=0;k<10;k++) {
   2.583 +			dsum=0;
   2.584 +			for (j=1;j<layers2.size();j++) {
   2.585 +				Vector l=(Vector)(layers2.elementAt(j));
   2.586 +				if (l.size()>=2) {
   2.587 +					do {
   2.588 +						change=false;
   2.589 +						d1=((Region)(l.firstElement())).pred_deflection();
   2.590 +						for (i=0;i<l.size()-1;i++) {
   2.591 +							r1=(Region)(l.elementAt(i));
   2.592 +							r2=(Region)(l.elementAt(i+1));
   2.593 +							d2=r2.pred_deflection();
   2.594 +							if (r1.touching(r2) && (d1 <= 0 && d2 < d1 ||
   2.595 +								d2 > 0 && d1 > d2 || d1 > 0 && d2 < 0)) {
   2.596 +								r1.combine(r2);
   2.597 +								l.removeElement(r2);
   2.598 +								change=true;
   2.599 +								d2=r1.pred_deflection();
   2.600 +							}
   2.601 +							d1=d2;
   2.602 +						}
   2.603 +					} while (change);
   2.604 +				}
   2.605 +				for (i=0;i<l.size();i++) {
   2.606 +					r1=(Region)(l.elementAt(i));
   2.607 +					d1=r1.pred_deflection();
   2.608 +					offset=d1;
   2.609 +					if (d1<0 && i>0) offset=-Math.min(
   2.610 +						((Region)(l.elementAt(i-1))).spaceBetween(r1),-d1);
   2.611 +					if (d1>=0 && i<l.size()-1) offset=Math.min(
   2.612 +						r1.spaceBetween((Region)(l.elementAt(i+1))),d1);
   2.613 +					r1.move(offset);
   2.614 +					dsum+=Math.abs(d1);
   2.615 +				}		
   2.616 +			}
   2.617 +			if (dsum==0) break;
   2.618 +		}
   2.619 +	}		
   2.620 +
   2.621 +	/********************************************************************/
   2.622 +	/*                      rubberband method                           */
   2.623 +	/********************************************************************/
   2.624 +
   2.625 +	public void rubberband(Vector layers) {
   2.626 +		Enumeration e1,e2;
   2.627 +		int i,n,k,d,d2;
   2.628 +		Vector v;
   2.629 +		Vertex vx;
   2.630 +
   2.631 +		for (k=0;k<10;k++) {
   2.632 +			e1=layers.elements();
   2.633 +			while (e1.hasMoreElements()) {
   2.634 +				v=(Vector)(e1.nextElement());
   2.635 +				for (i=0;i<v.size();i++) {
   2.636 +					n=0;d=0;
   2.637 +					vx=(Vertex)(v.elementAt(i));
   2.638 +					e2=vx.getChildren();
   2.639 +					while (e2.hasMoreElements()) {
   2.640 +						d+=((Vertex)(e2.nextElement())).getX()-vx.getX();
   2.641 +						n++;
   2.642 +					}
   2.643 +					e2=vx.getParents();
   2.644 +					while (e2.hasMoreElements()) {
   2.645 +						d+=((Vertex)(e2.nextElement())).getX()-vx.getX();
   2.646 +						n++;
   2.647 +					}
   2.648 +					d2=(n!=0?d/n:0);
   2.649 +
   2.650 +					if (d<0 && (i==0 || ((Vertex)(v.elementAt(i-1))).rightX()+box_hspace-box_width < vx.leftX()+d2) ||
   2.651 +						d>0 && (i==v.size()-1 || ((Vertex)(v.elementAt(i+1))).leftX()-box_hspace+box_width > vx.rightX()+d2))
   2.652 +						vx.setX(vx.getX()+d2);
   2.653 +				}
   2.654 +			}
   2.655 +		}
   2.656 +	}
   2.657 +
   2.658 +	/**** Intersection point of two lines (auxiliary function for calcSplines)   ****/
   2.659 +	/**** Calculate intersection point of line which is parallel to line (p1,p2) ****/
   2.660 +	/**** and leads through p5, with line (p3,p4)                                ****/
   2.661 +
   2.662 +	Point intersect(Point p1,Point p2,Point p3,Point p4,Point p5) {
   2.663 +		float x=0,y=0,s1=0,s2=0;
   2.664 +
   2.665 +		if (p1.x!=p2.x)
   2.666 +			s1=((float)(p2.y-p1.y))/(p2.x-p1.x);
   2.667 +		if (p3.x!=p4.x)
   2.668 +			s2=((float)(p4.y-p3.y))/(p4.x-p3.x);
   2.669 +		if (p1.x==p2.x) {
   2.670 +			x=p5.x;
   2.671 +			y=s2*(p5.x-p3.x)+p3.y;
   2.672 +		} else if (p3.x==p4.x) {
   2.673 +			x=p3.x;
   2.674 +			y=s1*(p3.x-p5.x)+p5.y;
   2.675 +		} else {
   2.676 +			x=(p5.x*s1-p3.x*s2+p3.y-p5.y)/(s1-s2);
   2.677 +			y=s2*(x-p3.x)+p3.y;
   2.678 +		}
   2.679 +		return new Point(Math.round(x),Math.round(y));
   2.680 +	}
   2.681 +
   2.682 +	/**** Calculate control points (auxiliary function for calcSplines) ****/
   2.683 +
   2.684 +	Points calcPoint(Point p1,Point p2,Point p3,int lboxx,int rboxx,int boxy) {
   2.685 +
   2.686 +		/*** Points p1 , p2 , p3 define a triangle which encloses the spline.  ***/
   2.687 +		/*** Check if adjacent boxes (specified by lboxx,rboxx and boxy)       ***/
   2.688 +		/*** collide with the spline. In this case p1 and p3 are shifted by an ***/
   2.689 +		/*** appropriate offset before they are returned                       ***/
   2.690 +
   2.691 +		int xh1,xh2,bx=0,by=0;
   2.692 +		boolean pt1 = boxy >= p1.y && boxy <= p3.y || boxy >= p3.y && boxy <= p1.y;
   2.693 +		boolean pt2 = boxy+box_height >= p1.y && boxy+box_height <= p3.y ||
   2.694 +                              boxy+box_height >= p3.y && boxy+box_height <= p1.y;
   2.695 +		boolean move = false;
   2.696 +		Point b;
   2.697 +
   2.698 +		xh1 = p1.x+(boxy-p1.y)*(p3.x-p1.x)/(p3.y-p1.y);
   2.699 +		xh2 = p1.x+(boxy+box_height-p1.y)*(p3.x-p1.x)/(p3.y-p1.y);
   2.700 +
   2.701 +		if (xh1 <= lboxx && pt1 && xh2 <= lboxx && pt2) {
   2.702 +			move = true;
   2.703 +			bx = lboxx;
   2.704 +			by = boxy + (xh1 < xh2 ? 0 : box_height ) ;
   2.705 +		} else if (xh1 >= rboxx && pt1 && xh2 >= rboxx && pt2) {
   2.706 +			move = true;
   2.707 +			bx = rboxx;
   2.708 +			by = boxy + (xh1 > xh2 ? 0 : box_height ) ;
   2.709 +		} else if ( (xh1 <= lboxx || xh1 >= rboxx) && pt1) {
   2.710 +			move = true;
   2.711 +			bx = (xh1 <= lboxx ? lboxx : rboxx ) ;
   2.712 +			by = boxy;
   2.713 +		} else if ( (xh2 <= lboxx || xh2 >= rboxx) && pt2) {
   2.714 +			move = true;
   2.715 +			bx = (xh2 <= lboxx ? lboxx : rboxx ) ;
   2.716 +			by = boxy+box_height;
   2.717 +		}
   2.718 +		b=new Point(bx,by);
   2.719 +		if (move) return new Points(intersect(p1,p3,p1,p2,b),intersect(p1,p3,p2,p3,b));
   2.720 +		else return new Points(p1,p3);
   2.721 +	}
   2.722 +
   2.723 +	/********************************************************************/
   2.724 +	/*                        calculate splines                         */
   2.725 +	/********************************************************************/
   2.726 +
   2.727 +	public void calcSplines(Vector layers) {
   2.728 +		Enumeration e2,e1=vertices.elements();
   2.729 +		Vertex vx1,vx2,vx3;
   2.730 +		Vector pos,layer;
   2.731 +		int x1,y1,x2,y2,x3,y3,xh,k,leftx,rightx,spc;
   2.732 +
   2.733 +		while (e1.hasMoreElements()) {
   2.734 +			vx1=(Vertex)(e1.nextElement());
   2.735 +			if (!vx1.isDummy()) {
   2.736 +				e2=vx1.getChildren();
   2.737 +				while (e2.hasMoreElements()) {
   2.738 +					vx2=(Vertex)(e2.nextElement());
   2.739 +					if (vx2.isDummy()) {
   2.740 +						vx3=vx2;
   2.741 +						/**** convert edge to spline ****/
   2.742 +						pos=new Vector(10,10);
   2.743 +						x1=vx1.getX();
   2.744 +						y1=vx1.getY()+box_height;
   2.745 +
   2.746 +						do {
   2.747 +							/*** calculate position of control points ***/
   2.748 +							x2=vx2.getX();
   2.749 +							y2=vx2.getY();
   2.750 +							layer=(Vector)(layers.elementAt(vx2.getDegree()));
   2.751 +							k=layer.indexOf(vx2);
   2.752 +							vx2=(Vertex)((vx2.getChildren()).nextElement());
   2.753 +							x3=vx2.getX();
   2.754 +							y3=vx2.getY();
   2.755 +							// spc=(box_hspace-box_width)/3;
   2.756 +							// spc=box_height*3/4;
   2.757 +							spc=0;
   2.758 +							leftx = k==0 /* || ((Vertex)(layer.elementAt(k-1))).isDummy() */ ?
   2.759 +								Integer.MIN_VALUE:
   2.760 +								((Vertex)(layer.elementAt(k-1))).rightX()+spc;
   2.761 +							rightx = k==layer.size()-1 /* || ((Vertex)(layer.elementAt(k+1))).isDummy() */ ?
   2.762 +								Integer.MAX_VALUE:
   2.763 +								((Vertex)(layer.elementAt(k+1))).leftX()-spc;
   2.764 +							xh=x2+box_height*(x3-x2)/(y3-y2);
   2.765 +							if (!(x2<=x3 && xh>=rightx || x2>x3 && xh<=leftx)) {
   2.766 +								/* top control point */
   2.767 +								pos.addElement(new Integer(1));
   2.768 +								y1=y2;
   2.769 +							} else {
   2.770 +								xh=x1+(y2-y1)*(x2-x1)/(y2+box_height-y1);
   2.771 +								if (!(x2<=x1 && xh>=rightx || x2>x1 && xh<=leftx))
   2.772 +									/* bottom control point */
   2.773 +									pos.addElement(new Integer(2));
   2.774 +								else
   2.775 +									/* two control points needed */
   2.776 +									pos.addElement(new Integer(3));
   2.777 +								y1=y2+box_height;
   2.778 +							}
   2.779 +							x1=x2;
   2.780 +						} while (vx2.isDummy());
   2.781 +						pos.addElement(new Integer(1));
   2.782 +
   2.783 +						/**** calculate triangles ****/
   2.784 +						vx2=vx3;
   2.785 +
   2.786 +						int pos1,pos2,i=0;
   2.787 +						Vector pts=new Vector(10,10);
   2.788 +						int lboxx,rboxx,boxy;
   2.789 +
   2.790 +						x1=vx1.getX();
   2.791 +						y1=vx1.getY()+box_height;
   2.792 +						pts.addElement(new Point(x1,y1)); /** edge starting point **/
   2.793 +						do {
   2.794 +							x2=vx2.getX();
   2.795 +							y2=vx2.getY();
   2.796 +							pos1=((Integer)(pos.elementAt(i))).intValue();
   2.797 +							pos2=((Integer)(pos.elementAt(i+1))).intValue();
   2.798 +							i++;
   2.799 +							layer=(Vector)(layers.elementAt(vx2.getDegree()));
   2.800 +							k=layer.indexOf(vx2);
   2.801 +							boxy=vx2.getY();
   2.802 +							vx2=(Vertex)((vx2.getChildren()).nextElement());
   2.803 +							x3=vx2.getX();
   2.804 +							y3=vx2.getY();
   2.805 +							if (pos1==2) y2+=box_height;
   2.806 +							if (pos2==2) y3+=box_height;
   2.807 +
   2.808 +							lboxx = (k==0 /* || ((Vertex)(layer.elementAt(k-1))).isDummy() */ ) ?
   2.809 +								Integer.MIN_VALUE :
   2.810 +								((Vertex)(layer.elementAt(k-1))).rightX();
   2.811 +
   2.812 +							rboxx = (k==layer.size()-1 /* || ((Vertex)(layer.elementAt(k+1))).isDummy() */ ) ?
   2.813 +								Integer.MAX_VALUE :
   2.814 +								((Vertex)(layer.elementAt(k+1))).leftX();
   2.815 +
   2.816 +							Point p1,p2,p3;
   2.817 +							Points ps;
   2.818 +
   2.819 +							p1 = new Point((x1+x2)/2,(y1+y2)/2);
   2.820 +
   2.821 +							if (pos1<=2) {
   2.822 +								/** one control point **/
   2.823 +								p2 = new Point(x2,y2);
   2.824 +								ps = calcPoint(p1,p2,new Point((x2+x3)/2,(y2+y3)/2),lboxx,rboxx,boxy);
   2.825 +								pts.addElement(ps.p);
   2.826 +								pts.addElement(p2);
   2.827 +								pts.addElement(ps.q);
   2.828 +							} else {
   2.829 +								/** two control points **/
   2.830 +								p2 = new Point(x2,y2-box_height);
   2.831 +								p3 = new Point(x2,y2+box_height2);
   2.832 +								ps = calcPoint(p1,p2,p3,lboxx,rboxx,boxy);
   2.833 +								pts.addElement(ps.p);
   2.834 +								pts.addElement(p2);
   2.835 +								pts.addElement(ps.q);
   2.836 +								p2 = new Point(x2,y2+box_height*2);
   2.837 +								ps = calcPoint(p3,p2,new Point((p2.x+x3)/2,(p2.y+y3)/2),
   2.838 +								               lboxx,rboxx,boxy);
   2.839 +								pts.addElement(ps.p);
   2.840 +								pts.addElement(p2);
   2.841 +								pts.addElement(ps.q);
   2.842 +							}
   2.843 +							x1=p2.x;
   2.844 +							y1=p2.y;
   2.845 +						} while (vx2.isDummy());
   2.846 +
   2.847 +						pts.addElement(new Point(vx2.getX(),vx2.getY())); /** edge end point **/
   2.848 +						splines.addElement(new Spline(pts));
   2.849 +					}
   2.850 +				}
   2.851 +			}
   2.852 +		}
   2.853 +	}
   2.854 +
   2.855 +	/********************************************************************/
   2.856 +	/*                      calculate bounding box                      */
   2.857 +	/********************************************************************/
   2.858 +
   2.859 +	public void calcBoundingBox() {
   2.860 +		min_y=min_x=Integer.MAX_VALUE;
   2.861 +		max_y=max_x=Integer.MIN_VALUE;
   2.862 +
   2.863 +		Enumeration e1=vertices.elements();
   2.864 +		Vertex v;
   2.865 +
   2.866 +		while (e1.hasMoreElements()) {
   2.867 +			v=(Vertex)(e1.nextElement());
   2.868 +			min_x=Math.min(min_x,v.leftX());
   2.869 +			max_x=Math.max(max_x,v.rightX());
   2.870 +			min_y=Math.min(min_y,v.getY());
   2.871 +			max_y=Math.max(max_y,v.getY()+box_height);
   2.872 +		}
   2.873 +		min_x-=20;
   2.874 +		min_y-=20;
   2.875 +		max_x+=20;
   2.876 +		max_y+=20;
   2.877 +	}
   2.878 +
   2.879 +	/********************************************************************/
   2.880 +	/*                           draw graph                             */
   2.881 +	/********************************************************************/
   2.882 +					 
   2.883 +	public void draw(Graphics g) {
   2.884 +		if (box_height==0) layout(g);
   2.885 +
   2.886 +		g.translate(-min_x,-min_y);
   2.887 +
   2.888 +		Enumeration e1=vertices.elements();
   2.889 +		while (e1.hasMoreElements())
   2.890 +			((Vertex)(e1.nextElement())).draw(g);
   2.891 +
   2.892 +		e1=splines.elements();
   2.893 +		while (e1.hasMoreElements())
   2.894 +			((Spline)(e1.nextElement())).draw(g);
   2.895 +	}
   2.896 +
   2.897 +	/********************************************************************/
   2.898 +	/*               return vertex at position (x,y)                    */
   2.899 +	/********************************************************************/
   2.900 +
   2.901 +	public Vertex vertexAt(int x,int y) {
   2.902 +		Enumeration e1=vertices.elements();
   2.903 +		while (e1.hasMoreElements()) {
   2.904 +			Vertex v=(Vertex)(e1.nextElement());
   2.905 +			if (v.contains(x,y)) return v;
   2.906 +		}
   2.907 +		return null;
   2.908 +	}
   2.909 +
   2.910 +	/********************************************************************/
   2.911 +	/*       encode list of vertices (as array of vertice numbers)      */
   2.912 +	/********************************************************************/
   2.913 +
   2.914 +	public Vector encode(Vector v) {
   2.915 +		Vector code=new Vector(10,10);
   2.916 +		Enumeration e1=v.elements();
   2.917 +
   2.918 +		while (e1.hasMoreElements()) {
   2.919 +			Vertex vx=(Vertex)(e1.nextElement());
   2.920 +			if (vx.getNumber()>=0)
   2.921 +				code.addElement(new Integer(vx.getNumber()));
   2.922 +		}
   2.923 +		return code;
   2.924 +	}
   2.925 +
   2.926 +	/********************************************************************/
   2.927 +	/*                      get vertex with number n                    */
   2.928 +	/********************************************************************/
   2.929 +
   2.930 +	public Vertex getVertexByNum(int x) {
   2.931 +		Enumeration e1=vertices.elements();
   2.932 +
   2.933 +		while (e1.hasMoreElements()) {
   2.934 +			Vertex vx=(Vertex)(e1.nextElement());
   2.935 +			if (vx.getNumber()==x) return vx;
   2.936 +		}
   2.937 +		return null;
   2.938 +	}
   2.939 +
   2.940 +	/********************************************************************/
   2.941 +	/*                      decode list of vertices                     */
   2.942 +	/********************************************************************/
   2.943 +
   2.944 +	public Vector decode(Vector code) {
   2.945 +		Enumeration e1=code.elements();
   2.946 +		Vector vec=new Vector(10,10);
   2.947 +
   2.948 +		while (e1.hasMoreElements()) {
   2.949 +			int i=((Integer)(e1.nextElement())).intValue();
   2.950 +			//Vertex vx=getVertexByNum(i);
   2.951 +			//if (vx!=null) vec.addElement(vx);
   2.952 +			vec.addElement(vertices2[i]);
   2.953 +		}
   2.954 +		return vec;
   2.955 +	}
   2.956 +
   2.957 +	/********************************************************************/
   2.958 +	/*                       collapse vertices                          */
   2.959 +	/********************************************************************/
   2.960 +
   2.961 +	public void collapse(Vector vs,String name,Vector inflate) {
   2.962 +		Enumeration e1,e2,e3;
   2.963 +		boolean nonempty=false;
   2.964 +		Vertex vx3,vx2,vx1;
   2.965 +		
   2.966 +		e1=vertices.elements();
   2.967 +
   2.968 +		vx1=new NormalVertex(name);
   2.969 +		vx1.setInflate(inflate);
   2.970 +
   2.971 +		while (e1.hasMoreElements()) {
   2.972 +			vx2=(Vertex)(e1.nextElement());
   2.973 +
   2.974 +			if (vs.indexOf(vx2)<0) {
   2.975 +				e2=vx2.getParents();
   2.976 +				while (e2.hasMoreElements()) {
   2.977 +					vx3=(Vertex)(e2.nextElement());
   2.978 +					if (vs.indexOf(vx3)>=0) {
   2.979 +						if (!vx1.isChild(vx2))
   2.980 +							vx1.addChild(vx2);
   2.981 +						vx3.removeChild(vx2);
   2.982 +					}
   2.983 +				}
   2.984 +
   2.985 +				e2=vx2.getChildren();
   2.986 +				while (e2.hasMoreElements()) {
   2.987 +					vx3=(Vertex)(e2.nextElement());
   2.988 +					if (vs.indexOf(vx3)>=0) {
   2.989 +						if (!vx2.isChild(vx1))
   2.990 +							vx2.addChild(vx1);
   2.991 +						vx2.removeChild(vx3);
   2.992 +					}
   2.993 +				}
   2.994 +			} else { nonempty=true; }
   2.995 +		}
   2.996 +
   2.997 +		e1=vs.elements();
   2.998 +		while (e1.hasMoreElements())
   2.999 +			try {
  2.1000 +				removeVertex((Vertex)(e1.nextElement()));
  2.1001 +			} catch (NoSuchElementException exn) {}
  2.1002 +
  2.1003 +		if (nonempty) addVertex(vx1);
  2.1004 +	}
  2.1005 +
  2.1006 +	/********************************************************************/
  2.1007 +	/*                      PostScript output                           */
  2.1008 +	/********************************************************************/
  2.1009 +
  2.1010 +	public void PS(String fname,boolean printable) throws IOException {
  2.1011 +		FileOutputStream f = new FileOutputStream(fname);
  2.1012 +		PrintStream p = new PrintStream(f);
  2.1013 +
  2.1014 +		if (printable)
  2.1015 +			p.println("%!PS-Adobe-2.0\n\n%%BeginProlog");
  2.1016 +		else {
  2.1017 +			p.println("%!PS-Adobe-2.0 EPSF-2.0\n%%Orientation: Portrait");
  2.1018 +			p.println("%%BoundingBox: "+min_x+" "+min_y+" "+max_x+" "+max_y);
  2.1019 +			p.println("%%EndComments\n\n%%BeginProlog");
  2.1020 +		}
  2.1021 +		p.println("/m { moveto } def /l { lineto } def /n { newpath } def");
  2.1022 +		p.println("/s { stroke } def /c { curveto } def");
  2.1023 +		p.println("/b { n 0 0 m dup true charpath pathbbox 1 index 4 index sub");
  2.1024 +		p.println("7 index exch sub 2 div 9 index add 1 index 4 index sub 7 index exch sub");
  2.1025 +		p.println("2 div 9 index add 2 index add m pop pop pop pop");
  2.1026 +		p.println("1 -1 scale show 1 -1 scale n 3 index 3 index m 1 index 0 rlineto");
  2.1027 +		p.println("0 exch rlineto neg 0 rlineto closepath s pop pop } def");
  2.1028 +		p.println("%%EndProlog\n");
  2.1029 +		if (printable) {
  2.1030 +			int hsize=max_x-min_x;
  2.1031 +			int vsize=max_y-min_y;
  2.1032 +			if (hsize>vsize) {
  2.1033 +				// Landscape output
  2.1034 +				double scale=Math.min(1,Math.min(750.0/hsize,500.0/vsize));
  2.1035 +				double trans_x=50+max_y*scale+(500-scale*vsize)/2.0;
  2.1036 +				double trans_y=50+max_x*scale+(750-scale*hsize)/2.0;
  2.1037 +				p.println(trans_x+" "+trans_y+" translate");
  2.1038 +				p.println("-90 rotate");
  2.1039 +				p.println(scale+" "+(-scale)+" scale");
  2.1040 +			} else {
  2.1041 +				// Portrait output
  2.1042 +				double scale=Math.min(1,Math.min(500.0/hsize,750.0/vsize));
  2.1043 +				double trans_x=50-min_x*scale+(500-scale*hsize)/2.0;
  2.1044 +				double trans_y=50+max_y*scale+(750-scale*vsize)/2.0;
  2.1045 +				p.println(trans_x+" "+trans_y+" translate");
  2.1046 +				p.println(scale+" "+(-scale)+" scale");
  2.1047 +			}
  2.1048 +		} else
  2.1049 +			p.println("0 "+(max_y+min_y)+" translate\n1 -1 scale");
  2.1050 +
  2.1051 +		p.println("/Helvetica findfont 12 scalefont setfont");
  2.1052 +		p.println("0.5 setlinewidth");
  2.1053 +
  2.1054 +		Enumeration e1=vertices.elements();
  2.1055 +		while (e1.hasMoreElements())
  2.1056 +			((Vertex)(e1.nextElement())).PS(p);
  2.1057 +
  2.1058 +		e1=splines.elements();
  2.1059 +		while (e1.hasMoreElements())
  2.1060 +			((Spline)(e1.nextElement())).PS(p);
  2.1061 +
  2.1062 +		if (printable) p.println("showpage");
  2.1063 +
  2.1064 +		f.close();
  2.1065 +	}
  2.1066 +}
  2.1067 +
  2.1068 +/**** Return value of function calcPoint ****/
  2.1069 +
  2.1070 +class Points {
  2.1071 +	public Point p,q;
  2.1072 +
  2.1073 +	public Points(Point p1,Point p2) {
  2.1074 +		p=p1;q=p2;
  2.1075 +	}
  2.1076 +}
  2.1077 +
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/lib/browser/GraphBrowser/GraphBrowser.java	Wed Aug 06 00:06:47 1997 +0200
     3.3 @@ -0,0 +1,190 @@
     3.4 +/***************************************************************************
     3.5 +  Title:      GraphBrowser/GraphBrowser.java
     3.6 +  ID:         $Id$
     3.7 +  Author:     Stefan Berghofer, TU Muenchen
     3.8 +  Copyright   1997  TU Muenchen
     3.9 +
    3.10 +  This is the graph browser's main class. It contains the "main(...)"
    3.11 +  method, which is used for the stand-alone version, as well as
    3.12 +  "init(...)", "start(...)" and "stop(...)" methods which are used for
    3.13 +  the applet version.
    3.14 +  Note: GraphBrowser is designed for the 1.0.2 version of the JDK.
    3.15 +***************************************************************************/
    3.16 +
    3.17 +package GraphBrowser;
    3.18 +
    3.19 +import java.awt.*;
    3.20 +import java.applet.*;
    3.21 +import java.io.*;
    3.22 +import java.util.*;
    3.23 +import java.net.*;
    3.24 +import awtUtilities.*;
    3.25 +
    3.26 +public class GraphBrowser extends Applet {
    3.27 +	GraphView gv;
    3.28 +	TreeBrowser tb=null;
    3.29 +	String gfname;
    3.30 +
    3.31 +	static boolean isApplet;
    3.32 +	static Frame f;
    3.33 +
    3.34 +	public GraphBrowser(String name) {
    3.35 +		gfname=name;
    3.36 +	}
    3.37 +
    3.38 +	public GraphBrowser() {}
    3.39 +
    3.40 +	public void showWaitMessage() {
    3.41 +		if (isApplet)
    3.42 +			getAppletContext().showStatus("calculating layout, please wait ...");
    3.43 +		else {
    3.44 +			f.setCursor(Frame.WAIT_CURSOR);
    3.45 +		}
    3.46 +	}
    3.47 +
    3.48 +	public void showReadyMessage() {
    3.49 +		if (isApplet)
    3.50 +			getAppletContext().showStatus("ready !");
    3.51 +		else {
    3.52 +			f.setCursor(Frame.DEFAULT_CURSOR);
    3.53 +		}
    3.54 +	}
    3.55 +
    3.56 +	public void viewFile(String fname) {
    3.57 +		try {
    3.58 +			if (isApplet)
    3.59 +				getAppletContext().showDocument(new URL(getDocumentBase(), fname),"_blank");
    3.60 +			else {
    3.61 +				String path=gfname.substring(0,gfname.lastIndexOf('/')+1);
    3.62 +				InputStream is;
    3.63 +				String line, text="";
    3.64 +				DataInputStream di;
    3.65 +
    3.66 +				is=new FileInputStream(path+fname);
    3.67 +				di=new DataInputStream(is);
    3.68 +				while ((line=di.readLine())!=null)
    3.69 +					text+=line+"\n";
    3.70 +
    3.71 +				if (fname.endsWith(".html")) {
    3.72 +					/**** convert HTML to text (just a quick hack) ****/
    3.73 +
    3.74 +					String buf="";
    3.75 +					char[] text2,text3;
    3.76 +					int i,j=0;
    3.77 +					boolean special=false, html=false;
    3.78 +					char ctrl;
    3.79 +
    3.80 +					text2 = text.toCharArray();
    3.81 +					text3 = new char[text.length()];
    3.82 +					for (i = 0; i < text.length(); i++) {
    3.83 +						char c = text2[i];
    3.84 +						if (c == '&') {
    3.85 +							special = true;
    3.86 +							buf = "";
    3.87 +						} else if (special) {
    3.88 +							if (c == ';') {
    3.89 +								special = false;
    3.90 +								if (buf.equals("lt"))
    3.91 +									text3[j++] = '<';
    3.92 +								else if (buf.equals("gt"))
    3.93 +									text3[j++] = '>';
    3.94 +								else if (buf.equals("amp"))
    3.95 +									text3[j++] = '&';
    3.96 +							} else
    3.97 +								buf += c;
    3.98 +						} else if (c == '<') {
    3.99 +							html = true;
   3.100 +							ctrl = text2[i+1];
   3.101 +							if ((ctrl == 'P') || (ctrl == 'B'))
   3.102 +								text3[j++] = '\n';		
   3.103 +						} else if (c == '>')
   3.104 +							html = false;
   3.105 +						else if (!html)
   3.106 +							text3[j++] = c;
   3.107 +					}
   3.108 +					text = String.valueOf(text3);
   3.109 +				}
   3.110 +							
   3.111 +				Frame f=new TextFrame(fname.substring(fname.lastIndexOf('/')+1),text);
   3.112 +				f.resize(500,600);
   3.113 +				f.show();
   3.114 +			}
   3.115 +		} catch (Exception exn) {
   3.116 +			System.out.println("Can't read file "+fname);
   3.117 +		}
   3.118 +	}
   3.119 +				
   3.120 +	public void PS(String fname,boolean printable) throws IOException {
   3.121 +		gv.PS(fname,printable);
   3.122 +	}
   3.123 +
   3.124 +	public boolean isEmpty() {
   3.125 +		return tb==null;
   3.126 +	}
   3.127 +
   3.128 +	public void initBrowser(InputStream is) {
   3.129 +		try {
   3.130 +			TreeNode tn=new TreeNode("Directories","",-1,true);
   3.131 +			gv=new GraphView(new Graph(is,tn),this);
   3.132 +			tb=new TreeBrowser(tn,gv);
   3.133 +			gv.setTreeBrowser(tb);
   3.134 +			Vector v=new Vector(10,10);
   3.135 +			tn.collapsedDirectories(v);
   3.136 +			gv.collapseDir(v);
   3.137 +			Component gv2=new Border(gv,5);
   3.138 +			Component tb2=new Border(tb,5);
   3.139 +			GridBagLayout gridbag = new GridBagLayout();
   3.140 +			GridBagConstraints cnstr = new GridBagConstraints();
   3.141 +			setLayout(gridbag);
   3.142 +			cnstr.fill = GridBagConstraints.BOTH;
   3.143 +			cnstr.insets = new Insets(5,5,5,5);
   3.144 +			cnstr.weightx = 1;
   3.145 +			cnstr.weighty = 1;
   3.146 +			cnstr.gridwidth = 1;
   3.147 +			gridbag.setConstraints(tb2,cnstr);
   3.148 +			add(tb2);
   3.149 +			cnstr.weightx = 2.5;
   3.150 +			cnstr.gridwidth = GridBagConstraints.REMAINDER;
   3.151 +			gridbag.setConstraints(gv2,cnstr);
   3.152 +			add(gv2);
   3.153 +		} catch (IOException exn) {
   3.154 +			System.out.println("\nI/O error while reading graph file.");
   3.155 +		} catch (ParseError exn) {
   3.156 +			System.out.println("\nParse error in graph file:");
   3.157 +			System.out.println(exn.getMessage());
   3.158 +			System.out.println("\nSyntax:\n<vertexname> <dirname> [ + ] <path> [ < | > ] [ <vertexname> [ ... [ <vertexname> ] ... ] ] ;");
   3.159 +		}
   3.160 +	}		
   3.161 +
   3.162 +	public void init() {
   3.163 +		isApplet=true;
   3.164 +		gfname=getParameter("graphfile");
   3.165 +		try {
   3.166 +			InputStream is=(new URL(getDocumentBase(), gfname)).openConnection().getInputStream();
   3.167 +			initBrowser(is);
   3.168 +			is.close();
   3.169 +		} catch (MalformedURLException exn) {
   3.170 +			System.out.println("Invalid URL: "+gfname);
   3.171 +		} catch (IOException exn) {
   3.172 +			System.out.println("I/O error while reading "+gfname+".");
   3.173 +		}
   3.174 +	}
   3.175 +
   3.176 +	public static void main(String[] args) {
   3.177 +		isApplet=false;
   3.178 +		try {
   3.179 +			GraphBrowser gb=new GraphBrowser(args.length > 0 ? args[0] : "");
   3.180 +			if (args.length>0) {
   3.181 +				InputStream is=new FileInputStream(args[0]);
   3.182 +				gb.initBrowser(is);
   3.183 +				is.close();
   3.184 +			}
   3.185 +			f=new GraphBrowserFrame(gb);
   3.186 +			f.resize(700,500);
   3.187 +			f.show();
   3.188 +		} catch (IOException exn) {
   3.189 +			System.out.println("Can't open graph file "+args[0]);
   3.190 +		}
   3.191 +	}
   3.192 +}
   3.193 +
     4.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.2 +++ b/lib/browser/GraphBrowser/GraphBrowserFrame.java	Wed Aug 06 00:06:47 1997 +0200
     4.3 @@ -0,0 +1,118 @@
     4.4 +/***************************************************************************
     4.5 +  Title:      GraphBrowser/GraphBrowserFrame.java
     4.6 +  ID:         $Id$
     4.7 +  Author:     Stefan Berghofer, TU Muenchen
     4.8 +  Copyright   1997  TU Muenchen
     4.9 +
    4.10 +  This class is the frame for the stand-alone application. It contains
    4.11 +  methods for handling menubar events.
    4.12 +***************************************************************************/
    4.13 +
    4.14 +package GraphBrowser;
    4.15 +
    4.16 +import java.awt.*;
    4.17 +import java.io.*;
    4.18 +import awtUtilities.*;
    4.19 +
    4.20 +public class GraphBrowserFrame extends Frame {
    4.21 +	GraphBrowser gb;
    4.22 +	MenuItem i1,i2;
    4.23 +	String graphDir,psDir;
    4.24 +
    4.25 +	public void checkMenuItems() {
    4.26 +		if (gb.isEmpty()) {
    4.27 +			i1.disable();
    4.28 +			i2.disable();
    4.29 +		} else {
    4.30 +			i1.enable();
    4.31 +			i2.enable();
    4.32 +		}
    4.33 +	}
    4.34 +
    4.35 +	public boolean action(Event evt, Object arg) {
    4.36 +		if (evt.target instanceof MenuItem) {
    4.37 +			String label=(String)arg;
    4.38 +			if (label.equals("Quit"))
    4.39 +				System.exit(0);
    4.40 +			else if (label.equals("Export to PostScript")) {
    4.41 +				PS(true,label);
    4.42 +				return true;
    4.43 +			} else if (label.equals("Export to EPS")) {
    4.44 +				PS(false,label);
    4.45 +				return true;
    4.46 +			} else if (label.equals("Open ...")) {
    4.47 +				FileDialog fd=new FileDialog(this,"Open graph file",FileDialog.LOAD);
    4.48 +				if (graphDir!=null)
    4.49 +					fd.setDirectory(graphDir);
    4.50 +				fd.show();
    4.51 +				if (fd.getFile()==null) return true;
    4.52 +				graphDir=fd.getDirectory();
    4.53 +				String fname=graphDir+fd.getFile();
    4.54 +				GraphBrowser gb2=new GraphBrowser(fname);
    4.55 +				try {
    4.56 +					InputStream is=new FileInputStream(fname);
    4.57 +					gb2.initBrowser(is);
    4.58 +					is.close();
    4.59 +				} catch (IOException exn) {
    4.60 +					String button[]={"OK"};
    4.61 +					MessageDialog md=new MessageDialog(this,"Error","Can't open file "+fname+".",button);
    4.62 +					md.resize(350,200);
    4.63 +					md.show();
    4.64 +					return true;
    4.65 +				}
    4.66 +				remove(gb);
    4.67 +				add("Center",gb2);
    4.68 +				gb=gb2;
    4.69 +				checkMenuItems();
    4.70 +				validate();
    4.71 +				return true;
    4.72 +			}
    4.73 +		}
    4.74 +		return false;
    4.75 +	}
    4.76 +
    4.77 +	public void PS(boolean printable,String label) {
    4.78 +		FileDialog fd=new FileDialog(this,label,FileDialog.SAVE);
    4.79 +		if (psDir!=null)
    4.80 +			fd.setDirectory(psDir);
    4.81 +		fd.show();
    4.82 +		if (fd.getFile()==null) return;
    4.83 +		psDir=fd.getDirectory();
    4.84 +		String fname=psDir+fd.getFile();
    4.85 +
    4.86 +		if ((new File(fname)).exists()) {
    4.87 +			String buttons[]={"Overwrite","Cancel"};
    4.88 +			MessageDialog md=new MessageDialog(this,"Warning",
    4.89 +			      "Warning: File "+fname+" already exists. Overwrite?",
    4.90 +			      buttons);
    4.91 +			md.resize(350,200);
    4.92 +			md.show();
    4.93 +			if (md.getText().equals("Cancel")) return;
    4.94 +		}
    4.95 +
    4.96 +		try {
    4.97 +			gb.PS(fname,printable);
    4.98 +		} catch (IOException exn) {
    4.99 +			String button[]={"OK"};
   4.100 +			MessageDialog md=new MessageDialog(this,"Error",
   4.101 +			      "Unable to write file "+fname+".",button);
   4.102 +			md.resize(350,200);
   4.103 +			md.show();
   4.104 +		}
   4.105 +	}
   4.106 +
   4.107 +	public GraphBrowserFrame(GraphBrowser br) {
   4.108 +		super("GraphBrowser");
   4.109 +		gb=br;
   4.110 +		MenuBar mb=new MenuBar();
   4.111 +		Menu m1=new Menu("File");
   4.112 +		m1.add(new MenuItem("Open ..."));
   4.113 +		m1.add(i1=new MenuItem("Export to PostScript"));
   4.114 +		m1.add(i2=new MenuItem("Export to EPS"));
   4.115 +		m1.add(new MenuItem("Quit"));
   4.116 +		checkMenuItems();
   4.117 +		mb.add(m1);
   4.118 +		setMenuBar(mb);
   4.119 +		add("Center",br);
   4.120 +	}
   4.121 +}
     5.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.2 +++ b/lib/browser/GraphBrowser/GraphView.java	Wed Aug 06 00:06:47 1997 +0200
     5.3 @@ -0,0 +1,236 @@
     5.4 +/***************************************************************************
     5.5 +  Title:      GraphBrowser/GraphView.java
     5.6 +  ID:         $Id$
     5.7 +  Author:     Stefan Berghofer, TU Muenchen
     5.8 +  Copyright   1997  TU Muenchen
     5.9 +
    5.10 +  This class defines the window in which the graph is displayed. It
    5.11 +  contains methods for handling events such as collapsing / uncollapsing
    5.12 +  nodes of the graph.
    5.13 +***************************************************************************/
    5.14 +
    5.15 +package GraphBrowser;
    5.16 +
    5.17 +import java.awt.*;
    5.18 +import java.io.*;
    5.19 +import java.util.*;
    5.20 +import awtUtilities.*;
    5.21 +
    5.22 +public class GraphView extends ScrollCanvas {
    5.23 +	Graph gra,gra2;
    5.24 +	GraphBrowser parent;
    5.25 +	Vertex v=null;
    5.26 +	Vector collapsed=new Vector(10,10);
    5.27 +	Vector collapsedDirs=new Vector(10,10);
    5.28 +	TreeBrowser tb;
    5.29 +	long timestamp;
    5.30 +	Vertex highlighted=null;
    5.31 +
    5.32 +	public void setTreeBrowser(TreeBrowser br) {
    5.33 +		tb=br;
    5.34 +	}
    5.35 +
    5.36 +	public GraphBrowser getBrowser() { return parent; }
    5.37 +
    5.38 +	public Graph getGraph() { return gra; }
    5.39 +
    5.40 +	public Graph getOriginalGraph() { return gra2; }
    5.41 +
    5.42 +	public GraphView(Graph gr,GraphBrowser br) {
    5.43 +		gra2=gr;
    5.44 +		parent=br;
    5.45 +		gra=(Graph)(gra2.clone());
    5.46 +	}
    5.47 +
    5.48 +	public void PS(String fname,boolean printable) throws IOException {
    5.49 +		gra.PS(fname,printable);
    5.50 +	}
    5.51 +
    5.52 +	public void paintCanvas(Graphics g)
    5.53 +	{
    5.54 +		set_size(gra.max_x-gra.min_x,gra.max_y-gra.min_y);
    5.55 +		gra.draw(g);
    5.56 +	}
    5.57 +
    5.58 +	public boolean mouseMove(Event evt,int x,int y) {
    5.59 +		x+=gra.min_x;
    5.60 +		y+=gra.min_y;
    5.61 +
    5.62 +		Vertex v2=gra.vertexAt(x,y);
    5.63 +		Graphics g=getGraphics();
    5.64 +		g.translate(-gra.min_x,-gra.min_y);
    5.65 +		if (highlighted!=null) {
    5.66 +			highlighted.drawBox(g,Color.lightGray);
    5.67 +			highlighted=null;
    5.68 +		}
    5.69 +		if (v2!=v) {
    5.70 +			if (v!=null) v.removeButtons(g);
    5.71 +			if (v2!=null) v2.drawButtons(g);
    5.72 +			v=v2;
    5.73 +		}
    5.74 +		return true;
    5.75 +	}
    5.76 +
    5.77 +	/*****************************************************************/
    5.78 +	/* This method is called if successor / predecessor nodes (whose */
    5.79 +	/* numbers are stored in Vector c) of a certain node should be   */
    5.80 +        /* displayed again                                               */
    5.81 +	/*****************************************************************/
    5.82 +
    5.83 +	void uncollapse(Vector c) {
    5.84 +		collapsed.removeElement(c);
    5.85 +		collapseNodes();
    5.86 +	}
    5.87 +
    5.88 +	/*****************************************************************/
    5.89 +	/* This method is called by class TreeBrowser when directories   */
    5.90 +	/* are collapsed / uncollapsed by the user                       */
    5.91 +	/*****************************************************************/
    5.92 +
    5.93 +	public void collapseDir(Vector v) {
    5.94 +		collapsedDirs=v;
    5.95 +
    5.96 +		collapseNodes();
    5.97 +	}
    5.98 +
    5.99 +	/*****************************************************************/
   5.100 +	/*                      Inflate node again                       */
   5.101 +	/*****************************************************************/
   5.102 +
   5.103 +	public void inflateNode(Vector c) {
   5.104 +		Enumeration e1;
   5.105 +
   5.106 +		e1=collapsedDirs.elements();
   5.107 +		while (e1.hasMoreElements()) {
   5.108 +			Directory d=(Directory)(e1.nextElement());
   5.109 +			if (d.collapsed==c) {
   5.110 +				tb.selectNode(d.getNode());
   5.111 +				return;
   5.112 +			}
   5.113 +		}
   5.114 +
   5.115 +		collapsed.removeElement(c);
   5.116 +		e1=gra2.getVertices();
   5.117 +		while (e1.hasMoreElements()) {
   5.118 +			Vertex vx=(Vertex)(e1.nextElement());
   5.119 +			if (vx.getUp()==c) vx.setUp(null);
   5.120 +			if (vx.getDown()==c) vx.setDown(null);
   5.121 +		}
   5.122 +
   5.123 +		collapseNodes();
   5.124 +		relayout();
   5.125 +	}
   5.126 +
   5.127 +	public void relayout() {
   5.128 +		parent.showWaitMessage();
   5.129 +		highlighted=null;
   5.130 +		gra.layout(getGraphics());
   5.131 +		v=null;
   5.132 +		update(getGraphics());
   5.133 +		parent.showReadyMessage();
   5.134 +	}
   5.135 +
   5.136 +	public void focusToVertex(int n) {
   5.137 +		Vertex vx=gra.getVertexByNum(n);
   5.138 +		if (vx!=null) {
   5.139 +			focus_to(vx.getX()-gra.min_x,vx.getY()-gra.min_y);
   5.140 +			highlighted=vx;
   5.141 +			Graphics g=getGraphics();
   5.142 +			g.translate(-gra.min_x,-gra.min_y);
   5.143 +			vx.drawBox(g,Color.white);
   5.144 +		}
   5.145 +	}
   5.146 +
   5.147 +	/*****************************************************************/
   5.148 +	/*             Create new graph with collapsed nodes             */
   5.149 +	/*****************************************************************/
   5.150 +
   5.151 +	public void collapseNodes() {
   5.152 +		Enumeration e1=collapsed.elements();
   5.153 +		gra=(Graph)(gra2.clone());
   5.154 +
   5.155 +		while (e1.hasMoreElements()) {
   5.156 +			Vector v1=(Vector)(e1.nextElement());
   5.157 +			Vector v2=gra.decode(v1);
   5.158 +			if (!v2.isEmpty()) gra.collapse(v2,"[. . . .]",v1);
   5.159 +		}
   5.160 +
   5.161 +		e1=collapsedDirs.elements();
   5.162 +
   5.163 +		while (e1.hasMoreElements()) {
   5.164 +			Directory d=(Directory)(e1.nextElement());
   5.165 +			Vector v=gra.decode(d.getCollapsed());
   5.166 +			if (!v.isEmpty())
   5.167 +				gra.collapse(v,"["+d.getName()+"]",d.getCollapsed());
   5.168 +		}
   5.169 +	}
   5.170 +
   5.171 +	public boolean mouseDown(Event evt,int x,int y) {
   5.172 +		Vector code=null;
   5.173 +		Vertex v2;
   5.174 +		x+=gra.min_x;
   5.175 +		y+=gra.min_y;
   5.176 +
   5.177 +		if (v!=null) {
   5.178 +			int num=v.getNumber();
   5.179 +			v2=gra2.getVertexByNum(num);
   5.180 +			if (v.leftButton(x,y)) {
   5.181 +				if (v.getUp()!=null) {
   5.182 +					code=v.getUp();
   5.183 +					v2.setUp(null);
   5.184 +					v=null;
   5.185 +					uncollapse(code);
   5.186 +					relayout();
   5.187 +					focusToVertex(num);
   5.188 +				} else {
   5.189 +					Vector vs=v2.getPreds();
   5.190 +					code=gra2.encode(vs);
   5.191 +					v.setUp(code);v2.setUp(code);
   5.192 +					v=null;
   5.193 +					collapsed.insertElementAt(code,0);
   5.194 +					collapseNodes();
   5.195 +					relayout();
   5.196 +					focusToVertex(num);
   5.197 +				}
   5.198 +			} else if (v.rightButton(x,y)) {
   5.199 +				if (v.getDown()!=null) {
   5.200 +					code=v.getDown();
   5.201 +					v2.setDown(null);
   5.202 +					v=null;
   5.203 +					uncollapse(code);
   5.204 +					relayout();
   5.205 +					focusToVertex(num);
   5.206 +				} else {
   5.207 +					Vector vs=v2.getSuccs();
   5.208 +					code=gra2.encode(vs);
   5.209 +					v.setDown(code);v2.setDown(code);
   5.210 +					v=null;
   5.211 +					collapsed.insertElementAt(code,0);
   5.212 +					collapseNodes();
   5.213 +					relayout();
   5.214 +					focusToVertex(num);
   5.215 +				}
   5.216 +			} else if (v.getInflate()!=null) {
   5.217 +				inflateNode(v.getInflate());
   5.218 +				v=null;
   5.219 +			} else {
   5.220 +				if (evt.when-timestamp < 400 && !(v.getPath().equals("")))
   5.221 +					parent.viewFile(v.getPath());
   5.222 +				timestamp=evt.when;
   5.223 +			}
   5.224 +		}
   5.225 +		return true;
   5.226 +	}
   5.227 +
   5.228 +	public boolean mouseExit(Event evt,int x,int y) {
   5.229 +		Graphics g=getGraphics();
   5.230 +		g.translate(-gra.min_x,-gra.min_y);
   5.231 +		if (highlighted!=null) {
   5.232 +			highlighted.drawBox(g,Color.lightGray);
   5.233 +			highlighted=null;
   5.234 +		}
   5.235 +		if (v!=null) v.removeButtons(g);
   5.236 +		v=null;
   5.237 +		return true;
   5.238 +	}
   5.239 +}
     6.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     6.2 +++ b/lib/browser/GraphBrowser/NormalVertex.java	Wed Aug 06 00:06:47 1997 +0200
     6.3 @@ -0,0 +1,161 @@
     6.4 +/***************************************************************************
     6.5 +  Title:      GraphBrowser/NormalVertex.java
     6.6 +  ID:         $Id$
     6.7 +  Author:     Stefan Berghofer, TU Muenchen
     6.8 +  Copyright   1997  TU Muenchen
     6.9 +
    6.10 +  This class represents an ordinary vertex. It contains methods for
    6.11 +  drawing and PostScript output.
    6.12 +***************************************************************************/
    6.13 +
    6.14 +package GraphBrowser;
    6.15 +
    6.16 +import java.util.*;
    6.17 +import java.awt.*;
    6.18 +import java.io.*;
    6.19 +
    6.20 +class NormalVertex extends Vertex {
    6.21 +	String label="",path="",dir="",ID="";
    6.22 +	Vector up,down,inflate=null;
    6.23 +
    6.24 +	public Object clone() {
    6.25 +		Vertex ve=new NormalVertex(label);
    6.26 +                ve.setID(ID);
    6.27 +		ve.setNumber(getNumber());
    6.28 +		ve.setUp(getUp());ve.setDown(getDown());
    6.29 +		ve.setX(getX());ve.setY(getY());
    6.30 +		ve.setPath(getPath());
    6.31 +		return ve;
    6.32 +	}
    6.33 +
    6.34 +	/*** Constructor ***/
    6.35 +
    6.36 +	public NormalVertex(String s) { label=s; }
    6.37 +
    6.38 +	public void setInflate(Vector v) { inflate=v; }
    6.39 +
    6.40 +	public Vector getInflate() { return inflate; }
    6.41 +
    6.42 +	public Vector getUp() { return up; }
    6.43 +
    6.44 +	public void setUp(Vector v) { up=v; }
    6.45 +
    6.46 +	public Vector getDown() { return down; }
    6.47 +
    6.48 +	public void setDown(Vector v) { down=v; }
    6.49 +
    6.50 +	public String getLabel() {return label;}
    6.51 +
    6.52 +	public void setLabel(String s) {label=s;}
    6.53 +
    6.54 +	public void setID(String s) { ID=s; }
    6.55 +
    6.56 +        public String getID() { return ID; }
    6.57 +
    6.58 +	public String getPath() { return path;}
    6.59 +
    6.60 +	public void setPath(String p) { path=p; }
    6.61 +
    6.62 +	public String getDir() { return dir; }
    6.63 +
    6.64 +	public void setDir(String d) { dir=d; }
    6.65 +
    6.66 +	public int leftX() { return getX()-gra.box_width2; }
    6.67 +
    6.68 +	public int rightX() { return getX()+gra.box_width2; }
    6.69 +
    6.70 +	public void drawBox(Graphics g,Color boxColor) {
    6.71 +		FontMetrics fm=g.getFontMetrics(font);
    6.72 +		g.setFont(font);
    6.73 +		int h=fm.getAscent()+fm.getDescent();
    6.74 +
    6.75 +		g.setColor(boxColor);
    6.76 +		g.fillRect(getX()-gra.box_width2,getY(),gra.box_width,gra.box_height);
    6.77 +		g.setColor(Color.black);
    6.78 +		g.drawRect(getX()-gra.box_width2,getY(),gra.box_width,gra.box_height);
    6.79 +		if (getNumber()<0) {
    6.80 +			g.setColor(Color.red);
    6.81 +			label=label.substring(1,label.length()-1);
    6.82 +			while (label.length()>0 && fm.stringWidth("["+label+"]")>gra.box_width-8)
    6.83 +					label=label.substring(0,label.length()-1);
    6.84 +			label="["+label+"]";
    6.85 +		}
    6.86 +
    6.87 +		g.drawString(label,
    6.88 +		             (int)Math.round((gra.box_width-fm.stringWidth(label))/2.0)+getX()-gra.box_width2,
    6.89 +				fm.getAscent()+(int)Math.round((gra.box_height-h)/2.0)+getY());
    6.90 +	}
    6.91 +
    6.92 +	public void removeButtons(Graphics g) {
    6.93 +		drawBox(g,Color.lightGray);
    6.94 +	}
    6.95 +
    6.96 +	public void draw(Graphics g) {
    6.97 +		drawBox(g,Color.lightGray);
    6.98 +		g.setColor(Color.black);
    6.99 +		Enumeration e1=getChildren();
   6.100 +		while (e1.hasMoreElements()) {
   6.101 +			Vertex v=(Vertex)(e1.nextElement());
   6.102 +			if (!v.isDummy())
   6.103 +				g.drawLine(getX(),getY()+gra.box_height,v.getX(),v.getY());
   6.104 +		}
   6.105 +	}
   6.106 +
   6.107 +	public boolean contains(int x,int y) {
   6.108 +		return (x>=leftX() && x<=rightX() && y>=getY() &&
   6.109 +                        y<=getY()+gra.box_height);
   6.110 +	}
   6.111 +
   6.112 +	public boolean leftButton(int x,int y) {
   6.113 +		return contains(x,y) && x<=leftX()+gra.box_height && getParents().hasMoreElements() && getNumber()>=0;
   6.114 +	}
   6.115 +
   6.116 +	public boolean rightButton(int x,int y) {
   6.117 +		return contains(x,y) && x>=rightX()-gra.box_height && getChildren().hasMoreElements() && getNumber()>=0;
   6.118 +	}
   6.119 +
   6.120 +	public void drawButtons(Graphics g) {
   6.121 +		if (getNumber()<0) return;
   6.122 +
   6.123 +		int l=gra.box_height*2/3,d=gra.box_height/6;
   6.124 +		int up_x[] = { leftX()+d , leftX()+d+l/2 , leftX()+d+l };
   6.125 +		int up_y[] = { getY()+d+l , getY()+d , getY()+d+l };
   6.126 +		int down_x[] = { rightX()-d-l , rightX()-d-l/2 , rightX()-d };
   6.127 +		int down_y[] = { getY()+d , getY()+d+l , getY()+d };
   6.128 +
   6.129 +		if (getParents().hasMoreElements()) {
   6.130 +			g.setColor(Color.gray);
   6.131 +			g.fillRect(leftX()+1,getY()+1,gra.box_height-1,gra.box_height-1);
   6.132 +			g.setColor(getUp()!=null ? Color.red : Color.green);
   6.133 +			g.fillPolygon(up_x,up_y,3);
   6.134 +		}
   6.135 +		if (getChildren().hasMoreElements()) {
   6.136 +			g.setColor(Color.gray);
   6.137 +			g.fillRect(rightX()+1-gra.box_height,getY()+1,gra.box_height,gra.box_height-1);
   6.138 +			g.setColor(getDown()!=null ? Color.red : Color.green);
   6.139 +			g.fillPolygon(down_x,down_y,3);
   6.140 +		}
   6.141 +		g.setColor(Color.black);
   6.142 +	}
   6.143 +
   6.144 +	public void PS(PrintStream p) {
   6.145 +		p.print(leftX()+" "+getY()+" "+gra.box_width+" "+
   6.146 +		        gra.box_height+" (");
   6.147 +		for (int i=0;i<label.length();i++)
   6.148 +		{
   6.149 +			if (("()\\").indexOf(label.charAt(i))>=0)
   6.150 +				p.print("\\");
   6.151 +			p.print(label.charAt(i));
   6.152 +		}
   6.153 +		p.println(") b");
   6.154 +
   6.155 +		Enumeration e1=getChildren();
   6.156 +		while (e1.hasMoreElements()) {
   6.157 +			Vertex v=(Vertex)(e1.nextElement());
   6.158 +			if (!v.isDummy())
   6.159 +				p.println("n "+getX()+" "+(getY()+gra.box_height)+
   6.160 +				" m "+v.getX()+" "+v.getY()+" l s");
   6.161 +		}
   6.162 +	}	
   6.163 +}
   6.164 +		
     7.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     7.2 +++ b/lib/browser/GraphBrowser/Region.java	Wed Aug 06 00:06:47 1997 +0200
     7.3 @@ -0,0 +1,90 @@
     7.4 +/***************************************************************************
     7.5 +  Title:      GraphBrowser/Region.java
     7.6 +  ID:         $Id$
     7.7 +  Author:     Stefan Berghofer, TU Muenchen
     7.8 +  Copyright   1997  TU Muenchen
     7.9 +
    7.10 +  This is an auxiliary class which is used by the layout algorithm when
    7.11 +  calculating coordinates with the "pendulum method". A "region" is a
    7.12 +  group of nodes which "stick together".
    7.13 +***************************************************************************/
    7.14 +
    7.15 +package GraphBrowser;
    7.16 +
    7.17 +import java.util.*;
    7.18 +
    7.19 +class Region {
    7.20 +	Vector vertices=new Vector(10,10);
    7.21 +	Graph gra;
    7.22 +
    7.23 +	public Region(Graph g) { gra=g; }
    7.24 +
    7.25 +	public void addVertex(Vertex v) {
    7.26 +		vertices.addElement(v);
    7.27 +	}
    7.28 +
    7.29 +	public Enumeration getVertices() {
    7.30 +		return vertices.elements();
    7.31 +	}
    7.32 +
    7.33 +	public int pred_deflection() {
    7.34 +		float d1=0;
    7.35 +		int n=0;
    7.36 +		Enumeration e1=vertices.elements();
    7.37 +		while (e1.hasMoreElements()) {
    7.38 +			float d2=0;
    7.39 +			int p=0;
    7.40 +			n++;
    7.41 +			Vertex v=(Vertex)(e1.nextElement());
    7.42 +			Enumeration e2=v.getParents();
    7.43 +			while (e2.hasMoreElements()) {
    7.44 +				p++;
    7.45 +				d2+=((Vertex)(e2.nextElement())).getX()-v.getX();
    7.46 +			}
    7.47 +			if (p>0) d1+=d2/p;
    7.48 +		}
    7.49 +		return (int)(Math.round(d1/n));
    7.50 +	}
    7.51 +
    7.52 +	public int succ_deflection() {
    7.53 +		float d1=0;
    7.54 +		int n=0;
    7.55 +		Enumeration e1=vertices.elements();
    7.56 +		while (e1.hasMoreElements()) {
    7.57 +			float d2=0;
    7.58 +			int p=0;
    7.59 +			n++;
    7.60 +			Vertex v=(Vertex)(e1.nextElement());
    7.61 +			Enumeration e2=v.getChildren();
    7.62 +			while (e2.hasMoreElements()) {
    7.63 +				p++;
    7.64 +				d2+=((Vertex)(e2.nextElement())).getX()-v.getX();
    7.65 +			}
    7.66 +			if (p>0) d1+=d2/p;
    7.67 +		}
    7.68 +		return (int)(Math.round(d1/n));
    7.69 +	}
    7.70 +
    7.71 +	public void move(int x) {
    7.72 +		Enumeration e1=vertices.elements();
    7.73 +		while (e1.hasMoreElements()) {
    7.74 +			Vertex v=(Vertex)(e1.nextElement());
    7.75 +			v.setX(v.getX()+x);
    7.76 +		}
    7.77 +	}
    7.78 +
    7.79 +	public void combine(Region r2) {
    7.80 +		Enumeration e1=r2.getVertices();
    7.81 +		while (e1.hasMoreElements()) addVertex((Vertex)(e1.nextElement()));
    7.82 +	}
    7.83 +
    7.84 +	public int spaceBetween(Region r2) {
    7.85 +		return ((Vertex)(r2.getVertices().nextElement())).leftX()-
    7.86 +			((Vertex)(vertices.lastElement())).rightX()-
    7.87 +			gra.box_hspace+gra.box_width;
    7.88 +	}
    7.89 +
    7.90 +	public boolean touching(Region r2) {
    7.91 +		return spaceBetween(r2)==0;
    7.92 +	}
    7.93 +}
     8.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     8.2 +++ b/lib/browser/GraphBrowser/Spline.java	Wed Aug 06 00:06:47 1997 +0200
     8.3 @@ -0,0 +1,121 @@
     8.4 +/***************************************************************************
     8.5 +  Title:      GraphBrowser/Spline.java
     8.6 +  ID:         $Id$
     8.7 +  Author:     Stefan Berghofer, TU Muenchen
     8.8 +  Copyright   1997  TU Muenchen
     8.9 +
    8.10 +  This class is used for drawing spline curves (which are not yet
    8.11 +  supported by the Java AWT).
    8.12 +***************************************************************************/
    8.13 +
    8.14 +package GraphBrowser;
    8.15 +
    8.16 +import java.awt.*;
    8.17 +import java.util.*;
    8.18 +import java.io.*;
    8.19 +
    8.20 +class SplineSection {
    8.21 +
    8.22 +	/*** Section of a spline function ***/
    8.23 +
    8.24 +	double x_b,x_c,x_d;
    8.25 +	double y_b,y_c,y_d;
    8.26 +	int dx,dy;
    8.27 +
    8.28 +	public SplineSection(double xb,double xc,double xd,
    8.29 +		double yb,double yc,double yd,int dx2,int dy2) {
    8.30 +		x_b=xb;x_c=xc;x_d=xd;
    8.31 +		y_b=yb;y_c=yc;y_d=yd;
    8.32 +		dx=dx2;dy=dy2;
    8.33 +	}
    8.34 +
    8.35 +	public Point draw(Graphics g,Point s) {
    8.36 +		double m;
    8.37 +		int s_x,s_y,e_x=0,e_y=0;
    8.38 +		int x,y;
    8.39 +
    8.40 +		s_x=s.x;s_y=s.y;
    8.41 +		if (dx>=dy) {
    8.42 +			if (dx==0) return s;
    8.43 +			m=1/((double)dx);
    8.44 +			for (x=0;x<dx;x++) {
    8.45 +				e_x=(int)(Math.round((x_b*x*m+x_c)*x*m+x_d));
    8.46 +				e_y=(int)(Math.round((y_b*x*m+y_c)*x*m+y_d));
    8.47 +				g.drawLine(s_x,s_y,e_x,e_y);
    8.48 +				s_x=e_x;s_y=e_y;
    8.49 +			}
    8.50 +		} else {
    8.51 +			m=1/((double)dy);
    8.52 +			for (y=0;y<dy;y++) {
    8.53 +				e_x=(int)(Math.round((x_b*y*m+x_c)*y*m+x_d));
    8.54 +				e_y=(int)(Math.round((y_b*y*m+y_c)*y*m+y_d));
    8.55 +				g.drawLine(s_x,s_y,e_x,e_y);
    8.56 +				s_x=e_x;s_y=e_y;
    8.57 +			}
    8.58 +		}
    8.59 +		return new Point(e_x,e_y);
    8.60 +	}
    8.61 +}
    8.62 +
    8.63 +public class Spline {
    8.64 +
    8.65 +	Vector sections;
    8.66 +	Vector points;
    8.67 +	Point start,end;
    8.68 +
    8.69 +	public Spline(Vector pts) {
    8.70 +		int i;
    8.71 +		double d0,d1,d2,d3;
    8.72 +		Point p0,p1,p2;
    8.73 +		SplineSection s;
    8.74 +		
    8.75 +		start=(Point)(pts.firstElement());
    8.76 +		end=(Point)(pts.lastElement());
    8.77 +
    8.78 +		sections=new Vector(10,10);
    8.79 +		for (i=1;i<=pts.size()-4;i+=3) {
    8.80 +			p0=(Point)(pts.elementAt(i));
    8.81 +			p1=(Point)(pts.elementAt(i+1));
    8.82 +			p2=(Point)(pts.elementAt(i+2));
    8.83 +			s=new SplineSection(
    8.84 +				(double)(p2.x-2*p1.x+p0.x),
    8.85 +				2.0*(p1.x-p0.x),
    8.86 +				(double)(p0.x),
    8.87 +
    8.88 +				(double)(p2.y-2*p1.y+p0.y),
    8.89 +				2.0*(p1.y-p0.y),
    8.90 +				(double)(p0.y),
    8.91 +
    8.92 +				Math.abs(p2.x-p0.x),
    8.93 +				Math.abs(p2.y-p0.y)
    8.94 +			);
    8.95 +
    8.96 +			sections.addElement(s);
    8.97 +		}
    8.98 +		points=pts;
    8.99 +	}
   8.100 +
   8.101 +	public void draw(Graphics g) {
   8.102 +		Enumeration e1=sections.elements();
   8.103 +		Point p=start;
   8.104 +
   8.105 +		while (e1.hasMoreElements())
   8.106 +			p=((SplineSection)(e1.nextElement())).draw(g,p);
   8.107 +		g.drawLine(p.x,p.y,end.x,end.y);
   8.108 +	}
   8.109 +
   8.110 +	public void PS(PrintStream p) {
   8.111 +		Point p0,p1,p2;
   8.112 +		int i;
   8.113 +
   8.114 +		p.println("n "+start.x+" "+start.y+" m");
   8.115 +		for (i=1;i<=points.size()-4;i+=3) {
   8.116 +			p0=(Point)(points.elementAt(i));
   8.117 +			p1=(Point)(points.elementAt(i+1));
   8.118 +			p2=(Point)(points.elementAt(i+2));
   8.119 +			p.println(p0.x+" "+p0.y+" l");
   8.120 +			p.println(p0.x+" "+p0.y+" "+p1.x+" "+p1.y+" "+p2.x+" "+p2.y+" c");
   8.121 +		}
   8.122 +		p.println(end.x+" "+end.y+" l s");
   8.123 +	}
   8.124 +}
     9.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     9.2 +++ b/lib/browser/GraphBrowser/TreeBrowser.java	Wed Aug 06 00:06:47 1997 +0200
     9.3 @@ -0,0 +1,70 @@
     9.4 +/***************************************************************************
     9.5 +  Title:      GraphBrowser/TreeBrowser.java
     9.6 +  ID:         $Id$
     9.7 +  Author:     Stefan Berghofer, TU Muenchen
     9.8 +  Copyright   1997  TU Muenchen
     9.9 +
    9.10 +  This class defines the browser window which is used to display directory
    9.11 +  trees. It contains methods for handling events.
    9.12 +***************************************************************************/
    9.13 +
    9.14 +package GraphBrowser;
    9.15 +
    9.16 +import java.awt.*;
    9.17 +import awtUtilities.ScrollCanvas;
    9.18 +import java.util.*;
    9.19 +
    9.20 +
    9.21 +public class TreeBrowser extends ScrollCanvas
    9.22 +{
    9.23 +	TreeNode t;
    9.24 +	TreeNode selected;
    9.25 +	GraphView gv;
    9.26 +	long timestamp;
    9.27 +
    9.28 +	public TreeBrowser(TreeNode tn,GraphView gr) {
    9.29 +		t=tn;gv=gr;
    9.30 +	}
    9.31 +
    9.32 +	public boolean mouseDown(Event e,int x,int y)
    9.33 +	{
    9.34 +		TreeNode l=t.lookup(y);
    9.35 +
    9.36 +		if (l!=null)
    9.37 +		{
    9.38 +			if (l.select()) {
    9.39 +				Vector v=new Vector(10,10);
    9.40 +				t.collapsedDirectories(v);
    9.41 +				gv.collapseDir(v);
    9.42 +				gv.relayout();
    9.43 +			} else {
    9.44 +				Vertex vx=gv.getGraph().getVertexByNum(l.getNumber());
    9.45 +				gv.focusToVertex(l.getNumber());
    9.46 +				vx=gv.getOriginalGraph().getVertexByNum(l.getNumber());
    9.47 +				if (e.when-timestamp < 400 && !(vx.getPath().equals("")))
    9.48 +					gv.getBrowser().viewFile(vx.getPath());
    9.49 +				timestamp=e.when;
    9.50 +
    9.51 +			}
    9.52 +			selected=l;repaint();
    9.53 +			
    9.54 +		}
    9.55 +		return true;
    9.56 +	}
    9.57 +
    9.58 +	public void selectNode(TreeNode nd) {
    9.59 +		Vector v=new Vector(10,10);
    9.60 +		nd.select();
    9.61 +		t.collapsedDirectories(v);
    9.62 +		gv.collapseDir(v);
    9.63 +		gv.relayout();
    9.64 +		selected=nd;repaint();
    9.65 +	}
    9.66 +
    9.67 +	public void paintCanvas(Graphics g)
    9.68 +	{
    9.69 +		Dimension d=t.draw(g,5,5,selected);
    9.70 +		set_size(5+d.width,5+d.height);
    9.71 +	}
    9.72 +}
    9.73 +
    10.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    10.2 +++ b/lib/browser/GraphBrowser/TreeNode.java	Wed Aug 06 00:06:47 1997 +0200
    10.3 @@ -0,0 +1,187 @@
    10.4 +/***************************************************************************
    10.5 +  Title:      GraphBrowser/TreeNode.java
    10.6 +  ID:         $Id$
    10.7 +  Author:     Stefan Berghofer, TU Muenchen
    10.8 +  Copyright   1997  TU Muenchen
    10.9 +
   10.10 +  This class contains methods for storing and manipulating directory
   10.11 +  trees (e.g. collapsing / uncollapsing directory branches).
   10.12 +***************************************************************************/
   10.13 +
   10.14 +package GraphBrowser;
   10.15 +
   10.16 +import java.awt.*;
   10.17 +import java.util.*;
   10.18 +
   10.19 +class Directory {
   10.20 +	TreeNode node;
   10.21 +	String name;
   10.22 +	Vector collapsed;
   10.23 +
   10.24 +	public Directory(TreeNode nd,String n,Vector col) {
   10.25 +		collapsed=col;
   10.26 +		name=n;
   10.27 +		node=nd;
   10.28 +	}
   10.29 +
   10.30 +	public TreeNode getNode() { return node; }
   10.31 +
   10.32 +	public String getName() { return name; }
   10.33 +
   10.34 +	public Vector getCollapsed() { return collapsed; }
   10.35 +}
   10.36 +
   10.37 +public class TreeNode
   10.38 +{
   10.39 +	static Font f=new Font("Helvetica",Font.PLAIN,15);
   10.40 +	int starty,endy,number;
   10.41 +	String name,path;
   10.42 +
   10.43 +	Vector leaves=new Vector(10,10);
   10.44 +	boolean unfold=false;
   10.45 +
   10.46 +	public void insertNode(String n,String d,String p,int num,boolean u) {
   10.47 +		if (d.length()==0) {
   10.48 +			leaves.addElement(new TreeNode(n,p,num));
   10.49 +			unfold=unfold||u;
   10.50 +		} else {
   10.51 +			unfold=unfold||u;
   10.52 +			String str1,str2;
   10.53 +			if (d.indexOf('/')<0) {
   10.54 +				str1=d;str2="";
   10.55 +			} else {
   10.56 +				str1=d.substring(0,d.indexOf('/'));
   10.57 +				str2=d.substring(d.indexOf('/')+1);
   10.58 +			}
   10.59 +
   10.60 +			Enumeration e1=leaves.elements();
   10.61 +			TreeNode nd=null;
   10.62 +
   10.63 +			while (e1.hasMoreElements()) {
   10.64 +				TreeNode nd2=(TreeNode)(e1.nextElement());
   10.65 +				if (nd2.name.equals(str1)) {
   10.66 +					nd=nd2;break;
   10.67 +				}
   10.68 +			}
   10.69 +			if (nd==null) {
   10.70 +				nd=new TreeNode(str1,"",-1);
   10.71 +				leaves.addElement(nd);
   10.72 +			}
   10.73 +			nd.insertNode(n,str2,p,num,u);
   10.74 +		}
   10.75 +	}
   10.76 +
   10.77 +	public TreeNode(String n,String p,int num) {
   10.78 +		name=n;
   10.79 +		path=p;
   10.80 +		number=num;
   10.81 +	}
   10.82 +
   10.83 +	public TreeNode(String n,String p,int num,boolean u) {
   10.84 +		this(n,p,num);
   10.85 +		unfold=u;
   10.86 +	}	
   10.87 +
   10.88 +	public int getNumber() { return number; }
   10.89 +
   10.90 +	public TreeNode lookup(int y)
   10.91 +	{
   10.92 +		if (y>=starty && y<endy) return this;
   10.93 +		else
   10.94 +		if (unfold)
   10.95 +			for (int i=0;i<leaves.size();i++)
   10.96 +			{
   10.97 +				TreeNode t=((TreeNode)leaves.elementAt(i)).lookup(y);
   10.98 +				if (t!=null) return t;
   10.99 +			}
  10.100 +		return null;
  10.101 +	}
  10.102 +
  10.103 +	public boolean select()
  10.104 +	{
  10.105 +		if (!leaves.isEmpty()) {
  10.106 +			if (unfold) collapse();
  10.107 +			else unfold=true;
  10.108 +			return true;
  10.109 +		}
  10.110 +		return false; 
  10.111 +	}
  10.112 +
  10.113 +	public void collapse()
  10.114 +	{
  10.115 +		unfold=false;
  10.116 +		/*
  10.117 +		for(int i=0;i<leaves.size();i++)
  10.118 +			((Tree)leaves.elementAt(i)).collapse();
  10.119 +		*/
  10.120 +	}
  10.121 +
  10.122 +	void collapsedNodes(Vector v) {
  10.123 +		if (number>=0) v.addElement(new Integer(number));
  10.124 +		Enumeration e1=leaves.elements();
  10.125 +		while (e1.hasMoreElements())
  10.126 +			((TreeNode)(e1.nextElement())).collapsedNodes(v);
  10.127 +	}
  10.128 +
  10.129 +	public void collapsedDirectories(Vector v) {
  10.130 +		if (!unfold) {
  10.131 +			Vector v2=new Vector(10,10);
  10.132 +			v.addElement(new Directory(this,name,v2));
  10.133 +			collapsedNodes(v2);
  10.134 +		} else {
  10.135 +			Enumeration e1=leaves.elements();
  10.136 +			while (e1.hasMoreElements()) {
  10.137 +				TreeNode tn=(TreeNode)(e1.nextElement());
  10.138 +				if (!tn.leaves.isEmpty())
  10.139 +					tn.collapsedDirectories(v);
  10.140 +			}
  10.141 +		}
  10.142 +	}
  10.143 +
  10.144 +	public Dimension draw(Graphics g,int x,int y,TreeNode t)
  10.145 +	{
  10.146 +		FontMetrics fm=g.getFontMetrics(f);
  10.147 +		g.setFont(f);
  10.148 +		int h=fm.getHeight();
  10.149 +		int down_x[]={x,x+h,x+(int)(h/2)};
  10.150 +		int down_y[]={y,y,y+h};
  10.151 +		int right_x[]={x,x+h,x};
  10.152 +		int right_y[]={y,y+(int)(h/2),y+h};
  10.153 +		int dx=0;
  10.154 +
  10.155 +		if (unfold)
  10.156 +		{
  10.157 +			g.setColor(Color.green);
  10.158 +			g.fillPolygon(down_x,down_y,3);
  10.159 +			g.setColor(Color.black);
  10.160 +			g.drawString(name,x+h+10,y+fm.getAscent());
  10.161 +			starty=y;endy=y+h;
  10.162 +			dx=Math.max(dx,x+h+10+fm.stringWidth(name));
  10.163 +			y+=h+5;
  10.164 +			for(int i=0;i<leaves.size();i++)
  10.165 +			{
  10.166 +				Dimension d=((TreeNode)leaves.elementAt(i)).draw(g,x+h+10,y,t);
  10.167 +				y=d.height;
  10.168 +				dx=Math.max(dx,d.width);
  10.169 +			}
  10.170 +		}
  10.171 +		else
  10.172 +		{
  10.173 +			g.setColor(leaves.isEmpty() ? Color.blue : Color.red);
  10.174 +			g.fillPolygon(right_x,right_y,3);
  10.175 +			if (this==t && leaves.isEmpty())
  10.176 +			{
  10.177 +				g.setColor(Color.white);
  10.178 +				g.fillRect(x+h+10,y,fm.stringWidth(name),h);
  10.179 +			}
  10.180 +			g.setColor(Color.black);
  10.181 +			g.drawString(name,x+h+10,y+fm.getAscent());
  10.182 +			starty=y;endy=y+h;
  10.183 +			dx=Math.max(dx,x+h+10+fm.stringWidth(name));
  10.184 +			y+=h+5;
  10.185 +		}
  10.186 +		return new Dimension(dx,y);
  10.187 +	}
  10.188 +}
  10.189 +
  10.190 +
    11.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    11.2 +++ b/lib/browser/GraphBrowser/Vertex.java	Wed Aug 06 00:06:47 1997 +0200
    11.3 @@ -0,0 +1,206 @@
    11.4 +/***************************************************************************
    11.5 +  Title:      GraphBrowser/Vertex.java
    11.6 +  ID:         $Id$
    11.7 +  Author:     Stefan Berghofer, TU Muenchen
    11.8 +  Copyright   1997  TU Muenchen
    11.9 +
   11.10 +  This class contains attributes and methods common to all kinds of
   11.11 +  vertices (e.g. coordinates, successors, predecessors).
   11.12 +***************************************************************************/
   11.13 +
   11.14 +package GraphBrowser;
   11.15 +
   11.16 +import java.util.*;
   11.17 +import java.awt.*;
   11.18 +import java.io.*;
   11.19 +
   11.20 +abstract class Vertex {
   11.21 +	protected static final Font font=new Font("Helvetica",Font.PLAIN,12);
   11.22 +
   11.23 +	Vector children=new Vector(10,10);
   11.24 +	Vector parents=new Vector(10,10);
   11.25 +	int degree=0;
   11.26 +	int number=-1;
   11.27 +	double weight=0;
   11.28 +	int x,y;
   11.29 +	Graph gra;
   11.30 +
   11.31 +	public abstract Object clone();
   11.32 +
   11.33 +	public void setGraph(Graph g) { gra=g; }
   11.34 +
   11.35 +	public int countChildren() { return children.size(); }
   11.36 +
   11.37 +	/** getInflate returns a vector of vertices which get **/
   11.38 +	/** inflated again if the user clicks on this vertex  **/
   11.39 +
   11.40 +	public void setInflate(Vector v) {}
   11.41 +
   11.42 +	public Vector getInflate() { return null; }
   11.43 +
   11.44 +	/** getUp returns a vector of vertices which get inflated   **/
   11.45 +	/** again, if the user clicks on this vertex's upward arrow **/
   11.46 +
   11.47 +	public Vector getUp() { return null; }
   11.48 +
   11.49 +	public void setUp(Vector v) {}
   11.50 +
   11.51 +	/** getUp returns a vector of vertices which get inflated     **/
   11.52 +	/** again, if the user clicks on this vertex's downward arrow **/
   11.53 +
   11.54 +	public Vector getDown() { return null; }
   11.55 +
   11.56 +	public void setDown(Vector v) {}
   11.57 +
   11.58 +	/** internal number, for decoding / encoding etc. **/
   11.59 +
   11.60 +	public int getNumber() { return number; }
   11.61 +
   11.62 +	public void setNumber(int n) { number=n; }
   11.63 +
   11.64 +	public String getLabel() {return "";}
   11.65 +
   11.66 +	public void setLabel(String s) {}
   11.67 +
   11.68 +	/** unique identifier **/
   11.69 +
   11.70 +	public String getID() {return "";}
   11.71 +
   11.72 +	public void setID(String s) {}
   11.73 +
   11.74 +	public Dimension getLabelSize(Graphics g) {
   11.75 +		FontMetrics fm=g.getFontMetrics(font);
   11.76 +		
   11.77 +		return new Dimension(
   11.78 +		        Math.max(fm.stringWidth("[. . . .]"),fm.stringWidth(getLabel())),
   11.79 +			fm.getAscent()+fm.getDescent());
   11.80 +	}
   11.81 +		
   11.82 +	public String getPath() { return "";}
   11.83 +
   11.84 +	public void setPath(String p) {}
   11.85 +
   11.86 +	public String getDir() { return ""; }
   11.87 +
   11.88 +	public void setDir(String d) {}
   11.89 +
   11.90 +	public void setWeight(double w) {weight=w;}
   11.91 +
   11.92 +	public double getWeight() {return weight;}
   11.93 +
   11.94 +	public void setDegree(int d) { degree=d; }
   11.95 +
   11.96 +	public int getDegree() { return degree; }
   11.97 +
   11.98 +	public boolean isDummy() { return false; }
   11.99 +
  11.100 +	public Enumeration getChildren() {
  11.101 +		return ((Vector)(children.clone())).elements();
  11.102 +	}
  11.103 +
  11.104 +	public void addChild(Vertex v) {
  11.105 +		children.addElement(v);
  11.106 +		v.parents.addElement(this);
  11.107 +	}
  11.108 +
  11.109 +	public void removeChild(Vertex v) {
  11.110 +		children.removeElement(v);
  11.111 +		v.parents.removeElement(this);
  11.112 +	}
  11.113 +
  11.114 +	public boolean isChild(Vertex v) {
  11.115 +		return children.indexOf(v)>=0;
  11.116 +	}
  11.117 +
  11.118 +	public boolean isParent(Vertex v) {
  11.119 +		return parents.indexOf(v)>=0;
  11.120 +	}
  11.121 +
  11.122 +	public Enumeration getParents() {
  11.123 +		return ((Vector)(parents.clone())).elements();
  11.124 +	}
  11.125 +
  11.126 +	public void addParent(Vertex v) {
  11.127 +		parents.addElement(v);
  11.128 +		v.children.addElement(this);
  11.129 +	}
  11.130 +
  11.131 +	public void removeParent(Vertex v) {
  11.132 +		parents.removeElement(v);
  11.133 +		v.children.removeElement(this);
  11.134 +	}
  11.135 +
  11.136 +	/********************************************************************/
  11.137 +	/*                   get all predecessor vertices                   */
  11.138 +	/********************************************************************/
  11.139 +
  11.140 +	public Vector getPreds() {
  11.141 +		Vector v1=new Vector(10,10);
  11.142 +		Vertex vx1,vx2;
  11.143 +		Enumeration e1,e2;
  11.144 +
  11.145 +		e1=getParents();
  11.146 +		while (e1.hasMoreElements()) {
  11.147 +			vx1=(Vertex)(e1.nextElement());
  11.148 +			if (v1.indexOf(vx1)<0) v1.addElement(vx1);
  11.149 +			e2=vx1.getPreds().elements();
  11.150 +			while (e2.hasMoreElements()) {
  11.151 +				vx2=(Vertex)(e2.nextElement());
  11.152 +				if (v1.indexOf(vx2)<0) v1.addElement(vx2);			
  11.153 +			}
  11.154 +		}
  11.155 +
  11.156 +		return v1;
  11.157 +	}
  11.158 +
  11.159 +	/********************************************************************/
  11.160 +	/*                     get all successor vertices                   */
  11.161 +	/********************************************************************/
  11.162 +
  11.163 +	public Vector getSuccs() {
  11.164 +		Vector v1=new Vector(10,10);
  11.165 +		Vertex vx1,vx2;
  11.166 +		Enumeration e1,e2;
  11.167 +
  11.168 +		e1=getChildren();
  11.169 +		while (e1.hasMoreElements()) {
  11.170 +			vx1=(Vertex)(e1.nextElement());
  11.171 +			if (v1.indexOf(vx1)<0) v1.addElement(vx1);
  11.172 +			e2=vx1.getSuccs().elements();
  11.173 +			while (e2.hasMoreElements()) {
  11.174 +				vx2=(Vertex)(e2.nextElement());
  11.175 +				if (v1.indexOf(vx2)<0) v1.addElement(vx2);			
  11.176 +			}
  11.177 +		}
  11.178 +
  11.179 +		return v1;
  11.180 +	}
  11.181 +
  11.182 +	public void setX(int x) {this.x=x;}
  11.183 +
  11.184 +	public void setY(int y) {this.y=y;}
  11.185 +
  11.186 +	public int getX() {return x;}
  11.187 +
  11.188 +	public int getY() {return y;}
  11.189 +
  11.190 +	public abstract int leftX();
  11.191 +
  11.192 +	public abstract int rightX();
  11.193 +
  11.194 +	public abstract void draw(Graphics g);
  11.195 +
  11.196 +	public void drawButtons(Graphics g) {}
  11.197 +
  11.198 +	public void drawBox(Graphics g,Color boxColor) {}
  11.199 +
  11.200 +	public void removeButtons(Graphics g) {}
  11.201 +
  11.202 +	public boolean contains(int x,int y) { return false; }
  11.203 +
  11.204 +	public boolean leftButton(int x,int y) { return false; }
  11.205 +
  11.206 +	public boolean rightButton(int x,int y) { return false; }
  11.207 +
  11.208 +	public void PS(PrintStream p) {}
  11.209 +}
    12.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    12.2 +++ b/lib/browser/awtUtilities/Border.java	Wed Aug 06 00:06:47 1997 +0200
    12.3 @@ -0,0 +1,41 @@
    12.4 +/***************************************************************************
    12.5 +  Title:      awtUtilities/Border.java
    12.6 +  ID:         $Id$
    12.7 +  Author:     Stefan Berghofer, TU Muenchen
    12.8 +  Copyright   1997  TU Muenchen
    12.9 +
   12.10 +  This class defines a nice 3D border.
   12.11 +***************************************************************************/
   12.12 +
   12.13 +package awtUtilities;
   12.14 +
   12.15 +import java.awt.*;
   12.16 +
   12.17 +public class Border extends Panel {
   12.18 +	int bs;
   12.19 +
   12.20 +	public Insets insets() {
   12.21 +		return new Insets(bs*3/2,bs*3/2,bs*3/2,bs*3/2);
   12.22 +	}
   12.23 +
   12.24 +	public Border(Component comp,int s) {
   12.25 +		setLayout(new GridLayout(1,1));
   12.26 +		add(comp);
   12.27 +		bs=s;
   12.28 +	}
   12.29 +
   12.30 +	public void paint(Graphics g) {
   12.31 +		int w=size().width;
   12.32 +		int h=size().height;
   12.33 +		int x1[]={0,bs,w-bs,w}, y1[]={0,bs,bs,0};
   12.34 +		int x2[]={w,w-bs,w-bs,w}, y2[]={0,bs,h-bs,h};
   12.35 +		int y3[]={h,h-bs,h-bs,h};
   12.36 +
   12.37 +		g.setColor(new Color(224,224,224));
   12.38 +		g.fillPolygon(y1,y2,4);
   12.39 +		g.fillPolygon(x1,y1,4);
   12.40 +		g.setColor(Color.gray);
   12.41 +		g.fillPolygon(x2,y2,4);
   12.42 +		g.fillPolygon(x1,y3,4);
   12.43 +	}
   12.44 +}
    13.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    13.2 +++ b/lib/browser/awtUtilities/MessageDialog.java	Wed Aug 06 00:06:47 1997 +0200
    13.3 @@ -0,0 +1,54 @@
    13.4 +/***************************************************************************
    13.5 +  Title:      awtUtilities/MessageDialog.java
    13.6 +  ID:         $Id$
    13.7 +  Author:     Stefan Berghofer, TU Muenchen
    13.8 +  Copyright   1997  TU Muenchen
    13.9 +
   13.10 +  This class defines a dialog window for displaying messages and buttons.
   13.11 +***************************************************************************/
   13.12 +
   13.13 +package awtUtilities;
   13.14 +
   13.15 +import java.awt.*;
   13.16 +
   13.17 +public class MessageDialog extends Dialog {
   13.18 +	String txt;
   13.19 +
   13.20 +	public String getText() { return txt; }
   13.21 +
   13.22 +	public boolean action(Event evt, Object arg) {
   13.23 +		if (evt.target instanceof Button) {
   13.24 +			txt=(String)arg;
   13.25 +			hide();
   13.26 +			return true;
   13.27 +		} else return false;
   13.28 +	}
   13.29 +
   13.30 +	public MessageDialog(Frame parent,String title,String text,String []buttons) {
   13.31 +		super(parent,title,true);
   13.32 +		int i;
   13.33 +		Panel p1=new Panel(),p2=new Panel();
   13.34 +		p1.setLayout(new FlowLayout(FlowLayout.CENTER,0,0));
   13.35 +		p2.setLayout(new FlowLayout());
   13.36 +		setFont(new Font("Helvetica", Font.PLAIN, 14));
   13.37 +		setLayout(new GridLayout(2,1));
   13.38 +
   13.39 +		while (true) {
   13.40 +			int pos=text.indexOf(' ');
   13.41 +			if (pos<0) {
   13.42 +				p1.add(new Label(text));
   13.43 +				break;
   13.44 +			} else {
   13.45 +				p1.add(new Label(text.substring(0,pos)));
   13.46 +				if (pos+1==text.length())
   13.47 +					break;
   13.48 +				else
   13.49 +					text=text.substring(pos+1);
   13.50 +			}
   13.51 +		}
   13.52 +
   13.53 +		add(p1);add(p2);
   13.54 +		for (i=0;i<buttons.length;i++)
   13.55 +			p2.add(new Button(buttons[i]));
   13.56 +	}
   13.57 +}
    14.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    14.2 +++ b/lib/browser/awtUtilities/ScrollCanvas.java	Wed Aug 06 00:06:47 1997 +0200
    14.3 @@ -0,0 +1,169 @@
    14.4 +/***************************************************************************
    14.5 +  Title:      awtUtilities/ScrollCanvas.java
    14.6 +  ID:         $Id$
    14.7 +  Author:     Stefan Berghofer, TU Muenchen
    14.8 +  Copyright   1997  TU Muenchen
    14.9 +
   14.10 +  This class contains defines a window with scrollbars, which is not
   14.11 +  supported by the 1.0.2 version of the JDK. To use this class, simply
   14.12 +  derive your own class from it and overwrite the paintCanvas method.
   14.13 +  When a repaint event occurs, ScrollCanvas automatically calls the
   14.14 +  paintCanvas method. The user doesn't have to take care of transposing
   14.15 +  mouse or graphics coordinates.
   14.16 +  Note: In later versions of the JDK, a ScrollPane class will be provided,
   14.17 +  which can be used instead.
   14.18 +***************************************************************************/
   14.19 +
   14.20 +package awtUtilities;
   14.21 +
   14.22 +import java.awt.*;
   14.23 +
   14.24 +class DummyCanvas extends Canvas {
   14.25 +	ScrollCanvas parent;
   14.26 +
   14.27 +	public DummyCanvas(ScrollCanvas p) {
   14.28 +		parent=p;
   14.29 +	}
   14.30 +
   14.31 +	public void paint(Graphics g) {
   14.32 +		parent.paint(g);
   14.33 +	}
   14.34 +
   14.35 +	public void update(Graphics g) {
   14.36 +		parent.update(g);
   14.37 +	}
   14.38 +}
   14.39 +
   14.40 +public class ScrollCanvas extends Panel
   14.41 +{
   14.42 +	Scrollbar scrollv,scrollh;
   14.43 +	Canvas can;
   14.44 +	Image img=null;
   14.45 +	int offset_x=0,offset_y=0;
   14.46 +	int size_x=100,size_y=100;
   14.47 +	int old_x=0,old_y=0;
   14.48 +
   14.49 +	public boolean handleEvent(Event evt)
   14.50 +	{
   14.51 +		evt.x+=offset_x;
   14.52 +		evt.y+=offset_y;
   14.53 +		if (evt.target instanceof Scrollbar)
   14.54 +		{
   14.55 +			offset_x=scrollh.getValue();
   14.56 +			offset_y=scrollv.getValue();
   14.57 +			Graphics g=can.getGraphics();
   14.58 +			if (old_x!=size_x || old_y!=size_y)
   14.59 +				update(g);
   14.60 +			else {
   14.61 +				g.translate(-offset_x,-offset_y);
   14.62 +				g.drawImage(img,0,0,this);
   14.63 +			}
   14.64 +			return true;
   14.65 +		}
   14.66 +		else return super.handleEvent(evt);
   14.67 +	}
   14.68 +
   14.69 +	public void adjust_scrollbars()
   14.70 +	{
   14.71 +		int viewport_v=can.size().height;
   14.72 +		int viewport_h=can.size().width;
   14.73 +		int value_v=scrollv.getValue();
   14.74 +		int value_h=scrollh.getValue();
   14.75 +
   14.76 +		scrollv.setValues(value_v,viewport_v,0,size_y-viewport_v);
   14.77 +		scrollh.setValues(value_h,viewport_h,0,size_x-viewport_h);
   14.78 +		scrollv.setLineIncrement(viewport_v/20);
   14.79 +		scrollv.setPageIncrement(viewport_v);
   14.80 +		scrollh.setLineIncrement(viewport_h/20);
   14.81 +		scrollh.setPageIncrement(viewport_h);
   14.82 +		offset_x=scrollh.getValue();
   14.83 +		offset_y=scrollv.getValue();
   14.84 +	}
   14.85 +
   14.86 +	public void set_size(int x,int y)
   14.87 +	{
   14.88 +		size_x=x;size_y=y;
   14.89 +		adjust_scrollbars();
   14.90 +	}
   14.91 +
   14.92 +	public void focus_to(int x,int y) {
   14.93 +		offset_x=Math.min(scrollh.getMaximum(),Math.max(0,x-can.size().width/2));
   14.94 +		offset_y=Math.min(scrollv.getMaximum(),Math.max(0,y-can.size().height/2));
   14.95 +
   14.96 +		scrollh.setValue(offset_x);
   14.97 +		scrollv.setValue(offset_y);
   14.98 +		Graphics g=can.getGraphics();
   14.99 +		if (old_x!=size_x || old_y!=size_y)
  14.100 +			update(g);
  14.101 +		else {
  14.102 +			g.translate(-offset_x,-offset_y);
  14.103 +			g.drawImage(img,0,0,this);
  14.104 +		}
  14.105 +	}		
  14.106 +
  14.107 +	public void update(Graphics g) {
  14.108 +		g=can.getGraphics();
  14.109 +		int viewport_v=can.size().height;
  14.110 +		int viewport_h=can.size().width;
  14.111 +		int img_x=Math.max(viewport_h,size_x+1);
  14.112 +		int img_y=Math.max(viewport_v,size_y+1);
  14.113 +
  14.114 +		old_x=size_x;old_y=size_y;
  14.115 +		img=createImage(img_x,img_y);
  14.116 +		Graphics g2=img.getGraphics();
  14.117 +		g2.setColor(Color.lightGray);
  14.118 +		g2.fillRect(0,0,img_x,img_y);
  14.119 +		g2.setColor(Color.black);
  14.120 +		paintCanvas(g2);
  14.121 +		adjust_scrollbars();
  14.122 +		g.translate(-offset_x,-offset_y);
  14.123 +		g.drawImage(img,0,0,this);
  14.124 +	}
  14.125 +
  14.126 +	public void paint(Graphics g)
  14.127 +	{
  14.128 +		if (img!=null && old_x==size_x && old_y==size_y) {
  14.129 +			g=can.getGraphics();
  14.130 +			adjust_scrollbars();
  14.131 +			g.translate(-offset_x,-offset_y);
  14.132 +			g.drawImage(img,0,0,this);
  14.133 +		} else update(g);
  14.134 +	}
  14.135 +
  14.136 +	public Graphics getGraphics() {
  14.137 +		Graphics g=can.getGraphics();
  14.138 +
  14.139 +		g.translate(-offset_x,-offset_y);
  14.140 +		return g;
  14.141 +	}	
  14.142 +
  14.143 +	public void paintCanvas(Graphics g)
  14.144 +	{}
  14.145 +
  14.146 +	public ScrollCanvas()
  14.147 +	{
  14.148 +		can=new DummyCanvas(this);
  14.149 +		GridBagLayout gridbag = new GridBagLayout();
  14.150 +		GridBagConstraints c = new GridBagConstraints();
  14.151 +		scrollv=new Scrollbar(Scrollbar.VERTICAL);
  14.152 +		scrollh=new Scrollbar(Scrollbar.HORIZONTAL);
  14.153 +
  14.154 +		setLayout(gridbag);
  14.155 +		c.weightx = 1.0;
  14.156 +		c.weighty = 1.0;
  14.157 +		c.gridwidth=1;
  14.158 +		c.fill = GridBagConstraints.BOTH;
  14.159 +		gridbag.setConstraints(can,c);
  14.160 +		add(can);
  14.161 +		c.weightx=0;
  14.162 +		c.weighty=0;
  14.163 +		c.gridwidth = GridBagConstraints.REMAINDER;
  14.164 +		c.fill = GridBagConstraints.VERTICAL;
  14.165 +		gridbag.setConstraints(scrollv,c);
  14.166 +		add(scrollv);
  14.167 +		c.gridwidth = 1;
  14.168 +		c.fill = GridBagConstraints.HORIZONTAL;
  14.169 +		gridbag.setConstraints(scrollh,c);
  14.170 +		add(scrollh);
  14.171 +	}
  14.172 +}
    15.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    15.2 +++ b/lib/browser/awtUtilities/TextFrame.java	Wed Aug 06 00:06:47 1997 +0200
    15.3 @@ -0,0 +1,28 @@
    15.4 +/***************************************************************************
    15.5 +  Title:      Graph/TextFrame.java
    15.6 +  ID:         $Id$
    15.7 +  Author:     Stefan Berghofer, TU Muenchen
    15.8 +  Copyright   1997  TU Muenchen
    15.9 +
   15.10 +  This class defines a simple text viewer.
   15.11 +***************************************************************************/
   15.12 +
   15.13 +package awtUtilities;
   15.14 +
   15.15 +import java.awt.*;
   15.16 +
   15.17 +public class TextFrame extends Frame {
   15.18 +	public boolean action(Event evt,Object obj) {
   15.19 +		if (evt.target instanceof Button)
   15.20 +			hide();
   15.21 +		return true;
   15.22 +	}
   15.23 +
   15.24 +	public TextFrame(String title,String text) {
   15.25 +		super(title);
   15.26 +		TextArea ta=new TextArea(text,200,80);
   15.27 +		ta.setEditable(false);
   15.28 +		add("Center",ta);
   15.29 +		add("South",new Button("Dismiss"));
   15.30 +	}
   15.31 +}