Source files for Isabelle theory graph browser.
Initial revision.
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/lib/browser/GraphBrowser/DummyVertex.java Wed Aug 06 00:06:47 1997 +0200
@@ -0,0 +1,31 @@
+/***************************************************************************
+ Title: GraphBrowser/DummyVertex.java
+ ID: $Id$
+ Author: Stefan Berghofer, TU Muenchen
+ Copyright 1997 TU Muenchen
+
+ This class represents a dummy vertex, which is used to simplify the
+ layout algorithm.
+***************************************************************************/
+
+package GraphBrowser;
+
+import java.util.*;
+import java.awt.*;
+
+class DummyVertex extends Vertex {
+ public boolean isDummy() {return true;}
+
+ public Object clone() {
+ Vertex ve=new DummyVertex();
+ ve.setX(getX());ve.setY(getY());
+ return ve;
+ }
+
+ public int leftX() { return getX(); }
+
+ public int rightX() { return getX(); }
+
+ public void draw(Graphics g) {}
+}
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/lib/browser/GraphBrowser/Graph.java Wed Aug 06 00:06:47 1997 +0200
@@ -0,0 +1,1074 @@
+/***************************************************************************
+ Title: GraphBrowser/Graph.java
+ ID: $Id$
+ Author: Stefan Berghofer, TU Muenchen
+ Copyright 1997 TU Muenchen
+
+ This class contains the core of the layout algorithm and methods for
+ drawing and PostScript output.
+***************************************************************************/
+
+package GraphBrowser;
+
+import java.util.*;
+import java.awt.*;
+import java.io.*;
+
+class ParseError extends Exception {
+ public ParseError(String s) { super(s); }
+}
+
+public class Graph {
+ /**** parameters for layout ****/
+
+ public int box_height=0;
+ public int box_height2;
+ public int box_width;
+ public int box_width2;
+ public int box_hspace;
+
+ Vector vertices=new Vector(10,10);
+ Vector splines=new Vector(10,10);
+ Vector numEdges=new Vector(10,10);
+ Vertex []vertices2;
+
+ public int min_x=0,min_y=0,max_x=10,max_y=10;
+
+ /********************************************************************/
+ /* clone graph object */
+ /********************************************************************/
+
+ public Object clone() {
+ Graph gr=new Graph();
+ Enumeration e1;
+ int i;
+
+ gr.splines=(Vector)(splines.clone());
+
+ e1=vertices.elements();
+ while (e1.hasMoreElements())
+ gr.addVertex((Vertex)(((Vertex)(e1.nextElement())).clone()));
+
+ for (i=0;i<vertices.size();i++) {
+ Vertex vx1=(Vertex)(gr.vertices.elementAt(i));
+ e1=((Vertex)(vertices.elementAt(i))).getChildren();
+ while (e1.hasMoreElements()) {
+ Vertex vx2=(Vertex)(gr.vertices.elementAt(vertices.indexOf(e1.nextElement())));
+ vx1.addChild(vx2);
+ }
+ }
+
+ gr.vertices2 = new Vertex[vertices.size()];
+ gr.vertices.copyInto(gr.vertices2);
+
+ gr.min_x=min_x;gr.max_x=max_x;
+ gr.min_y=min_y;gr.max_y=max_y;
+
+ return gr;
+ }
+
+ Graph() {}
+
+ /********************************************************************/
+ /* Read graph from stream */
+ /********************************************************************/
+
+ public Graph(InputStream s,TreeNode tn) throws IOException, ParseError {
+ StreamTokenizer tok=new StreamTokenizer(s);
+ String name,dir,vertexID;
+ Vertex ve1,ve2;
+ boolean children,unfoldDir;
+ int index=0;
+
+ tok.nextToken();
+ while (tok.ttype!=StreamTokenizer.TT_EOF) {
+ if (tok.ttype!=StreamTokenizer.TT_WORD && tok.ttype!='"')
+ throw new ParseError("expected: vertex name\nfound : "+tok.toString());
+ name=tok.sval;
+ tok.nextToken();
+ if (tok.ttype!=StreamTokenizer.TT_WORD && tok.ttype!='"')
+ throw new ParseError("expected: vertex identifier\nfound : "+tok.toString());
+ vertexID=tok.sval;
+ tok.nextToken();
+ if (tok.ttype!=StreamTokenizer.TT_WORD && tok.ttype!='"')
+ throw new ParseError("expected: directory name\nfound : "+tok.toString());
+ dir=tok.sval;
+ tok.nextToken();
+ if (tok.ttype=='+') {
+ unfoldDir=true;
+ tok.nextToken();
+ } else
+ unfoldDir=false;
+ if (tok.ttype!=StreamTokenizer.TT_WORD && tok.ttype!='"')
+ throw new ParseError("expected: path name\nfound : "+tok.toString());
+ ve1=findVertex(vertexID);
+ if (ve1==null) {
+ ve1=new NormalVertex("");
+ ve1.setID(vertexID);
+ ve1.setNumber(index++);
+ addVertex(ve1);
+ }
+ ve1.setPath(tok.sval);
+ ve1.setDir(dir);
+ ve1.setLabel(name);
+ tn.insertNode(name,dir,tok.sval,ve1.getNumber(),unfoldDir);
+ tok.nextToken();
+ if (tok.ttype=='<') {
+ children=true;
+ tok.nextToken();
+ } else if (tok.ttype=='>') {
+ children=false;
+ tok.nextToken();
+ } else children=true;
+ while (tok.ttype!=';') {
+ if (tok.ttype!=StreamTokenizer.TT_WORD && tok.ttype!='"')
+ throw new ParseError("expected: child vertex identifier or ';'\nfound : "+tok.toString());
+ ve2=findVertex(tok.sval);
+ if (ve2==null) {
+ ve2=new NormalVertex("");
+ ve2.setID(tok.sval);
+ ve2.setNumber(index++);
+ addVertex(ve2);
+ }
+ if (children)
+ ve1.addChild(ve2);
+ else
+ ve1.addParent(ve2);
+ tok.nextToken();
+ }
+ tok.nextToken();
+ }
+ vertices2 = new Vertex[vertices.size()];
+ vertices.copyInto(vertices2);
+ }
+
+ /*** Find vertex with identifier vertexID ***/
+
+ public Vertex findVertex(String vertexID) {
+ Enumeration e1=vertices.elements();
+ Vertex v1;
+
+ while (e1.hasMoreElements()) {
+ v1=(Vertex)(e1.nextElement());
+ if ((v1.getID()).equals(vertexID))
+ return v1;
+ }
+ return null;
+ }
+
+ public void addVertex(Vertex v) {
+ vertices.addElement(v);
+ v.setGraph(this);
+ }
+
+ public void removeVertex(Vertex v) {
+ vertices.removeElement(v);
+ }
+
+ public Enumeration getVertices() {
+ return vertices.elements();
+ }
+
+ /********************************************************************/
+ /* graph layout */
+ /********************************************************************/
+
+ public void layout(Graphics g) {
+ splines.removeAllElements();
+ hasseDiagram();
+ Vector layers=min_crossings(insert_dummies((Vector)(sort().elementAt(0))));
+ setParameters(g);
+ init_coordinates(layers);
+ pendulum(layers);
+ rubberband(layers);
+ calcSplines(layers);
+ calcBoundingBox();
+ }
+
+ /********************************************************************/
+ /* set layout parameters */
+ /********************************************************************/
+
+ public void setParameters(Graphics g) {
+ Enumeration e1=vertices.elements();
+ int h,w;
+ h=w=Integer.MIN_VALUE;
+
+ while (e1.hasMoreElements()) {
+ Dimension dim=((Vertex)(e1.nextElement())).getLabelSize(g);
+ h=Math.max(h,dim.height);
+ w=Math.max(w,dim.width);
+ }
+ box_height=h+4;
+ box_height2=box_height/2;
+ box_width=w+8;
+ box_width2=box_width/2;
+ box_hspace=box_width+20;
+ }
+
+ /********************************************************************/
+ /* topological sorting */
+ /********************************************************************/
+
+ public Vector sort() {
+ Vector todo=(Vector)(vertices.clone());
+ Vector layers=new Vector(10,10);
+ Vector todo2;
+ Enumeration e1,e2;
+ Vertex v,v2;
+
+ e1=vertices.elements();
+ while (e1.hasMoreElements())
+ ((Vertex)(e1.nextElement())).setDegree(0);
+
+ e1=vertices.elements();
+ while (e1.hasMoreElements()) {
+ v=(Vertex)(e1.nextElement());
+ e2=v.getChildren();
+ while (e2.hasMoreElements()) {
+ v2=(Vertex)(e2.nextElement());
+ todo.removeElement(v2);
+ v2.setDegree(1+v2.getDegree());
+ }
+ }
+ while (!todo.isEmpty()) {
+ layers.addElement(todo);
+ todo2=new Vector(10,10);
+ e1=todo.elements();
+ while (e1.hasMoreElements()) {
+ e2=((Vertex)(e1.nextElement())).getChildren();
+ while (e2.hasMoreElements()) {
+ v=(Vertex)(e2.nextElement());
+ v.setDegree(v.getDegree()-1);
+ if (v.getDegree()==0) {
+ todo2.addElement(v);
+ v.setDegree(layers.size());
+ }
+ }
+ }
+ todo=todo2;
+ }
+ return layers;
+ }
+
+ /********************************************************************/
+ /* compute hasse diagram */
+ /********************************************************************/
+
+ public void hasseDiagram() {
+ Enumeration e1,e2;
+ Vertex vx1,vx2;
+
+ /** construct adjacence matrix **/
+
+ int vs=vertices.size();
+ boolean adj[][]=new boolean[vs][vs];
+ boolean adj2[][]=new boolean[vs][vs];
+ int i,j,k;
+
+ e1=getVertices();
+ for (i=0;i<vs;i++) {
+ vx1=(Vertex)(e1.nextElement());
+ e2=vx1.getChildren();
+ while (e2.hasMoreElements()) {
+ vx2=(Vertex)(e2.nextElement());
+ j=vertices.indexOf(vx2);
+ adj[i][j]=true;
+ adj2[i][j]=true;
+ }
+ }
+
+ /** compute transitive closure R+ **/
+
+ for (k=0;k<vs;k++)
+ for (i=0;i<vs;i++)
+ if (adj[i][k])
+ for (j=0;j<vs;j++)
+ adj[i][j] = adj[i][j] || adj[k][j];
+
+ /** compute R \ (R+)^2 **/
+
+ for (i=0;i<vs;i++)
+ for (j=0;j<vs;j++)
+ if (adj2[i][j]) {
+ vx1=(Vertex)(vertices.elementAt(i));
+ vx2=(Vertex)(vertices.elementAt(j));
+ for (k=0;k<vs;k++)
+ if (adj[i][k] && adj[k][j]) {
+ vx1.removeChild(vx2);
+ break;
+ }
+ }
+ }
+
+ /********************************************************************/
+ /* insert dummy vertices */
+ /********************************************************************/
+
+ public Vector insert_dummies(Vector v) {
+ Vector layers2=new Vector(10,10);
+ int n_edges;
+
+ do {
+ Enumeration e1=v.elements(),e2;
+ Vector next=new Vector(10,10);
+
+ layers2.addElement(v);
+ n_edges=0;
+ while (e1.hasMoreElements()) {
+ Vertex v1=(Vertex)(e1.nextElement());
+ e2=v1.getChildren();
+ while (e2.hasMoreElements()) {
+ n_edges++;
+ Vertex v2=(Vertex)(e2.nextElement());
+ if (v2.getDegree()!=v1.getDegree()+1) {
+ Vertex v3=new DummyVertex();
+ v3.addChild(v2);
+ v3.setDegree(v1.getDegree()+1);
+ v1.removeChild(v2);
+ v1.addChild(v3);
+ next.addElement(v3);
+ addVertex(v3);
+ } else if (next.indexOf(v2)<0) next.addElement(v2);
+ }
+ }
+ v=next;
+ numEdges.addElement(new Integer(n_edges));
+ } while (!v.isEmpty());
+ return layers2;
+ }
+
+ /********************************************************************/
+ /* calculation of crossings */
+ /********************************************************************/
+
+ public int count_crossings(Vector layers,int oldcr) {
+ int i,j,y1,y2,cr=0,l;
+ for (l=0;l<layers.size()-1;l++) {
+ Vector v1=(Vector)(layers.elementAt(l));
+ for (i=0;i<v1.size();i++) {
+ Enumeration e2=((Vertex)(v1.elementAt(i))).getChildren();
+ while (e2.hasMoreElements()) {
+ y1=((Vector)(layers.elementAt(l+1))).indexOf(e2.nextElement());
+ for (j=0;j<i;j++) {
+ Enumeration e3=((Vertex)(v1.elementAt(j))).getChildren();
+ while (e3.hasMoreElements()) {
+ y2=((Vector)(layers.elementAt(l+1))).indexOf(e3.nextElement());
+ if (y1<y2) {
+ cr++;
+ if (cr>=oldcr) return cr;
+ }
+ }
+ }
+ }
+ }
+ }
+ return cr;
+ }
+
+ /********************************************************************/
+ /* calculation of crossings where vertices vx1 and vx2 are involved */
+ /* vx1 and vx2 must be in same layer and vx1 is left from vx2 */
+ /********************************************************************/
+
+ public int count_crossings_2(Vector layers,Vertex vx1,Vertex vx2,int oldcr) {
+ int i,cr=0,l=vx1.getDegree();
+ Vertex va,vb;
+ Vector layer;
+ Enumeration e1,e2;
+
+ if (l>0) {
+ layer=(Vector)(layers.elementAt(l-1));
+ e1=vx1.getParents();
+ while (e1.hasMoreElements()) {
+ va=(Vertex)(e1.nextElement());
+ i=layer.indexOf(va);
+ e2=vx2.getParents();
+ while (e2.hasMoreElements()) {
+ vb=(Vertex)(e2.nextElement());
+ if (layer.indexOf(vb)<i) {
+ cr++;
+ if (cr>=oldcr) return cr;
+ }
+ }
+ }
+ }
+ if (l<layers.size()-1) {
+ layer=(Vector)(layers.elementAt(l+1));
+ e1=vx1.getChildren();
+ while (e1.hasMoreElements()) {
+ va=(Vertex)(e1.nextElement());
+ i=layer.indexOf(va);
+ e2=vx2.getChildren();
+ while (e2.hasMoreElements()) {
+ vb=(Vertex)(e2.nextElement());
+ if (layer.indexOf(vb)<i) {
+ cr++;
+ if (cr>=oldcr) return cr;
+ }
+ }
+ }
+ }
+ return cr;
+ }
+
+ /********************************************************************/
+ /* reduction of crossings by exchanging adjacent vertices */
+ /********************************************************************/
+
+ public void exchangeVertices(Vector layers,int oldcr) {
+ int i,l,c1,c2;
+ Vertex vx1,vx2;
+ Vector v1;
+
+ for (l=0;l<layers.size();l++) {
+ v1=(Vector)(layers.elementAt(l));
+ for (i=0;i<v1.size()-1;i++) {
+ vx1=(Vertex)(v1.elementAt(i));
+ vx2=(Vertex)(v1.elementAt(i+1));
+ c1=count_crossings_2(layers,vx1,vx2,oldcr);
+ c2=count_crossings_2(layers,vx2,vx1,c1);
+ if (c2<c1) {
+ v1.setElementAt(vx2,i);
+ v1.setElementAt(vx1,i+1);
+ }
+ }
+ }
+ }
+
+ /********************************************************************/
+ /* minimization of crossings */
+ /********************************************************************/
+
+ public Vector min_crossings(Vector layers) {
+ int n,i,l,k,z=0,cr2,cr=count_crossings(layers,Integer.MAX_VALUE);
+ boolean topdown=true,first=true;
+ Enumeration e1,e2;
+ Vector v1,v2,layers2=null,best=layers;
+ Vertex vx1,vx2;
+ n=0;
+ while (n<3 && cr>0) {
+ if (topdown) {
+ /** top-down-traversal **/
+
+ layers2=new Vector(10,10);
+ for (l=0;l<layers.size();l++) {
+ v1=(Vector)(layers.elementAt(l));
+ if (l==0) layers2.addElement(v1.clone());
+ else {
+ v2=new Vector(10,10);
+ layers2.addElement(v2);
+ e1=v1.elements();
+ while (e1.hasMoreElements()) {
+ vx1=(Vertex)(e1.nextElement());
+ k=0;z=0;
+ e2=vx1.getParents();
+ while (e2.hasMoreElements()) {
+ k+=((Vector)(layers2.elementAt(l-1))).indexOf(e2.nextElement());
+ z++;
+ }
+ if (z>0)
+ vx1.setWeight(((double)(k))/z);
+ else if (first)
+ vx1.setWeight(Double.MAX_VALUE);
+ for (i=0;i<v2.size();i++)
+ if (vx1.getWeight()<((Vertex)(v2.elementAt(i))).getWeight()) break;
+ if (i==v2.size()) v2.addElement(vx1);
+ else v2.insertElementAt(vx1,i);
+ }
+ }
+ }
+ } else {
+ /** bottom-up-traversal **/
+
+ layers2=new Vector(10,10);
+ for (l=layers.size()-1;l>=0;l--) {
+ v1=(Vector)(layers.elementAt(l));
+ if (l==layers.size()-1) layers2.addElement(v1.clone());
+ else {
+ v2=new Vector(10,10);
+ layers2.insertElementAt(v2,0);
+ e1=v1.elements();
+ while (e1.hasMoreElements()) {
+ vx1=(Vertex)(e1.nextElement());
+ k=0;z=0;
+ e2=vx1.getChildren();
+ while (e2.hasMoreElements()) {
+ k+=((Vector)(layers2.elementAt(1))).indexOf(e2.nextElement());
+ z++;
+ }
+ if (z>0)
+ vx1.setWeight(((double)(k))/z);
+ else if (first)
+ vx1.setWeight(Double.MAX_VALUE);
+ for (i=0;i<v2.size();i++)
+ if (vx1.getWeight()<((Vertex)(v2.elementAt(i))).getWeight()) break;
+ if (i==v2.size()) v2.addElement(vx1);
+ else v2.insertElementAt(vx1,i);
+ }
+ }
+ }
+ }
+ //exchangeVertices(layers2,cr);
+ topdown=!topdown;
+ first=false;
+ layers=layers2;
+
+ cr2=count_crossings(layers2,cr);
+ if (cr2<cr) {
+ best=layers2;
+ cr=cr2;
+ } else n++;
+ }
+
+ while (true) {
+ exchangeVertices(best,cr);
+ cr2=count_crossings(best,cr);
+ if (cr2<cr)
+ cr=cr2;
+ else
+ break;
+ }
+
+ return best;
+ }
+
+ /********************************************************************/
+ /* set initial coordinates */
+ /********************************************************************/
+
+ public void init_coordinates(Vector layers) {
+ int y=0;
+ Enumeration e1=layers.elements();
+ Enumeration e3=numEdges.elements();
+ while (e1.hasMoreElements()) {
+ Vector v1=(Vector)(e1.nextElement());
+ Enumeration e2=v1.elements();
+ int x=box_width2;
+ while (e2.hasMoreElements()) {
+ Vertex ve=(Vertex)(e2.nextElement());
+ ve.setX(x);
+ ve.setY(y);
+ x+=box_hspace;
+ }
+ y+=box_height+Math.max(35,7*(((Integer)(e3.nextElement())).intValue()));
+ }
+ }
+
+ /********************************************************************/
+ /* pendulum method */
+ /********************************************************************/
+
+ public void pendulum(Vector layers) {
+ Vector layers2=new Vector(10,10);
+ Enumeration e1=layers.elements(),e2;
+ int i,j,d1,d2,k,offset,dsum;
+ Region r1,r2;
+ boolean change;
+
+ while (e1.hasMoreElements()) {
+ e2=((Vector)(e1.nextElement())).elements();
+ Vector layer=new Vector(10,10);
+ layers2.addElement(layer);
+ while (e2.hasMoreElements()) {
+ Region r=new Region(this);
+ r.addVertex((Vertex)(e2.nextElement()));
+ layer.addElement(r);
+ }
+ }
+ for (k=0;k<10;k++) {
+ dsum=0;
+ for (j=1;j<layers2.size();j++) {
+ Vector l=(Vector)(layers2.elementAt(j));
+ if (l.size()>=2) {
+ do {
+ change=false;
+ d1=((Region)(l.firstElement())).pred_deflection();
+ for (i=0;i<l.size()-1;i++) {
+ r1=(Region)(l.elementAt(i));
+ r2=(Region)(l.elementAt(i+1));
+ d2=r2.pred_deflection();
+ if (r1.touching(r2) && (d1 <= 0 && d2 < d1 ||
+ d2 > 0 && d1 > d2 || d1 > 0 && d2 < 0)) {
+ r1.combine(r2);
+ l.removeElement(r2);
+ change=true;
+ d2=r1.pred_deflection();
+ }
+ d1=d2;
+ }
+ } while (change);
+ }
+ for (i=0;i<l.size();i++) {
+ r1=(Region)(l.elementAt(i));
+ d1=r1.pred_deflection();
+ offset=d1;
+ if (d1<0 && i>0) offset=-Math.min(
+ ((Region)(l.elementAt(i-1))).spaceBetween(r1),-d1);
+ if (d1>=0 && i<l.size()-1) offset=Math.min(
+ r1.spaceBetween((Region)(l.elementAt(i+1))),d1);
+ r1.move(offset);
+ dsum+=Math.abs(d1);
+ }
+ }
+ if (dsum==0) break;
+ }
+ }
+
+ /********************************************************************/
+ /* rubberband method */
+ /********************************************************************/
+
+ public void rubberband(Vector layers) {
+ Enumeration e1,e2;
+ int i,n,k,d,d2;
+ Vector v;
+ Vertex vx;
+
+ for (k=0;k<10;k++) {
+ e1=layers.elements();
+ while (e1.hasMoreElements()) {
+ v=(Vector)(e1.nextElement());
+ for (i=0;i<v.size();i++) {
+ n=0;d=0;
+ vx=(Vertex)(v.elementAt(i));
+ e2=vx.getChildren();
+ while (e2.hasMoreElements()) {
+ d+=((Vertex)(e2.nextElement())).getX()-vx.getX();
+ n++;
+ }
+ e2=vx.getParents();
+ while (e2.hasMoreElements()) {
+ d+=((Vertex)(e2.nextElement())).getX()-vx.getX();
+ n++;
+ }
+ d2=(n!=0?d/n:0);
+
+ if (d<0 && (i==0 || ((Vertex)(v.elementAt(i-1))).rightX()+box_hspace-box_width < vx.leftX()+d2) ||
+ d>0 && (i==v.size()-1 || ((Vertex)(v.elementAt(i+1))).leftX()-box_hspace+box_width > vx.rightX()+d2))
+ vx.setX(vx.getX()+d2);
+ }
+ }
+ }
+ }
+
+ /**** Intersection point of two lines (auxiliary function for calcSplines) ****/
+ /**** Calculate intersection point of line which is parallel to line (p1,p2) ****/
+ /**** and leads through p5, with line (p3,p4) ****/
+
+ Point intersect(Point p1,Point p2,Point p3,Point p4,Point p5) {
+ float x=0,y=0,s1=0,s2=0;
+
+ if (p1.x!=p2.x)
+ s1=((float)(p2.y-p1.y))/(p2.x-p1.x);
+ if (p3.x!=p4.x)
+ s2=((float)(p4.y-p3.y))/(p4.x-p3.x);
+ if (p1.x==p2.x) {
+ x=p5.x;
+ y=s2*(p5.x-p3.x)+p3.y;
+ } else if (p3.x==p4.x) {
+ x=p3.x;
+ y=s1*(p3.x-p5.x)+p5.y;
+ } else {
+ x=(p5.x*s1-p3.x*s2+p3.y-p5.y)/(s1-s2);
+ y=s2*(x-p3.x)+p3.y;
+ }
+ return new Point(Math.round(x),Math.round(y));
+ }
+
+ /**** Calculate control points (auxiliary function for calcSplines) ****/
+
+ Points calcPoint(Point p1,Point p2,Point p3,int lboxx,int rboxx,int boxy) {
+
+ /*** Points p1 , p2 , p3 define a triangle which encloses the spline. ***/
+ /*** Check if adjacent boxes (specified by lboxx,rboxx and boxy) ***/
+ /*** collide with the spline. In this case p1 and p3 are shifted by an ***/
+ /*** appropriate offset before they are returned ***/
+
+ int xh1,xh2,bx=0,by=0;
+ boolean pt1 = boxy >= p1.y && boxy <= p3.y || boxy >= p3.y && boxy <= p1.y;
+ boolean pt2 = boxy+box_height >= p1.y && boxy+box_height <= p3.y ||
+ boxy+box_height >= p3.y && boxy+box_height <= p1.y;
+ boolean move = false;
+ Point b;
+
+ xh1 = p1.x+(boxy-p1.y)*(p3.x-p1.x)/(p3.y-p1.y);
+ xh2 = p1.x+(boxy+box_height-p1.y)*(p3.x-p1.x)/(p3.y-p1.y);
+
+ if (xh1 <= lboxx && pt1 && xh2 <= lboxx && pt2) {
+ move = true;
+ bx = lboxx;
+ by = boxy + (xh1 < xh2 ? 0 : box_height ) ;
+ } else if (xh1 >= rboxx && pt1 && xh2 >= rboxx && pt2) {
+ move = true;
+ bx = rboxx;
+ by = boxy + (xh1 > xh2 ? 0 : box_height ) ;
+ } else if ( (xh1 <= lboxx || xh1 >= rboxx) && pt1) {
+ move = true;
+ bx = (xh1 <= lboxx ? lboxx : rboxx ) ;
+ by = boxy;
+ } else if ( (xh2 <= lboxx || xh2 >= rboxx) && pt2) {
+ move = true;
+ bx = (xh2 <= lboxx ? lboxx : rboxx ) ;
+ by = boxy+box_height;
+ }
+ b=new Point(bx,by);
+ if (move) return new Points(intersect(p1,p3,p1,p2,b),intersect(p1,p3,p2,p3,b));
+ else return new Points(p1,p3);
+ }
+
+ /********************************************************************/
+ /* calculate splines */
+ /********************************************************************/
+
+ public void calcSplines(Vector layers) {
+ Enumeration e2,e1=vertices.elements();
+ Vertex vx1,vx2,vx3;
+ Vector pos,layer;
+ int x1,y1,x2,y2,x3,y3,xh,k,leftx,rightx,spc;
+
+ while (e1.hasMoreElements()) {
+ vx1=(Vertex)(e1.nextElement());
+ if (!vx1.isDummy()) {
+ e2=vx1.getChildren();
+ while (e2.hasMoreElements()) {
+ vx2=(Vertex)(e2.nextElement());
+ if (vx2.isDummy()) {
+ vx3=vx2;
+ /**** convert edge to spline ****/
+ pos=new Vector(10,10);
+ x1=vx1.getX();
+ y1=vx1.getY()+box_height;
+
+ do {
+ /*** calculate position of control points ***/
+ x2=vx2.getX();
+ y2=vx2.getY();
+ layer=(Vector)(layers.elementAt(vx2.getDegree()));
+ k=layer.indexOf(vx2);
+ vx2=(Vertex)((vx2.getChildren()).nextElement());
+ x3=vx2.getX();
+ y3=vx2.getY();
+ // spc=(box_hspace-box_width)/3;
+ // spc=box_height*3/4;
+ spc=0;
+ leftx = k==0 /* || ((Vertex)(layer.elementAt(k-1))).isDummy() */ ?
+ Integer.MIN_VALUE:
+ ((Vertex)(layer.elementAt(k-1))).rightX()+spc;
+ rightx = k==layer.size()-1 /* || ((Vertex)(layer.elementAt(k+1))).isDummy() */ ?
+ Integer.MAX_VALUE:
+ ((Vertex)(layer.elementAt(k+1))).leftX()-spc;
+ xh=x2+box_height*(x3-x2)/(y3-y2);
+ if (!(x2<=x3 && xh>=rightx || x2>x3 && xh<=leftx)) {
+ /* top control point */
+ pos.addElement(new Integer(1));
+ y1=y2;
+ } else {
+ xh=x1+(y2-y1)*(x2-x1)/(y2+box_height-y1);
+ if (!(x2<=x1 && xh>=rightx || x2>x1 && xh<=leftx))
+ /* bottom control point */
+ pos.addElement(new Integer(2));
+ else
+ /* two control points needed */
+ pos.addElement(new Integer(3));
+ y1=y2+box_height;
+ }
+ x1=x2;
+ } while (vx2.isDummy());
+ pos.addElement(new Integer(1));
+
+ /**** calculate triangles ****/
+ vx2=vx3;
+
+ int pos1,pos2,i=0;
+ Vector pts=new Vector(10,10);
+ int lboxx,rboxx,boxy;
+
+ x1=vx1.getX();
+ y1=vx1.getY()+box_height;
+ pts.addElement(new Point(x1,y1)); /** edge starting point **/
+ do {
+ x2=vx2.getX();
+ y2=vx2.getY();
+ pos1=((Integer)(pos.elementAt(i))).intValue();
+ pos2=((Integer)(pos.elementAt(i+1))).intValue();
+ i++;
+ layer=(Vector)(layers.elementAt(vx2.getDegree()));
+ k=layer.indexOf(vx2);
+ boxy=vx2.getY();
+ vx2=(Vertex)((vx2.getChildren()).nextElement());
+ x3=vx2.getX();
+ y3=vx2.getY();
+ if (pos1==2) y2+=box_height;
+ if (pos2==2) y3+=box_height;
+
+ lboxx = (k==0 /* || ((Vertex)(layer.elementAt(k-1))).isDummy() */ ) ?
+ Integer.MIN_VALUE :
+ ((Vertex)(layer.elementAt(k-1))).rightX();
+
+ rboxx = (k==layer.size()-1 /* || ((Vertex)(layer.elementAt(k+1))).isDummy() */ ) ?
+ Integer.MAX_VALUE :
+ ((Vertex)(layer.elementAt(k+1))).leftX();
+
+ Point p1,p2,p3;
+ Points ps;
+
+ p1 = new Point((x1+x2)/2,(y1+y2)/2);
+
+ if (pos1<=2) {
+ /** one control point **/
+ p2 = new Point(x2,y2);
+ ps = calcPoint(p1,p2,new Point((x2+x3)/2,(y2+y3)/2),lboxx,rboxx,boxy);
+ pts.addElement(ps.p);
+ pts.addElement(p2);
+ pts.addElement(ps.q);
+ } else {
+ /** two control points **/
+ p2 = new Point(x2,y2-box_height);
+ p3 = new Point(x2,y2+box_height2);
+ ps = calcPoint(p1,p2,p3,lboxx,rboxx,boxy);
+ pts.addElement(ps.p);
+ pts.addElement(p2);
+ pts.addElement(ps.q);
+ p2 = new Point(x2,y2+box_height*2);
+ ps = calcPoint(p3,p2,new Point((p2.x+x3)/2,(p2.y+y3)/2),
+ lboxx,rboxx,boxy);
+ pts.addElement(ps.p);
+ pts.addElement(p2);
+ pts.addElement(ps.q);
+ }
+ x1=p2.x;
+ y1=p2.y;
+ } while (vx2.isDummy());
+
+ pts.addElement(new Point(vx2.getX(),vx2.getY())); /** edge end point **/
+ splines.addElement(new Spline(pts));
+ }
+ }
+ }
+ }
+ }
+
+ /********************************************************************/
+ /* calculate bounding box */
+ /********************************************************************/
+
+ public void calcBoundingBox() {
+ min_y=min_x=Integer.MAX_VALUE;
+ max_y=max_x=Integer.MIN_VALUE;
+
+ Enumeration e1=vertices.elements();
+ Vertex v;
+
+ while (e1.hasMoreElements()) {
+ v=(Vertex)(e1.nextElement());
+ min_x=Math.min(min_x,v.leftX());
+ max_x=Math.max(max_x,v.rightX());
+ min_y=Math.min(min_y,v.getY());
+ max_y=Math.max(max_y,v.getY()+box_height);
+ }
+ min_x-=20;
+ min_y-=20;
+ max_x+=20;
+ max_y+=20;
+ }
+
+ /********************************************************************/
+ /* draw graph */
+ /********************************************************************/
+
+ public void draw(Graphics g) {
+ if (box_height==0) layout(g);
+
+ g.translate(-min_x,-min_y);
+
+ Enumeration e1=vertices.elements();
+ while (e1.hasMoreElements())
+ ((Vertex)(e1.nextElement())).draw(g);
+
+ e1=splines.elements();
+ while (e1.hasMoreElements())
+ ((Spline)(e1.nextElement())).draw(g);
+ }
+
+ /********************************************************************/
+ /* return vertex at position (x,y) */
+ /********************************************************************/
+
+ public Vertex vertexAt(int x,int y) {
+ Enumeration e1=vertices.elements();
+ while (e1.hasMoreElements()) {
+ Vertex v=(Vertex)(e1.nextElement());
+ if (v.contains(x,y)) return v;
+ }
+ return null;
+ }
+
+ /********************************************************************/
+ /* encode list of vertices (as array of vertice numbers) */
+ /********************************************************************/
+
+ public Vector encode(Vector v) {
+ Vector code=new Vector(10,10);
+ Enumeration e1=v.elements();
+
+ while (e1.hasMoreElements()) {
+ Vertex vx=(Vertex)(e1.nextElement());
+ if (vx.getNumber()>=0)
+ code.addElement(new Integer(vx.getNumber()));
+ }
+ return code;
+ }
+
+ /********************************************************************/
+ /* get vertex with number n */
+ /********************************************************************/
+
+ public Vertex getVertexByNum(int x) {
+ Enumeration e1=vertices.elements();
+
+ while (e1.hasMoreElements()) {
+ Vertex vx=(Vertex)(e1.nextElement());
+ if (vx.getNumber()==x) return vx;
+ }
+ return null;
+ }
+
+ /********************************************************************/
+ /* decode list of vertices */
+ /********************************************************************/
+
+ public Vector decode(Vector code) {
+ Enumeration e1=code.elements();
+ Vector vec=new Vector(10,10);
+
+ while (e1.hasMoreElements()) {
+ int i=((Integer)(e1.nextElement())).intValue();
+ //Vertex vx=getVertexByNum(i);
+ //if (vx!=null) vec.addElement(vx);
+ vec.addElement(vertices2[i]);
+ }
+ return vec;
+ }
+
+ /********************************************************************/
+ /* collapse vertices */
+ /********************************************************************/
+
+ public void collapse(Vector vs,String name,Vector inflate) {
+ Enumeration e1,e2,e3;
+ boolean nonempty=false;
+ Vertex vx3,vx2,vx1;
+
+ e1=vertices.elements();
+
+ vx1=new NormalVertex(name);
+ vx1.setInflate(inflate);
+
+ while (e1.hasMoreElements()) {
+ vx2=(Vertex)(e1.nextElement());
+
+ if (vs.indexOf(vx2)<0) {
+ e2=vx2.getParents();
+ while (e2.hasMoreElements()) {
+ vx3=(Vertex)(e2.nextElement());
+ if (vs.indexOf(vx3)>=0) {
+ if (!vx1.isChild(vx2))
+ vx1.addChild(vx2);
+ vx3.removeChild(vx2);
+ }
+ }
+
+ e2=vx2.getChildren();
+ while (e2.hasMoreElements()) {
+ vx3=(Vertex)(e2.nextElement());
+ if (vs.indexOf(vx3)>=0) {
+ if (!vx2.isChild(vx1))
+ vx2.addChild(vx1);
+ vx2.removeChild(vx3);
+ }
+ }
+ } else { nonempty=true; }
+ }
+
+ e1=vs.elements();
+ while (e1.hasMoreElements())
+ try {
+ removeVertex((Vertex)(e1.nextElement()));
+ } catch (NoSuchElementException exn) {}
+
+ if (nonempty) addVertex(vx1);
+ }
+
+ /********************************************************************/
+ /* PostScript output */
+ /********************************************************************/
+
+ public void PS(String fname,boolean printable) throws IOException {
+ FileOutputStream f = new FileOutputStream(fname);
+ PrintStream p = new PrintStream(f);
+
+ if (printable)
+ p.println("%!PS-Adobe-2.0\n\n%%BeginProlog");
+ else {
+ p.println("%!PS-Adobe-2.0 EPSF-2.0\n%%Orientation: Portrait");
+ p.println("%%BoundingBox: "+min_x+" "+min_y+" "+max_x+" "+max_y);
+ p.println("%%EndComments\n\n%%BeginProlog");
+ }
+ p.println("/m { moveto } def /l { lineto } def /n { newpath } def");
+ p.println("/s { stroke } def /c { curveto } def");
+ p.println("/b { n 0 0 m dup true charpath pathbbox 1 index 4 index sub");
+ p.println("7 index exch sub 2 div 9 index add 1 index 4 index sub 7 index exch sub");
+ p.println("2 div 9 index add 2 index add m pop pop pop pop");
+ p.println("1 -1 scale show 1 -1 scale n 3 index 3 index m 1 index 0 rlineto");
+ p.println("0 exch rlineto neg 0 rlineto closepath s pop pop } def");
+ p.println("%%EndProlog\n");
+ if (printable) {
+ int hsize=max_x-min_x;
+ int vsize=max_y-min_y;
+ if (hsize>vsize) {
+ // Landscape output
+ double scale=Math.min(1,Math.min(750.0/hsize,500.0/vsize));
+ double trans_x=50+max_y*scale+(500-scale*vsize)/2.0;
+ double trans_y=50+max_x*scale+(750-scale*hsize)/2.0;
+ p.println(trans_x+" "+trans_y+" translate");
+ p.println("-90 rotate");
+ p.println(scale+" "+(-scale)+" scale");
+ } else {
+ // Portrait output
+ double scale=Math.min(1,Math.min(500.0/hsize,750.0/vsize));
+ double trans_x=50-min_x*scale+(500-scale*hsize)/2.0;
+ double trans_y=50+max_y*scale+(750-scale*vsize)/2.0;
+ p.println(trans_x+" "+trans_y+" translate");
+ p.println(scale+" "+(-scale)+" scale");
+ }
+ } else
+ p.println("0 "+(max_y+min_y)+" translate\n1 -1 scale");
+
+ p.println("/Helvetica findfont 12 scalefont setfont");
+ p.println("0.5 setlinewidth");
+
+ Enumeration e1=vertices.elements();
+ while (e1.hasMoreElements())
+ ((Vertex)(e1.nextElement())).PS(p);
+
+ e1=splines.elements();
+ while (e1.hasMoreElements())
+ ((Spline)(e1.nextElement())).PS(p);
+
+ if (printable) p.println("showpage");
+
+ f.close();
+ }
+}
+
+/**** Return value of function calcPoint ****/
+
+class Points {
+ public Point p,q;
+
+ public Points(Point p1,Point p2) {
+ p=p1;q=p2;
+ }
+}
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/lib/browser/GraphBrowser/GraphBrowser.java Wed Aug 06 00:06:47 1997 +0200
@@ -0,0 +1,190 @@
+/***************************************************************************
+ Title: GraphBrowser/GraphBrowser.java
+ ID: $Id$
+ Author: Stefan Berghofer, TU Muenchen
+ Copyright 1997 TU Muenchen
+
+ This is the graph browser's main class. It contains the "main(...)"
+ method, which is used for the stand-alone version, as well as
+ "init(...)", "start(...)" and "stop(...)" methods which are used for
+ the applet version.
+ Note: GraphBrowser is designed for the 1.0.2 version of the JDK.
+***************************************************************************/
+
+package GraphBrowser;
+
+import java.awt.*;
+import java.applet.*;
+import java.io.*;
+import java.util.*;
+import java.net.*;
+import awtUtilities.*;
+
+public class GraphBrowser extends Applet {
+ GraphView gv;
+ TreeBrowser tb=null;
+ String gfname;
+
+ static boolean isApplet;
+ static Frame f;
+
+ public GraphBrowser(String name) {
+ gfname=name;
+ }
+
+ public GraphBrowser() {}
+
+ public void showWaitMessage() {
+ if (isApplet)
+ getAppletContext().showStatus("calculating layout, please wait ...");
+ else {
+ f.setCursor(Frame.WAIT_CURSOR);
+ }
+ }
+
+ public void showReadyMessage() {
+ if (isApplet)
+ getAppletContext().showStatus("ready !");
+ else {
+ f.setCursor(Frame.DEFAULT_CURSOR);
+ }
+ }
+
+ public void viewFile(String fname) {
+ try {
+ if (isApplet)
+ getAppletContext().showDocument(new URL(getDocumentBase(), fname),"_blank");
+ else {
+ String path=gfname.substring(0,gfname.lastIndexOf('/')+1);
+ InputStream is;
+ String line, text="";
+ DataInputStream di;
+
+ is=new FileInputStream(path+fname);
+ di=new DataInputStream(is);
+ while ((line=di.readLine())!=null)
+ text+=line+"\n";
+
+ if (fname.endsWith(".html")) {
+ /**** convert HTML to text (just a quick hack) ****/
+
+ String buf="";
+ char[] text2,text3;
+ int i,j=0;
+ boolean special=false, html=false;
+ char ctrl;
+
+ text2 = text.toCharArray();
+ text3 = new char[text.length()];
+ for (i = 0; i < text.length(); i++) {
+ char c = text2[i];
+ if (c == '&') {
+ special = true;
+ buf = "";
+ } else if (special) {
+ if (c == ';') {
+ special = false;
+ if (buf.equals("lt"))
+ text3[j++] = '<';
+ else if (buf.equals("gt"))
+ text3[j++] = '>';
+ else if (buf.equals("amp"))
+ text3[j++] = '&';
+ } else
+ buf += c;
+ } else if (c == '<') {
+ html = true;
+ ctrl = text2[i+1];
+ if ((ctrl == 'P') || (ctrl == 'B'))
+ text3[j++] = '\n';
+ } else if (c == '>')
+ html = false;
+ else if (!html)
+ text3[j++] = c;
+ }
+ text = String.valueOf(text3);
+ }
+
+ Frame f=new TextFrame(fname.substring(fname.lastIndexOf('/')+1),text);
+ f.resize(500,600);
+ f.show();
+ }
+ } catch (Exception exn) {
+ System.out.println("Can't read file "+fname);
+ }
+ }
+
+ public void PS(String fname,boolean printable) throws IOException {
+ gv.PS(fname,printable);
+ }
+
+ public boolean isEmpty() {
+ return tb==null;
+ }
+
+ public void initBrowser(InputStream is) {
+ try {
+ TreeNode tn=new TreeNode("Directories","",-1,true);
+ gv=new GraphView(new Graph(is,tn),this);
+ tb=new TreeBrowser(tn,gv);
+ gv.setTreeBrowser(tb);
+ Vector v=new Vector(10,10);
+ tn.collapsedDirectories(v);
+ gv.collapseDir(v);
+ Component gv2=new Border(gv,5);
+ Component tb2=new Border(tb,5);
+ GridBagLayout gridbag = new GridBagLayout();
+ GridBagConstraints cnstr = new GridBagConstraints();
+ setLayout(gridbag);
+ cnstr.fill = GridBagConstraints.BOTH;
+ cnstr.insets = new Insets(5,5,5,5);
+ cnstr.weightx = 1;
+ cnstr.weighty = 1;
+ cnstr.gridwidth = 1;
+ gridbag.setConstraints(tb2,cnstr);
+ add(tb2);
+ cnstr.weightx = 2.5;
+ cnstr.gridwidth = GridBagConstraints.REMAINDER;
+ gridbag.setConstraints(gv2,cnstr);
+ add(gv2);
+ } catch (IOException exn) {
+ System.out.println("\nI/O error while reading graph file.");
+ } catch (ParseError exn) {
+ System.out.println("\nParse error in graph file:");
+ System.out.println(exn.getMessage());
+ System.out.println("\nSyntax:\n<vertexname> <dirname> [ + ] <path> [ < | > ] [ <vertexname> [ ... [ <vertexname> ] ... ] ] ;");
+ }
+ }
+
+ public void init() {
+ isApplet=true;
+ gfname=getParameter("graphfile");
+ try {
+ InputStream is=(new URL(getDocumentBase(), gfname)).openConnection().getInputStream();
+ initBrowser(is);
+ is.close();
+ } catch (MalformedURLException exn) {
+ System.out.println("Invalid URL: "+gfname);
+ } catch (IOException exn) {
+ System.out.println("I/O error while reading "+gfname+".");
+ }
+ }
+
+ public static void main(String[] args) {
+ isApplet=false;
+ try {
+ GraphBrowser gb=new GraphBrowser(args.length > 0 ? args[0] : "");
+ if (args.length>0) {
+ InputStream is=new FileInputStream(args[0]);
+ gb.initBrowser(is);
+ is.close();
+ }
+ f=new GraphBrowserFrame(gb);
+ f.resize(700,500);
+ f.show();
+ } catch (IOException exn) {
+ System.out.println("Can't open graph file "+args[0]);
+ }
+ }
+}
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/lib/browser/GraphBrowser/GraphBrowserFrame.java Wed Aug 06 00:06:47 1997 +0200
@@ -0,0 +1,118 @@
+/***************************************************************************
+ Title: GraphBrowser/GraphBrowserFrame.java
+ ID: $Id$
+ Author: Stefan Berghofer, TU Muenchen
+ Copyright 1997 TU Muenchen
+
+ This class is the frame for the stand-alone application. It contains
+ methods for handling menubar events.
+***************************************************************************/
+
+package GraphBrowser;
+
+import java.awt.*;
+import java.io.*;
+import awtUtilities.*;
+
+public class GraphBrowserFrame extends Frame {
+ GraphBrowser gb;
+ MenuItem i1,i2;
+ String graphDir,psDir;
+
+ public void checkMenuItems() {
+ if (gb.isEmpty()) {
+ i1.disable();
+ i2.disable();
+ } else {
+ i1.enable();
+ i2.enable();
+ }
+ }
+
+ public boolean action(Event evt, Object arg) {
+ if (evt.target instanceof MenuItem) {
+ String label=(String)arg;
+ if (label.equals("Quit"))
+ System.exit(0);
+ else if (label.equals("Export to PostScript")) {
+ PS(true,label);
+ return true;
+ } else if (label.equals("Export to EPS")) {
+ PS(false,label);
+ return true;
+ } else if (label.equals("Open ...")) {
+ FileDialog fd=new FileDialog(this,"Open graph file",FileDialog.LOAD);
+ if (graphDir!=null)
+ fd.setDirectory(graphDir);
+ fd.show();
+ if (fd.getFile()==null) return true;
+ graphDir=fd.getDirectory();
+ String fname=graphDir+fd.getFile();
+ GraphBrowser gb2=new GraphBrowser(fname);
+ try {
+ InputStream is=new FileInputStream(fname);
+ gb2.initBrowser(is);
+ is.close();
+ } catch (IOException exn) {
+ String button[]={"OK"};
+ MessageDialog md=new MessageDialog(this,"Error","Can't open file "+fname+".",button);
+ md.resize(350,200);
+ md.show();
+ return true;
+ }
+ remove(gb);
+ add("Center",gb2);
+ gb=gb2;
+ checkMenuItems();
+ validate();
+ return true;
+ }
+ }
+ return false;
+ }
+
+ public void PS(boolean printable,String label) {
+ FileDialog fd=new FileDialog(this,label,FileDialog.SAVE);
+ if (psDir!=null)
+ fd.setDirectory(psDir);
+ fd.show();
+ if (fd.getFile()==null) return;
+ psDir=fd.getDirectory();
+ String fname=psDir+fd.getFile();
+
+ if ((new File(fname)).exists()) {
+ String buttons[]={"Overwrite","Cancel"};
+ MessageDialog md=new MessageDialog(this,"Warning",
+ "Warning: File "+fname+" already exists. Overwrite?",
+ buttons);
+ md.resize(350,200);
+ md.show();
+ if (md.getText().equals("Cancel")) return;
+ }
+
+ try {
+ gb.PS(fname,printable);
+ } catch (IOException exn) {
+ String button[]={"OK"};
+ MessageDialog md=new MessageDialog(this,"Error",
+ "Unable to write file "+fname+".",button);
+ md.resize(350,200);
+ md.show();
+ }
+ }
+
+ public GraphBrowserFrame(GraphBrowser br) {
+ super("GraphBrowser");
+ gb=br;
+ MenuBar mb=new MenuBar();
+ Menu m1=new Menu("File");
+ m1.add(new MenuItem("Open ..."));
+ m1.add(i1=new MenuItem("Export to PostScript"));
+ m1.add(i2=new MenuItem("Export to EPS"));
+ m1.add(new MenuItem("Quit"));
+ checkMenuItems();
+ mb.add(m1);
+ setMenuBar(mb);
+ add("Center",br);
+ }
+}
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/lib/browser/GraphBrowser/GraphView.java Wed Aug 06 00:06:47 1997 +0200
@@ -0,0 +1,236 @@
+/***************************************************************************
+ Title: GraphBrowser/GraphView.java
+ ID: $Id$
+ Author: Stefan Berghofer, TU Muenchen
+ Copyright 1997 TU Muenchen
+
+ This class defines the window in which the graph is displayed. It
+ contains methods for handling events such as collapsing / uncollapsing
+ nodes of the graph.
+***************************************************************************/
+
+package GraphBrowser;
+
+import java.awt.*;
+import java.io.*;
+import java.util.*;
+import awtUtilities.*;
+
+public class GraphView extends ScrollCanvas {
+ Graph gra,gra2;
+ GraphBrowser parent;
+ Vertex v=null;
+ Vector collapsed=new Vector(10,10);
+ Vector collapsedDirs=new Vector(10,10);
+ TreeBrowser tb;
+ long timestamp;
+ Vertex highlighted=null;
+
+ public void setTreeBrowser(TreeBrowser br) {
+ tb=br;
+ }
+
+ public GraphBrowser getBrowser() { return parent; }
+
+ public Graph getGraph() { return gra; }
+
+ public Graph getOriginalGraph() { return gra2; }
+
+ public GraphView(Graph gr,GraphBrowser br) {
+ gra2=gr;
+ parent=br;
+ gra=(Graph)(gra2.clone());
+ }
+
+ public void PS(String fname,boolean printable) throws IOException {
+ gra.PS(fname,printable);
+ }
+
+ public void paintCanvas(Graphics g)
+ {
+ set_size(gra.max_x-gra.min_x,gra.max_y-gra.min_y);
+ gra.draw(g);
+ }
+
+ public boolean mouseMove(Event evt,int x,int y) {
+ x+=gra.min_x;
+ y+=gra.min_y;
+
+ Vertex v2=gra.vertexAt(x,y);
+ Graphics g=getGraphics();
+ g.translate(-gra.min_x,-gra.min_y);
+ if (highlighted!=null) {
+ highlighted.drawBox(g,Color.lightGray);
+ highlighted=null;
+ }
+ if (v2!=v) {
+ if (v!=null) v.removeButtons(g);
+ if (v2!=null) v2.drawButtons(g);
+ v=v2;
+ }
+ return true;
+ }
+
+ /*****************************************************************/
+ /* This method is called if successor / predecessor nodes (whose */
+ /* numbers are stored in Vector c) of a certain node should be */
+ /* displayed again */
+ /*****************************************************************/
+
+ void uncollapse(Vector c) {
+ collapsed.removeElement(c);
+ collapseNodes();
+ }
+
+ /*****************************************************************/
+ /* This method is called by class TreeBrowser when directories */
+ /* are collapsed / uncollapsed by the user */
+ /*****************************************************************/
+
+ public void collapseDir(Vector v) {
+ collapsedDirs=v;
+
+ collapseNodes();
+ }
+
+ /*****************************************************************/
+ /* Inflate node again */
+ /*****************************************************************/
+
+ public void inflateNode(Vector c) {
+ Enumeration e1;
+
+ e1=collapsedDirs.elements();
+ while (e1.hasMoreElements()) {
+ Directory d=(Directory)(e1.nextElement());
+ if (d.collapsed==c) {
+ tb.selectNode(d.getNode());
+ return;
+ }
+ }
+
+ collapsed.removeElement(c);
+ e1=gra2.getVertices();
+ while (e1.hasMoreElements()) {
+ Vertex vx=(Vertex)(e1.nextElement());
+ if (vx.getUp()==c) vx.setUp(null);
+ if (vx.getDown()==c) vx.setDown(null);
+ }
+
+ collapseNodes();
+ relayout();
+ }
+
+ public void relayout() {
+ parent.showWaitMessage();
+ highlighted=null;
+ gra.layout(getGraphics());
+ v=null;
+ update(getGraphics());
+ parent.showReadyMessage();
+ }
+
+ public void focusToVertex(int n) {
+ Vertex vx=gra.getVertexByNum(n);
+ if (vx!=null) {
+ focus_to(vx.getX()-gra.min_x,vx.getY()-gra.min_y);
+ highlighted=vx;
+ Graphics g=getGraphics();
+ g.translate(-gra.min_x,-gra.min_y);
+ vx.drawBox(g,Color.white);
+ }
+ }
+
+ /*****************************************************************/
+ /* Create new graph with collapsed nodes */
+ /*****************************************************************/
+
+ public void collapseNodes() {
+ Enumeration e1=collapsed.elements();
+ gra=(Graph)(gra2.clone());
+
+ while (e1.hasMoreElements()) {
+ Vector v1=(Vector)(e1.nextElement());
+ Vector v2=gra.decode(v1);
+ if (!v2.isEmpty()) gra.collapse(v2,"[. . . .]",v1);
+ }
+
+ e1=collapsedDirs.elements();
+
+ while (e1.hasMoreElements()) {
+ Directory d=(Directory)(e1.nextElement());
+ Vector v=gra.decode(d.getCollapsed());
+ if (!v.isEmpty())
+ gra.collapse(v,"["+d.getName()+"]",d.getCollapsed());
+ }
+ }
+
+ public boolean mouseDown(Event evt,int x,int y) {
+ Vector code=null;
+ Vertex v2;
+ x+=gra.min_x;
+ y+=gra.min_y;
+
+ if (v!=null) {
+ int num=v.getNumber();
+ v2=gra2.getVertexByNum(num);
+ if (v.leftButton(x,y)) {
+ if (v.getUp()!=null) {
+ code=v.getUp();
+ v2.setUp(null);
+ v=null;
+ uncollapse(code);
+ relayout();
+ focusToVertex(num);
+ } else {
+ Vector vs=v2.getPreds();
+ code=gra2.encode(vs);
+ v.setUp(code);v2.setUp(code);
+ v=null;
+ collapsed.insertElementAt(code,0);
+ collapseNodes();
+ relayout();
+ focusToVertex(num);
+ }
+ } else if (v.rightButton(x,y)) {
+ if (v.getDown()!=null) {
+ code=v.getDown();
+ v2.setDown(null);
+ v=null;
+ uncollapse(code);
+ relayout();
+ focusToVertex(num);
+ } else {
+ Vector vs=v2.getSuccs();
+ code=gra2.encode(vs);
+ v.setDown(code);v2.setDown(code);
+ v=null;
+ collapsed.insertElementAt(code,0);
+ collapseNodes();
+ relayout();
+ focusToVertex(num);
+ }
+ } else if (v.getInflate()!=null) {
+ inflateNode(v.getInflate());
+ v=null;
+ } else {
+ if (evt.when-timestamp < 400 && !(v.getPath().equals("")))
+ parent.viewFile(v.getPath());
+ timestamp=evt.when;
+ }
+ }
+ return true;
+ }
+
+ public boolean mouseExit(Event evt,int x,int y) {
+ Graphics g=getGraphics();
+ g.translate(-gra.min_x,-gra.min_y);
+ if (highlighted!=null) {
+ highlighted.drawBox(g,Color.lightGray);
+ highlighted=null;
+ }
+ if (v!=null) v.removeButtons(g);
+ v=null;
+ return true;
+ }
+}
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/lib/browser/GraphBrowser/NormalVertex.java Wed Aug 06 00:06:47 1997 +0200
@@ -0,0 +1,161 @@
+/***************************************************************************
+ Title: GraphBrowser/NormalVertex.java
+ ID: $Id$
+ Author: Stefan Berghofer, TU Muenchen
+ Copyright 1997 TU Muenchen
+
+ This class represents an ordinary vertex. It contains methods for
+ drawing and PostScript output.
+***************************************************************************/
+
+package GraphBrowser;
+
+import java.util.*;
+import java.awt.*;
+import java.io.*;
+
+class NormalVertex extends Vertex {
+ String label="",path="",dir="",ID="";
+ Vector up,down,inflate=null;
+
+ public Object clone() {
+ Vertex ve=new NormalVertex(label);
+ ve.setID(ID);
+ ve.setNumber(getNumber());
+ ve.setUp(getUp());ve.setDown(getDown());
+ ve.setX(getX());ve.setY(getY());
+ ve.setPath(getPath());
+ return ve;
+ }
+
+ /*** Constructor ***/
+
+ public NormalVertex(String s) { label=s; }
+
+ public void setInflate(Vector v) { inflate=v; }
+
+ public Vector getInflate() { return inflate; }
+
+ public Vector getUp() { return up; }
+
+ public void setUp(Vector v) { up=v; }
+
+ public Vector getDown() { return down; }
+
+ public void setDown(Vector v) { down=v; }
+
+ public String getLabel() {return label;}
+
+ public void setLabel(String s) {label=s;}
+
+ public void setID(String s) { ID=s; }
+
+ public String getID() { return ID; }
+
+ public String getPath() { return path;}
+
+ public void setPath(String p) { path=p; }
+
+ public String getDir() { return dir; }
+
+ public void setDir(String d) { dir=d; }
+
+ public int leftX() { return getX()-gra.box_width2; }
+
+ public int rightX() { return getX()+gra.box_width2; }
+
+ public void drawBox(Graphics g,Color boxColor) {
+ FontMetrics fm=g.getFontMetrics(font);
+ g.setFont(font);
+ int h=fm.getAscent()+fm.getDescent();
+
+ g.setColor(boxColor);
+ g.fillRect(getX()-gra.box_width2,getY(),gra.box_width,gra.box_height);
+ g.setColor(Color.black);
+ g.drawRect(getX()-gra.box_width2,getY(),gra.box_width,gra.box_height);
+ if (getNumber()<0) {
+ g.setColor(Color.red);
+ label=label.substring(1,label.length()-1);
+ while (label.length()>0 && fm.stringWidth("["+label+"]")>gra.box_width-8)
+ label=label.substring(0,label.length()-1);
+ label="["+label+"]";
+ }
+
+ g.drawString(label,
+ (int)Math.round((gra.box_width-fm.stringWidth(label))/2.0)+getX()-gra.box_width2,
+ fm.getAscent()+(int)Math.round((gra.box_height-h)/2.0)+getY());
+ }
+
+ public void removeButtons(Graphics g) {
+ drawBox(g,Color.lightGray);
+ }
+
+ public void draw(Graphics g) {
+ drawBox(g,Color.lightGray);
+ g.setColor(Color.black);
+ Enumeration e1=getChildren();
+ while (e1.hasMoreElements()) {
+ Vertex v=(Vertex)(e1.nextElement());
+ if (!v.isDummy())
+ g.drawLine(getX(),getY()+gra.box_height,v.getX(),v.getY());
+ }
+ }
+
+ public boolean contains(int x,int y) {
+ return (x>=leftX() && x<=rightX() && y>=getY() &&
+ y<=getY()+gra.box_height);
+ }
+
+ public boolean leftButton(int x,int y) {
+ return contains(x,y) && x<=leftX()+gra.box_height && getParents().hasMoreElements() && getNumber()>=0;
+ }
+
+ public boolean rightButton(int x,int y) {
+ return contains(x,y) && x>=rightX()-gra.box_height && getChildren().hasMoreElements() && getNumber()>=0;
+ }
+
+ public void drawButtons(Graphics g) {
+ if (getNumber()<0) return;
+
+ int l=gra.box_height*2/3,d=gra.box_height/6;
+ int up_x[] = { leftX()+d , leftX()+d+l/2 , leftX()+d+l };
+ int up_y[] = { getY()+d+l , getY()+d , getY()+d+l };
+ int down_x[] = { rightX()-d-l , rightX()-d-l/2 , rightX()-d };
+ int down_y[] = { getY()+d , getY()+d+l , getY()+d };
+
+ if (getParents().hasMoreElements()) {
+ g.setColor(Color.gray);
+ g.fillRect(leftX()+1,getY()+1,gra.box_height-1,gra.box_height-1);
+ g.setColor(getUp()!=null ? Color.red : Color.green);
+ g.fillPolygon(up_x,up_y,3);
+ }
+ if (getChildren().hasMoreElements()) {
+ g.setColor(Color.gray);
+ g.fillRect(rightX()+1-gra.box_height,getY()+1,gra.box_height,gra.box_height-1);
+ g.setColor(getDown()!=null ? Color.red : Color.green);
+ g.fillPolygon(down_x,down_y,3);
+ }
+ g.setColor(Color.black);
+ }
+
+ public void PS(PrintStream p) {
+ p.print(leftX()+" "+getY()+" "+gra.box_width+" "+
+ gra.box_height+" (");
+ for (int i=0;i<label.length();i++)
+ {
+ if (("()\\").indexOf(label.charAt(i))>=0)
+ p.print("\\");
+ p.print(label.charAt(i));
+ }
+ p.println(") b");
+
+ Enumeration e1=getChildren();
+ while (e1.hasMoreElements()) {
+ Vertex v=(Vertex)(e1.nextElement());
+ if (!v.isDummy())
+ p.println("n "+getX()+" "+(getY()+gra.box_height)+
+ " m "+v.getX()+" "+v.getY()+" l s");
+ }
+ }
+}
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/lib/browser/GraphBrowser/Region.java Wed Aug 06 00:06:47 1997 +0200
@@ -0,0 +1,90 @@
+/***************************************************************************
+ Title: GraphBrowser/Region.java
+ ID: $Id$
+ Author: Stefan Berghofer, TU Muenchen
+ Copyright 1997 TU Muenchen
+
+ This is an auxiliary class which is used by the layout algorithm when
+ calculating coordinates with the "pendulum method". A "region" is a
+ group of nodes which "stick together".
+***************************************************************************/
+
+package GraphBrowser;
+
+import java.util.*;
+
+class Region {
+ Vector vertices=new Vector(10,10);
+ Graph gra;
+
+ public Region(Graph g) { gra=g; }
+
+ public void addVertex(Vertex v) {
+ vertices.addElement(v);
+ }
+
+ public Enumeration getVertices() {
+ return vertices.elements();
+ }
+
+ public int pred_deflection() {
+ float d1=0;
+ int n=0;
+ Enumeration e1=vertices.elements();
+ while (e1.hasMoreElements()) {
+ float d2=0;
+ int p=0;
+ n++;
+ Vertex v=(Vertex)(e1.nextElement());
+ Enumeration e2=v.getParents();
+ while (e2.hasMoreElements()) {
+ p++;
+ d2+=((Vertex)(e2.nextElement())).getX()-v.getX();
+ }
+ if (p>0) d1+=d2/p;
+ }
+ return (int)(Math.round(d1/n));
+ }
+
+ public int succ_deflection() {
+ float d1=0;
+ int n=0;
+ Enumeration e1=vertices.elements();
+ while (e1.hasMoreElements()) {
+ float d2=0;
+ int p=0;
+ n++;
+ Vertex v=(Vertex)(e1.nextElement());
+ Enumeration e2=v.getChildren();
+ while (e2.hasMoreElements()) {
+ p++;
+ d2+=((Vertex)(e2.nextElement())).getX()-v.getX();
+ }
+ if (p>0) d1+=d2/p;
+ }
+ return (int)(Math.round(d1/n));
+ }
+
+ public void move(int x) {
+ Enumeration e1=vertices.elements();
+ while (e1.hasMoreElements()) {
+ Vertex v=(Vertex)(e1.nextElement());
+ v.setX(v.getX()+x);
+ }
+ }
+
+ public void combine(Region r2) {
+ Enumeration e1=r2.getVertices();
+ while (e1.hasMoreElements()) addVertex((Vertex)(e1.nextElement()));
+ }
+
+ public int spaceBetween(Region r2) {
+ return ((Vertex)(r2.getVertices().nextElement())).leftX()-
+ ((Vertex)(vertices.lastElement())).rightX()-
+ gra.box_hspace+gra.box_width;
+ }
+
+ public boolean touching(Region r2) {
+ return spaceBetween(r2)==0;
+ }
+}
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/lib/browser/GraphBrowser/Spline.java Wed Aug 06 00:06:47 1997 +0200
@@ -0,0 +1,121 @@
+/***************************************************************************
+ Title: GraphBrowser/Spline.java
+ ID: $Id$
+ Author: Stefan Berghofer, TU Muenchen
+ Copyright 1997 TU Muenchen
+
+ This class is used for drawing spline curves (which are not yet
+ supported by the Java AWT).
+***************************************************************************/
+
+package GraphBrowser;
+
+import java.awt.*;
+import java.util.*;
+import java.io.*;
+
+class SplineSection {
+
+ /*** Section of a spline function ***/
+
+ double x_b,x_c,x_d;
+ double y_b,y_c,y_d;
+ int dx,dy;
+
+ public SplineSection(double xb,double xc,double xd,
+ double yb,double yc,double yd,int dx2,int dy2) {
+ x_b=xb;x_c=xc;x_d=xd;
+ y_b=yb;y_c=yc;y_d=yd;
+ dx=dx2;dy=dy2;
+ }
+
+ public Point draw(Graphics g,Point s) {
+ double m;
+ int s_x,s_y,e_x=0,e_y=0;
+ int x,y;
+
+ s_x=s.x;s_y=s.y;
+ if (dx>=dy) {
+ if (dx==0) return s;
+ m=1/((double)dx);
+ for (x=0;x<dx;x++) {
+ e_x=(int)(Math.round((x_b*x*m+x_c)*x*m+x_d));
+ e_y=(int)(Math.round((y_b*x*m+y_c)*x*m+y_d));
+ g.drawLine(s_x,s_y,e_x,e_y);
+ s_x=e_x;s_y=e_y;
+ }
+ } else {
+ m=1/((double)dy);
+ for (y=0;y<dy;y++) {
+ e_x=(int)(Math.round((x_b*y*m+x_c)*y*m+x_d));
+ e_y=(int)(Math.round((y_b*y*m+y_c)*y*m+y_d));
+ g.drawLine(s_x,s_y,e_x,e_y);
+ s_x=e_x;s_y=e_y;
+ }
+ }
+ return new Point(e_x,e_y);
+ }
+}
+
+public class Spline {
+
+ Vector sections;
+ Vector points;
+ Point start,end;
+
+ public Spline(Vector pts) {
+ int i;
+ double d0,d1,d2,d3;
+ Point p0,p1,p2;
+ SplineSection s;
+
+ start=(Point)(pts.firstElement());
+ end=(Point)(pts.lastElement());
+
+ sections=new Vector(10,10);
+ for (i=1;i<=pts.size()-4;i+=3) {
+ p0=(Point)(pts.elementAt(i));
+ p1=(Point)(pts.elementAt(i+1));
+ p2=(Point)(pts.elementAt(i+2));
+ s=new SplineSection(
+ (double)(p2.x-2*p1.x+p0.x),
+ 2.0*(p1.x-p0.x),
+ (double)(p0.x),
+
+ (double)(p2.y-2*p1.y+p0.y),
+ 2.0*(p1.y-p0.y),
+ (double)(p0.y),
+
+ Math.abs(p2.x-p0.x),
+ Math.abs(p2.y-p0.y)
+ );
+
+ sections.addElement(s);
+ }
+ points=pts;
+ }
+
+ public void draw(Graphics g) {
+ Enumeration e1=sections.elements();
+ Point p=start;
+
+ while (e1.hasMoreElements())
+ p=((SplineSection)(e1.nextElement())).draw(g,p);
+ g.drawLine(p.x,p.y,end.x,end.y);
+ }
+
+ public void PS(PrintStream p) {
+ Point p0,p1,p2;
+ int i;
+
+ p.println("n "+start.x+" "+start.y+" m");
+ for (i=1;i<=points.size()-4;i+=3) {
+ p0=(Point)(points.elementAt(i));
+ p1=(Point)(points.elementAt(i+1));
+ p2=(Point)(points.elementAt(i+2));
+ p.println(p0.x+" "+p0.y+" l");
+ p.println(p0.x+" "+p0.y+" "+p1.x+" "+p1.y+" "+p2.x+" "+p2.y+" c");
+ }
+ p.println(end.x+" "+end.y+" l s");
+ }
+}
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/lib/browser/GraphBrowser/TreeBrowser.java Wed Aug 06 00:06:47 1997 +0200
@@ -0,0 +1,70 @@
+/***************************************************************************
+ Title: GraphBrowser/TreeBrowser.java
+ ID: $Id$
+ Author: Stefan Berghofer, TU Muenchen
+ Copyright 1997 TU Muenchen
+
+ This class defines the browser window which is used to display directory
+ trees. It contains methods for handling events.
+***************************************************************************/
+
+package GraphBrowser;
+
+import java.awt.*;
+import awtUtilities.ScrollCanvas;
+import java.util.*;
+
+
+public class TreeBrowser extends ScrollCanvas
+{
+ TreeNode t;
+ TreeNode selected;
+ GraphView gv;
+ long timestamp;
+
+ public TreeBrowser(TreeNode tn,GraphView gr) {
+ t=tn;gv=gr;
+ }
+
+ public boolean mouseDown(Event e,int x,int y)
+ {
+ TreeNode l=t.lookup(y);
+
+ if (l!=null)
+ {
+ if (l.select()) {
+ Vector v=new Vector(10,10);
+ t.collapsedDirectories(v);
+ gv.collapseDir(v);
+ gv.relayout();
+ } else {
+ Vertex vx=gv.getGraph().getVertexByNum(l.getNumber());
+ gv.focusToVertex(l.getNumber());
+ vx=gv.getOriginalGraph().getVertexByNum(l.getNumber());
+ if (e.when-timestamp < 400 && !(vx.getPath().equals("")))
+ gv.getBrowser().viewFile(vx.getPath());
+ timestamp=e.when;
+
+ }
+ selected=l;repaint();
+
+ }
+ return true;
+ }
+
+ public void selectNode(TreeNode nd) {
+ Vector v=new Vector(10,10);
+ nd.select();
+ t.collapsedDirectories(v);
+ gv.collapseDir(v);
+ gv.relayout();
+ selected=nd;repaint();
+ }
+
+ public void paintCanvas(Graphics g)
+ {
+ Dimension d=t.draw(g,5,5,selected);
+ set_size(5+d.width,5+d.height);
+ }
+}
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/lib/browser/GraphBrowser/TreeNode.java Wed Aug 06 00:06:47 1997 +0200
@@ -0,0 +1,187 @@
+/***************************************************************************
+ Title: GraphBrowser/TreeNode.java
+ ID: $Id$
+ Author: Stefan Berghofer, TU Muenchen
+ Copyright 1997 TU Muenchen
+
+ This class contains methods for storing and manipulating directory
+ trees (e.g. collapsing / uncollapsing directory branches).
+***************************************************************************/
+
+package GraphBrowser;
+
+import java.awt.*;
+import java.util.*;
+
+class Directory {
+ TreeNode node;
+ String name;
+ Vector collapsed;
+
+ public Directory(TreeNode nd,String n,Vector col) {
+ collapsed=col;
+ name=n;
+ node=nd;
+ }
+
+ public TreeNode getNode() { return node; }
+
+ public String getName() { return name; }
+
+ public Vector getCollapsed() { return collapsed; }
+}
+
+public class TreeNode
+{
+ static Font f=new Font("Helvetica",Font.PLAIN,15);
+ int starty,endy,number;
+ String name,path;
+
+ Vector leaves=new Vector(10,10);
+ boolean unfold=false;
+
+ public void insertNode(String n,String d,String p,int num,boolean u) {
+ if (d.length()==0) {
+ leaves.addElement(new TreeNode(n,p,num));
+ unfold=unfold||u;
+ } else {
+ unfold=unfold||u;
+ String str1,str2;
+ if (d.indexOf('/')<0) {
+ str1=d;str2="";
+ } else {
+ str1=d.substring(0,d.indexOf('/'));
+ str2=d.substring(d.indexOf('/')+1);
+ }
+
+ Enumeration e1=leaves.elements();
+ TreeNode nd=null;
+
+ while (e1.hasMoreElements()) {
+ TreeNode nd2=(TreeNode)(e1.nextElement());
+ if (nd2.name.equals(str1)) {
+ nd=nd2;break;
+ }
+ }
+ if (nd==null) {
+ nd=new TreeNode(str1,"",-1);
+ leaves.addElement(nd);
+ }
+ nd.insertNode(n,str2,p,num,u);
+ }
+ }
+
+ public TreeNode(String n,String p,int num) {
+ name=n;
+ path=p;
+ number=num;
+ }
+
+ public TreeNode(String n,String p,int num,boolean u) {
+ this(n,p,num);
+ unfold=u;
+ }
+
+ public int getNumber() { return number; }
+
+ public TreeNode lookup(int y)
+ {
+ if (y>=starty && y<endy) return this;
+ else
+ if (unfold)
+ for (int i=0;i<leaves.size();i++)
+ {
+ TreeNode t=((TreeNode)leaves.elementAt(i)).lookup(y);
+ if (t!=null) return t;
+ }
+ return null;
+ }
+
+ public boolean select()
+ {
+ if (!leaves.isEmpty()) {
+ if (unfold) collapse();
+ else unfold=true;
+ return true;
+ }
+ return false;
+ }
+
+ public void collapse()
+ {
+ unfold=false;
+ /*
+ for(int i=0;i<leaves.size();i++)
+ ((Tree)leaves.elementAt(i)).collapse();
+ */
+ }
+
+ void collapsedNodes(Vector v) {
+ if (number>=0) v.addElement(new Integer(number));
+ Enumeration e1=leaves.elements();
+ while (e1.hasMoreElements())
+ ((TreeNode)(e1.nextElement())).collapsedNodes(v);
+ }
+
+ public void collapsedDirectories(Vector v) {
+ if (!unfold) {
+ Vector v2=new Vector(10,10);
+ v.addElement(new Directory(this,name,v2));
+ collapsedNodes(v2);
+ } else {
+ Enumeration e1=leaves.elements();
+ while (e1.hasMoreElements()) {
+ TreeNode tn=(TreeNode)(e1.nextElement());
+ if (!tn.leaves.isEmpty())
+ tn.collapsedDirectories(v);
+ }
+ }
+ }
+
+ public Dimension draw(Graphics g,int x,int y,TreeNode t)
+ {
+ FontMetrics fm=g.getFontMetrics(f);
+ g.setFont(f);
+ int h=fm.getHeight();
+ int down_x[]={x,x+h,x+(int)(h/2)};
+ int down_y[]={y,y,y+h};
+ int right_x[]={x,x+h,x};
+ int right_y[]={y,y+(int)(h/2),y+h};
+ int dx=0;
+
+ if (unfold)
+ {
+ g.setColor(Color.green);
+ g.fillPolygon(down_x,down_y,3);
+ g.setColor(Color.black);
+ g.drawString(name,x+h+10,y+fm.getAscent());
+ starty=y;endy=y+h;
+ dx=Math.max(dx,x+h+10+fm.stringWidth(name));
+ y+=h+5;
+ for(int i=0;i<leaves.size();i++)
+ {
+ Dimension d=((TreeNode)leaves.elementAt(i)).draw(g,x+h+10,y,t);
+ y=d.height;
+ dx=Math.max(dx,d.width);
+ }
+ }
+ else
+ {
+ g.setColor(leaves.isEmpty() ? Color.blue : Color.red);
+ g.fillPolygon(right_x,right_y,3);
+ if (this==t && leaves.isEmpty())
+ {
+ g.setColor(Color.white);
+ g.fillRect(x+h+10,y,fm.stringWidth(name),h);
+ }
+ g.setColor(Color.black);
+ g.drawString(name,x+h+10,y+fm.getAscent());
+ starty=y;endy=y+h;
+ dx=Math.max(dx,x+h+10+fm.stringWidth(name));
+ y+=h+5;
+ }
+ return new Dimension(dx,y);
+ }
+}
+
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/lib/browser/GraphBrowser/Vertex.java Wed Aug 06 00:06:47 1997 +0200
@@ -0,0 +1,206 @@
+/***************************************************************************
+ Title: GraphBrowser/Vertex.java
+ ID: $Id$
+ Author: Stefan Berghofer, TU Muenchen
+ Copyright 1997 TU Muenchen
+
+ This class contains attributes and methods common to all kinds of
+ vertices (e.g. coordinates, successors, predecessors).
+***************************************************************************/
+
+package GraphBrowser;
+
+import java.util.*;
+import java.awt.*;
+import java.io.*;
+
+abstract class Vertex {
+ protected static final Font font=new Font("Helvetica",Font.PLAIN,12);
+
+ Vector children=new Vector(10,10);
+ Vector parents=new Vector(10,10);
+ int degree=0;
+ int number=-1;
+ double weight=0;
+ int x,y;
+ Graph gra;
+
+ public abstract Object clone();
+
+ public void setGraph(Graph g) { gra=g; }
+
+ public int countChildren() { return children.size(); }
+
+ /** getInflate returns a vector of vertices which get **/
+ /** inflated again if the user clicks on this vertex **/
+
+ public void setInflate(Vector v) {}
+
+ public Vector getInflate() { return null; }
+
+ /** getUp returns a vector of vertices which get inflated **/
+ /** again, if the user clicks on this vertex's upward arrow **/
+
+ public Vector getUp() { return null; }
+
+ public void setUp(Vector v) {}
+
+ /** getUp returns a vector of vertices which get inflated **/
+ /** again, if the user clicks on this vertex's downward arrow **/
+
+ public Vector getDown() { return null; }
+
+ public void setDown(Vector v) {}
+
+ /** internal number, for decoding / encoding etc. **/
+
+ public int getNumber() { return number; }
+
+ public void setNumber(int n) { number=n; }
+
+ public String getLabel() {return "";}
+
+ public void setLabel(String s) {}
+
+ /** unique identifier **/
+
+ public String getID() {return "";}
+
+ public void setID(String s) {}
+
+ public Dimension getLabelSize(Graphics g) {
+ FontMetrics fm=g.getFontMetrics(font);
+
+ return new Dimension(
+ Math.max(fm.stringWidth("[. . . .]"),fm.stringWidth(getLabel())),
+ fm.getAscent()+fm.getDescent());
+ }
+
+ public String getPath() { return "";}
+
+ public void setPath(String p) {}
+
+ public String getDir() { return ""; }
+
+ public void setDir(String d) {}
+
+ public void setWeight(double w) {weight=w;}
+
+ public double getWeight() {return weight;}
+
+ public void setDegree(int d) { degree=d; }
+
+ public int getDegree() { return degree; }
+
+ public boolean isDummy() { return false; }
+
+ public Enumeration getChildren() {
+ return ((Vector)(children.clone())).elements();
+ }
+
+ public void addChild(Vertex v) {
+ children.addElement(v);
+ v.parents.addElement(this);
+ }
+
+ public void removeChild(Vertex v) {
+ children.removeElement(v);
+ v.parents.removeElement(this);
+ }
+
+ public boolean isChild(Vertex v) {
+ return children.indexOf(v)>=0;
+ }
+
+ public boolean isParent(Vertex v) {
+ return parents.indexOf(v)>=0;
+ }
+
+ public Enumeration getParents() {
+ return ((Vector)(parents.clone())).elements();
+ }
+
+ public void addParent(Vertex v) {
+ parents.addElement(v);
+ v.children.addElement(this);
+ }
+
+ public void removeParent(Vertex v) {
+ parents.removeElement(v);
+ v.children.removeElement(this);
+ }
+
+ /********************************************************************/
+ /* get all predecessor vertices */
+ /********************************************************************/
+
+ public Vector getPreds() {
+ Vector v1=new Vector(10,10);
+ Vertex vx1,vx2;
+ Enumeration e1,e2;
+
+ e1=getParents();
+ while (e1.hasMoreElements()) {
+ vx1=(Vertex)(e1.nextElement());
+ if (v1.indexOf(vx1)<0) v1.addElement(vx1);
+ e2=vx1.getPreds().elements();
+ while (e2.hasMoreElements()) {
+ vx2=(Vertex)(e2.nextElement());
+ if (v1.indexOf(vx2)<0) v1.addElement(vx2);
+ }
+ }
+
+ return v1;
+ }
+
+ /********************************************************************/
+ /* get all successor vertices */
+ /********************************************************************/
+
+ public Vector getSuccs() {
+ Vector v1=new Vector(10,10);
+ Vertex vx1,vx2;
+ Enumeration e1,e2;
+
+ e1=getChildren();
+ while (e1.hasMoreElements()) {
+ vx1=(Vertex)(e1.nextElement());
+ if (v1.indexOf(vx1)<0) v1.addElement(vx1);
+ e2=vx1.getSuccs().elements();
+ while (e2.hasMoreElements()) {
+ vx2=(Vertex)(e2.nextElement());
+ if (v1.indexOf(vx2)<0) v1.addElement(vx2);
+ }
+ }
+
+ return v1;
+ }
+
+ public void setX(int x) {this.x=x;}
+
+ public void setY(int y) {this.y=y;}
+
+ public int getX() {return x;}
+
+ public int getY() {return y;}
+
+ public abstract int leftX();
+
+ public abstract int rightX();
+
+ public abstract void draw(Graphics g);
+
+ public void drawButtons(Graphics g) {}
+
+ public void drawBox(Graphics g,Color boxColor) {}
+
+ public void removeButtons(Graphics g) {}
+
+ public boolean contains(int x,int y) { return false; }
+
+ public boolean leftButton(int x,int y) { return false; }
+
+ public boolean rightButton(int x,int y) { return false; }
+
+ public void PS(PrintStream p) {}
+}
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/lib/browser/awtUtilities/Border.java Wed Aug 06 00:06:47 1997 +0200
@@ -0,0 +1,41 @@
+/***************************************************************************
+ Title: awtUtilities/Border.java
+ ID: $Id$
+ Author: Stefan Berghofer, TU Muenchen
+ Copyright 1997 TU Muenchen
+
+ This class defines a nice 3D border.
+***************************************************************************/
+
+package awtUtilities;
+
+import java.awt.*;
+
+public class Border extends Panel {
+ int bs;
+
+ public Insets insets() {
+ return new Insets(bs*3/2,bs*3/2,bs*3/2,bs*3/2);
+ }
+
+ public Border(Component comp,int s) {
+ setLayout(new GridLayout(1,1));
+ add(comp);
+ bs=s;
+ }
+
+ public void paint(Graphics g) {
+ int w=size().width;
+ int h=size().height;
+ int x1[]={0,bs,w-bs,w}, y1[]={0,bs,bs,0};
+ int x2[]={w,w-bs,w-bs,w}, y2[]={0,bs,h-bs,h};
+ int y3[]={h,h-bs,h-bs,h};
+
+ g.setColor(new Color(224,224,224));
+ g.fillPolygon(y1,y2,4);
+ g.fillPolygon(x1,y1,4);
+ g.setColor(Color.gray);
+ g.fillPolygon(x2,y2,4);
+ g.fillPolygon(x1,y3,4);
+ }
+}
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/lib/browser/awtUtilities/MessageDialog.java Wed Aug 06 00:06:47 1997 +0200
@@ -0,0 +1,54 @@
+/***************************************************************************
+ Title: awtUtilities/MessageDialog.java
+ ID: $Id$
+ Author: Stefan Berghofer, TU Muenchen
+ Copyright 1997 TU Muenchen
+
+ This class defines a dialog window for displaying messages and buttons.
+***************************************************************************/
+
+package awtUtilities;
+
+import java.awt.*;
+
+public class MessageDialog extends Dialog {
+ String txt;
+
+ public String getText() { return txt; }
+
+ public boolean action(Event evt, Object arg) {
+ if (evt.target instanceof Button) {
+ txt=(String)arg;
+ hide();
+ return true;
+ } else return false;
+ }
+
+ public MessageDialog(Frame parent,String title,String text,String []buttons) {
+ super(parent,title,true);
+ int i;
+ Panel p1=new Panel(),p2=new Panel();
+ p1.setLayout(new FlowLayout(FlowLayout.CENTER,0,0));
+ p2.setLayout(new FlowLayout());
+ setFont(new Font("Helvetica", Font.PLAIN, 14));
+ setLayout(new GridLayout(2,1));
+
+ while (true) {
+ int pos=text.indexOf(' ');
+ if (pos<0) {
+ p1.add(new Label(text));
+ break;
+ } else {
+ p1.add(new Label(text.substring(0,pos)));
+ if (pos+1==text.length())
+ break;
+ else
+ text=text.substring(pos+1);
+ }
+ }
+
+ add(p1);add(p2);
+ for (i=0;i<buttons.length;i++)
+ p2.add(new Button(buttons[i]));
+ }
+}
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/lib/browser/awtUtilities/ScrollCanvas.java Wed Aug 06 00:06:47 1997 +0200
@@ -0,0 +1,169 @@
+/***************************************************************************
+ Title: awtUtilities/ScrollCanvas.java
+ ID: $Id$
+ Author: Stefan Berghofer, TU Muenchen
+ Copyright 1997 TU Muenchen
+
+ This class contains defines a window with scrollbars, which is not
+ supported by the 1.0.2 version of the JDK. To use this class, simply
+ derive your own class from it and overwrite the paintCanvas method.
+ When a repaint event occurs, ScrollCanvas automatically calls the
+ paintCanvas method. The user doesn't have to take care of transposing
+ mouse or graphics coordinates.
+ Note: In later versions of the JDK, a ScrollPane class will be provided,
+ which can be used instead.
+***************************************************************************/
+
+package awtUtilities;
+
+import java.awt.*;
+
+class DummyCanvas extends Canvas {
+ ScrollCanvas parent;
+
+ public DummyCanvas(ScrollCanvas p) {
+ parent=p;
+ }
+
+ public void paint(Graphics g) {
+ parent.paint(g);
+ }
+
+ public void update(Graphics g) {
+ parent.update(g);
+ }
+}
+
+public class ScrollCanvas extends Panel
+{
+ Scrollbar scrollv,scrollh;
+ Canvas can;
+ Image img=null;
+ int offset_x=0,offset_y=0;
+ int size_x=100,size_y=100;
+ int old_x=0,old_y=0;
+
+ public boolean handleEvent(Event evt)
+ {
+ evt.x+=offset_x;
+ evt.y+=offset_y;
+ if (evt.target instanceof Scrollbar)
+ {
+ offset_x=scrollh.getValue();
+ offset_y=scrollv.getValue();
+ Graphics g=can.getGraphics();
+ if (old_x!=size_x || old_y!=size_y)
+ update(g);
+ else {
+ g.translate(-offset_x,-offset_y);
+ g.drawImage(img,0,0,this);
+ }
+ return true;
+ }
+ else return super.handleEvent(evt);
+ }
+
+ public void adjust_scrollbars()
+ {
+ int viewport_v=can.size().height;
+ int viewport_h=can.size().width;
+ int value_v=scrollv.getValue();
+ int value_h=scrollh.getValue();
+
+ scrollv.setValues(value_v,viewport_v,0,size_y-viewport_v);
+ scrollh.setValues(value_h,viewport_h,0,size_x-viewport_h);
+ scrollv.setLineIncrement(viewport_v/20);
+ scrollv.setPageIncrement(viewport_v);
+ scrollh.setLineIncrement(viewport_h/20);
+ scrollh.setPageIncrement(viewport_h);
+ offset_x=scrollh.getValue();
+ offset_y=scrollv.getValue();
+ }
+
+ public void set_size(int x,int y)
+ {
+ size_x=x;size_y=y;
+ adjust_scrollbars();
+ }
+
+ public void focus_to(int x,int y) {
+ offset_x=Math.min(scrollh.getMaximum(),Math.max(0,x-can.size().width/2));
+ offset_y=Math.min(scrollv.getMaximum(),Math.max(0,y-can.size().height/2));
+
+ scrollh.setValue(offset_x);
+ scrollv.setValue(offset_y);
+ Graphics g=can.getGraphics();
+ if (old_x!=size_x || old_y!=size_y)
+ update(g);
+ else {
+ g.translate(-offset_x,-offset_y);
+ g.drawImage(img,0,0,this);
+ }
+ }
+
+ public void update(Graphics g) {
+ g=can.getGraphics();
+ int viewport_v=can.size().height;
+ int viewport_h=can.size().width;
+ int img_x=Math.max(viewport_h,size_x+1);
+ int img_y=Math.max(viewport_v,size_y+1);
+
+ old_x=size_x;old_y=size_y;
+ img=createImage(img_x,img_y);
+ Graphics g2=img.getGraphics();
+ g2.setColor(Color.lightGray);
+ g2.fillRect(0,0,img_x,img_y);
+ g2.setColor(Color.black);
+ paintCanvas(g2);
+ adjust_scrollbars();
+ g.translate(-offset_x,-offset_y);
+ g.drawImage(img,0,0,this);
+ }
+
+ public void paint(Graphics g)
+ {
+ if (img!=null && old_x==size_x && old_y==size_y) {
+ g=can.getGraphics();
+ adjust_scrollbars();
+ g.translate(-offset_x,-offset_y);
+ g.drawImage(img,0,0,this);
+ } else update(g);
+ }
+
+ public Graphics getGraphics() {
+ Graphics g=can.getGraphics();
+
+ g.translate(-offset_x,-offset_y);
+ return g;
+ }
+
+ public void paintCanvas(Graphics g)
+ {}
+
+ public ScrollCanvas()
+ {
+ can=new DummyCanvas(this);
+ GridBagLayout gridbag = new GridBagLayout();
+ GridBagConstraints c = new GridBagConstraints();
+ scrollv=new Scrollbar(Scrollbar.VERTICAL);
+ scrollh=new Scrollbar(Scrollbar.HORIZONTAL);
+
+ setLayout(gridbag);
+ c.weightx = 1.0;
+ c.weighty = 1.0;
+ c.gridwidth=1;
+ c.fill = GridBagConstraints.BOTH;
+ gridbag.setConstraints(can,c);
+ add(can);
+ c.weightx=0;
+ c.weighty=0;
+ c.gridwidth = GridBagConstraints.REMAINDER;
+ c.fill = GridBagConstraints.VERTICAL;
+ gridbag.setConstraints(scrollv,c);
+ add(scrollv);
+ c.gridwidth = 1;
+ c.fill = GridBagConstraints.HORIZONTAL;
+ gridbag.setConstraints(scrollh,c);
+ add(scrollh);
+ }
+}
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/lib/browser/awtUtilities/TextFrame.java Wed Aug 06 00:06:47 1997 +0200
@@ -0,0 +1,28 @@
+/***************************************************************************
+ Title: Graph/TextFrame.java
+ ID: $Id$
+ Author: Stefan Berghofer, TU Muenchen
+ Copyright 1997 TU Muenchen
+
+ This class defines a simple text viewer.
+***************************************************************************/
+
+package awtUtilities;
+
+import java.awt.*;
+
+public class TextFrame extends Frame {
+ public boolean action(Event evt,Object obj) {
+ if (evt.target instanceof Button)
+ hide();
+ return true;
+ }
+
+ public TextFrame(String title,String text) {
+ super(title);
+ TextArea ta=new TextArea(text,200,80);
+ ta.setEditable(false);
+ add("Center",ta);
+ add("South",new Button("Dismiss"));
+ }
+}