diff --git a/src/Tools/GraphBrowser/awtUtilities/Border.java b/src/Tools/GraphBrowser/awt/Border.java
rename from src/Tools/GraphBrowser/awtUtilities/Border.java
rename to src/Tools/GraphBrowser/awt/Border.java
--- a/src/Tools/GraphBrowser/awtUtilities/Border.java
+++ b/src/Tools/GraphBrowser/awt/Border.java
@@ -1,39 +1,39 @@
 /***************************************************************************
-  Title:      awtUtilities/Border.java
+  Title:      awt/Border.java
   Author:     Stefan Berghofer, TU Muenchen
 
   This class defines a nice 3D border.
 ***************************************************************************/
 
-package awtUtilities;
+package isabelle.awt;
 
 import java.awt.*;
 
 public class Border extends Panel {
 	int bs;
 
 	public Insets getInsets() {
 		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 = getSize().width;
 		int h = getSize().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);
 	}
 }
diff --git a/src/Tools/GraphBrowser/awtUtilities/MessageDialog.java b/src/Tools/GraphBrowser/awt/MessageDialog.java
rename from src/Tools/GraphBrowser/awtUtilities/MessageDialog.java
rename to src/Tools/GraphBrowser/awt/MessageDialog.java
--- a/src/Tools/GraphBrowser/awtUtilities/MessageDialog.java
+++ b/src/Tools/GraphBrowser/awt/MessageDialog.java
@@ -1,53 +1,53 @@
 /***************************************************************************
-  Title:      awtUtilities/MessageDialog.java
+  Title:      awt/MessageDialog.java
   Author:     Stefan Berghofer, TU Muenchen
 
   This class defines a dialog window for displaying messages and buttons.
 ***************************************************************************/
 
-package awtUtilities;
+package isabelle.awt;
 
 import java.awt.*;
 import java.awt.event.*;
 
 public class MessageDialog extends Dialog implements ActionListener {
 	String txt;
 
 	public String getText() { return txt; }
 
 	public void actionPerformed(ActionEvent evt) {
 		txt = evt.getActionCommand();
 		setVisible(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++) {
 			Button bt = new Button(buttons[i]);
 			p2.add(bt);
 			bt.addActionListener(this);
 		}
 	}
 }
diff --git a/src/Tools/GraphBrowser/awtUtilities/TextFrame.java b/src/Tools/GraphBrowser/awt/TextFrame.java
rename from src/Tools/GraphBrowser/awtUtilities/TextFrame.java
rename to src/Tools/GraphBrowser/awt/TextFrame.java
--- a/src/Tools/GraphBrowser/awtUtilities/TextFrame.java
+++ b/src/Tools/GraphBrowser/awt/TextFrame.java
@@ -1,27 +1,27 @@
 /***************************************************************************
-  Title:      Graph/TextFrame.java
+  Title:      awt/TextFrame.java
   Author:     Stefan Berghofer, TU Muenchen
 
   This class defines a simple text viewer.
 ***************************************************************************/
 
-package awtUtilities;
+package isabelle.awt;
 
 import java.awt.*;
 import java.awt.event.*;
 
 public class TextFrame extends Frame implements ActionListener {
 	public void actionPerformed(ActionEvent evt) {
 		setVisible(false);
 	}
 
 	public TextFrame(String title,String text) {
 		super(title);
 		TextArea ta = new TextArea(text,200,80);
 		Button bt = new Button("Dismiss");
 		bt.addActionListener(this);
 		ta.setEditable(false);
 		add("Center", ta);
 		add("South", bt);
 	}
 }
diff --git a/src/Tools/GraphBrowser/etc/build.props b/src/Tools/GraphBrowser/etc/build.props
--- a/src/Tools/GraphBrowser/etc/build.props
+++ b/src/Tools/GraphBrowser/etc/build.props
@@ -1,26 +1,26 @@
 description = graph browser
 lib = $ISABELLE_HOME/lib/classes
-name = GraphBrowser
+name = isabelle_graphbrowser
 javac_options = -source 7 -target 7
 sources = \
-  GraphBrowser/AWTFontMetrics.java \
-  GraphBrowser/AbstractFontMetrics.java \
-  GraphBrowser/Box.java \
-  GraphBrowser/Console.java \
-  GraphBrowser/DefaultFontMetrics.java \
-  GraphBrowser/Directory.java \
-  GraphBrowser/DummyVertex.java \
-  GraphBrowser/Graph.java \
-  GraphBrowser/GraphBrowser.java \
-  GraphBrowser/GraphBrowserFrame.java \
-  GraphBrowser/GraphView.java \
-  GraphBrowser/NormalVertex.java \
-  GraphBrowser/ParseError.java \
-  GraphBrowser/Region.java \
-  GraphBrowser/Spline.java \
-  GraphBrowser/TreeBrowser.java \
-  GraphBrowser/TreeNode.java \
-  GraphBrowser/Vertex.java \
-  awtUtilities/Border.java \
-  awtUtilities/MessageDialog.java \
-  awtUtilities/TextFrame.java
+  awt/Border.java \
+  awt/MessageDialog.java \
+  awt/TextFrame.java \
+  graphbrowser/AWTFontMetrics.java \
+  graphbrowser/AbstractFontMetrics.java \
+  graphbrowser/Box.java \
+  graphbrowser/Console.java \
+  graphbrowser/DefaultFontMetrics.java \
+  graphbrowser/Directory.java \
+  graphbrowser/DummyVertex.java \
+  graphbrowser/Graph.java \
+  graphbrowser/GraphBrowser.java \
+  graphbrowser/GraphBrowserFrame.java \
+  graphbrowser/GraphView.java \
+  graphbrowser/NormalVertex.java \
+  graphbrowser/ParseError.java \
+  graphbrowser/Region.java \
+  graphbrowser/Spline.java \
+  graphbrowser/TreeBrowser.java \
+  graphbrowser/TreeNode.java \
+  graphbrowser/Vertex.java
diff --git a/src/Tools/GraphBrowser/GraphBrowser/AWTFontMetrics.java b/src/Tools/GraphBrowser/graphbrowser/AWTFontMetrics.java
rename from src/Tools/GraphBrowser/GraphBrowser/AWTFontMetrics.java
rename to src/Tools/GraphBrowser/graphbrowser/AWTFontMetrics.java
--- a/src/Tools/GraphBrowser/GraphBrowser/AWTFontMetrics.java
+++ b/src/Tools/GraphBrowser/graphbrowser/AWTFontMetrics.java
@@ -1,31 +1,31 @@
 /***************************************************************************
-  Title:      GraphBrowser/AWTFontMetrics.java
+  Title:      graphbrowser/AWTFontMetrics.java
   Author:     Gerwin Klein, TU Muenchen
 
   AbstractFontMetrics from the AWT for graphics mode.
   
 ***************************************************************************/
 
-package GraphBrowser;
+package isabelle.graphbrowser;
 
 import java.awt.FontMetrics;
 
 public class AWTFontMetrics implements AbstractFontMetrics {
   private FontMetrics fontMetrics;
 
   public AWTFontMetrics(FontMetrics m) {
     fontMetrics = m;
   }
 
   public int stringWidth(String str) {
     return fontMetrics.stringWidth(str);
   }
 
   public int getAscent() {
     return fontMetrics.getAscent();
   }
 
   public int getDescent() {
     return fontMetrics.getDescent();
   }
 }
diff --git a/src/Tools/GraphBrowser/GraphBrowser/AbstractFontMetrics.java b/src/Tools/GraphBrowser/graphbrowser/AbstractFontMetrics.java
rename from src/Tools/GraphBrowser/GraphBrowser/AbstractFontMetrics.java
rename to src/Tools/GraphBrowser/graphbrowser/AbstractFontMetrics.java
--- a/src/Tools/GraphBrowser/GraphBrowser/AbstractFontMetrics.java
+++ b/src/Tools/GraphBrowser/graphbrowser/AbstractFontMetrics.java
@@ -1,16 +1,16 @@
 /***************************************************************************
-  Title:      GraphBrowser/AWTFontMetrics.java
+  Title:      graphbrowser/AWTFontMetrics.java
   Author:     Gerwin Klein, TU Muenchen
 
   AbstractFontMetrics avoids dependency on java.awt.FontMetrics in 
   batch mode.
   
 ***************************************************************************/
 
-package GraphBrowser;
+package isabelle.graphbrowser;
 
 public interface AbstractFontMetrics {
   public int stringWidth(String str);
   public int getAscent();
   public int getDescent();
 }
diff --git a/src/Tools/GraphBrowser/GraphBrowser/Box.java b/src/Tools/GraphBrowser/graphbrowser/Box.java
rename from src/Tools/GraphBrowser/GraphBrowser/Box.java
rename to src/Tools/GraphBrowser/graphbrowser/Box.java
--- a/src/Tools/GraphBrowser/GraphBrowser/Box.java
+++ b/src/Tools/GraphBrowser/graphbrowser/Box.java
@@ -1,20 +1,20 @@
 /***************************************************************************
-  Title:      GraphBrowser/Box.java
+  Title:      graphbrowser/Box.java
   Author:     Gerwin Klein, TU Muenchen
 
   A box with width and height. Used instead of java.awt.Dimension for 
   batch mode.
 
 ***************************************************************************/
 
-package GraphBrowser;
+package isabelle.graphbrowser;
 
 public class Box {
   public int width;
   public int height;
 
   public Box(int w, int h) {
     this.width = w;
     this.height = h;
   }
 }
diff --git a/src/Tools/GraphBrowser/GraphBrowser/Console.java b/src/Tools/GraphBrowser/graphbrowser/Console.java
rename from src/Tools/GraphBrowser/GraphBrowser/Console.java
rename to src/Tools/GraphBrowser/graphbrowser/Console.java
--- a/src/Tools/GraphBrowser/GraphBrowser/Console.java
+++ b/src/Tools/GraphBrowser/graphbrowser/Console.java
@@ -1,89 +1,89 @@
 /***************************************************************************
-  Title:      GraphBrowser/Console.java
+  Title:      graphbrowser/Console.java
   Author:     Gerwin Klein, TU Muenchen
   Options:    :tabSize=2:
 
   This is the graph browser's main class when run as a console application.
   It duplicates some logic from GraphBrowser and GraphView.
   It does so to remove dependency on AWT.
 
 ***************************************************************************/
 
-package GraphBrowser;
+package isabelle.graphbrowser;
 
 import java.io.*;
 import java.util.*;
 
 public class Console {
 	Graph g;
 	String gfname;  
 
   public Console(String name) {
     gfname = name;
   }
 
 	public void PS(String fname, boolean printable) throws IOException {
     g.layout(null);
 		g.PS(fname,printable);
 	}
 
 
 	public void collapseNodes(Vector collapsedDir) { 
 		Enumeration e1=collapsedDir.elements();
 		Graph gra=(Graph)(g.clone());
 
 		while (e1.hasMoreElements()) {
 			Directory d=(Directory)(e1.nextElement());
 			Vector v=gra.decode(d.getCollapsed());
 			if (!v.isEmpty())
 				gra.collapse(v,"["+d.getName()+"]",d.getCollapsed());
 		}
     
     g = gra;
 	}
 
 
 	public void initBrowser(InputStream is) {
 		try {
 			TreeNode tn = new TreeNode("Root", "", -1, true);
       g = new Graph(is, tn);
 			Vector v = new Vector(10,10);
 			tn.collapsedDirectories(v);      
       collapseNodes(v);
 		} catch (IOException exn) {
 			System.err.println("\nI/O error while reading graph file.");
 		} catch (ParseError exn) {
 			System.err.println("\nParse error in graph file:");
 			System.err.println(exn.getMessage());
 			System.err.println("\nSyntax:\n<vertexname> <vertexID> <dirname> [ + ] <path> "+
                          "[ < | > ] [ <vertexID> [ ... [ <vertexID> ] ... ] ] ;");
 		}
 	}
 
 	public static void main(String[] args) {
 		try {
       if (args.length <= 1) {
         System.err.println("Graph and output file expected.");
         return;
       }
 
 			Console console=new Console(args[0]);
       InputStream is=new FileInputStream(args[0]);
       console.initBrowser(is);
       is.close();      
     
       try {
         if (args[1].endsWith(".ps"))
           console.PS(args[1], true);
         else if (args[1].endsWith(".eps"))
           console.PS(args[1], false);
         else
           System.err.println("Unknown file type: " + args[1]);
       } catch (IOException exn) {
         System.err.println("Unable to write file " + args[1]);
       }
 		} catch (IOException exn) {
 			System.err.println("Can't open graph file "+args[0]);
 		}
 	}
 }
diff --git a/src/Tools/GraphBrowser/GraphBrowser/DefaultFontMetrics.java b/src/Tools/GraphBrowser/graphbrowser/DefaultFontMetrics.java
rename from src/Tools/GraphBrowser/GraphBrowser/DefaultFontMetrics.java
rename to src/Tools/GraphBrowser/graphbrowser/DefaultFontMetrics.java
--- a/src/Tools/GraphBrowser/GraphBrowser/DefaultFontMetrics.java
+++ b/src/Tools/GraphBrowser/graphbrowser/DefaultFontMetrics.java
@@ -1,48 +1,48 @@
 /***************************************************************************
-  Title:      GraphBrowser/DefaultFontMetrics.java
+  Title:      graphbrowser/DefaultFontMetrics.java
   Author:     Stefan Berghofer, TU Muenchen
   Options:    :tabSize=2:
 
   Default font metrics which is used when no graphics context
   is available (batch mode).
 ***************************************************************************/
 
-package GraphBrowser;
+package isabelle.graphbrowser;
 
 public class DefaultFontMetrics implements AbstractFontMetrics {
 
   private static int[] chars =
 	{13, 13, 17, 27, 27, 43, 32, 11, 16, 16, 19, 28, 13, 28, 13, 13, 27,
 	 27, 27, 27, 27, 27, 27, 27, 27, 27, 13, 13, 28, 28, 28, 27, 49, 32,
 	 32, 35, 35, 32, 29, 37, 35, 13, 24, 32, 27, 40, 35, 37, 32, 37, 35,
 	 32, 29, 35, 32, 45, 32, 32, 29, 13, 13, 13, 22, 27, 11, 27, 27, 24,
 	 27, 27, 13, 27, 27, 11, 11, 24, 11, 40, 27, 27, 27, 27, 16, 24, 13,
 	 27, 24, 35, 24, 24, 24, 16, 12, 16, 28};
 
   private int size;
 
   public DefaultFontMetrics(int size)
   { this.size = size; }
 
   public int getLeading()
   { return 1; }
 
   public int getAscent()
   { return (int)(Math.round(size * 46.0 / 48.0)); }
   
   public int getDescent() 
   { return (int)(Math.round(size * 10.0 / 48.0)); }
   
   public int charWidth(char c) {
     if (c < 32 || c > 126) { return 0; }
     else {
 	    return (int)(Math.round(chars[c - 32] * size / 48.0));
     }
   }
   
   public int stringWidth(String s) {
     int l=0, i;
     for (i=0; i < s.length(); i++) { l += charWidth(s.charAt(i)); }
     return l;
   }
 }
diff --git a/src/Tools/GraphBrowser/GraphBrowser/Directory.java b/src/Tools/GraphBrowser/graphbrowser/Directory.java
rename from src/Tools/GraphBrowser/GraphBrowser/Directory.java
rename to src/Tools/GraphBrowser/graphbrowser/Directory.java
--- a/src/Tools/GraphBrowser/GraphBrowser/Directory.java
+++ b/src/Tools/GraphBrowser/graphbrowser/Directory.java
@@ -1,21 +1,21 @@
-package GraphBrowser;
+package isabelle.graphbrowser;
 
 import java.util.Vector;
 
 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; }
 }
diff --git a/src/Tools/GraphBrowser/GraphBrowser/DummyVertex.java b/src/Tools/GraphBrowser/graphbrowser/DummyVertex.java
rename from src/Tools/GraphBrowser/GraphBrowser/DummyVertex.java
rename to src/Tools/GraphBrowser/graphbrowser/DummyVertex.java
--- a/src/Tools/GraphBrowser/GraphBrowser/DummyVertex.java
+++ b/src/Tools/GraphBrowser/graphbrowser/DummyVertex.java
@@ -1,29 +1,29 @@
 /***************************************************************************
-  Title:      GraphBrowser/DummyVertex.java
+  Title:      graphbrowser/DummyVertex.java
   Author:     Stefan Berghofer, TU Muenchen
   Options:    :tabSize=4:
 
   This class represents a dummy vertex, which is used to simplify the
   layout algorithm.
 ***************************************************************************/
 
-package GraphBrowser;
+package isabelle.graphbrowser;
 
 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) {}
 }
 
diff --git a/src/Tools/GraphBrowser/GraphBrowser/Graph.java b/src/Tools/GraphBrowser/graphbrowser/Graph.java
rename from src/Tools/GraphBrowser/GraphBrowser/Graph.java
rename to src/Tools/GraphBrowser/graphbrowser/Graph.java
--- a/src/Tools/GraphBrowser/GraphBrowser/Graph.java
+++ b/src/Tools/GraphBrowser/graphbrowser/Graph.java
@@ -1,1062 +1,1062 @@
 /***************************************************************************
-  Title:      GraphBrowser/Graph.java
+  Title:      graphbrowser/Graph.java
   Author:     Stefan Berghofer, TU Muenchen
   Options:    :tabSize=4:
 
   This class contains the core of the layout algorithm and methods for
   drawing and PostScript output.
 ***************************************************************************/
 
-package GraphBrowser;
+package isabelle.graphbrowser;
 
 import java.util.*;
 import java.awt.*;
 import java.io.*;
 
 public class Graph {
 	/**** parameters for layout ****/
 
 	public int box_height=0;
 	public int box_height2;
 	public Graphics gfx;
 
 	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(new InputStreamReader(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;
 		h=Integer.MIN_VALUE;
 
 		while (e1.hasMoreElements()) {
 		  Box dim=((Vertex)(e1.nextElement())).getLabelSize(g);
 			h=Math.max(h,dim.height);
 		}
 		box_height=h+4;
 		box_height2=box_height/2;
 		gfx=g;
 	}
 
 	/********************************************************************/
 	/*                       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(Integer.valueOf(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=0;
 			while (e2.hasMoreElements()) {
 				Vertex ve=(Vertex)(e2.nextElement());
 				ve.setX(x+ve.box_width2());
 				ve.setY(y);
 				x+=ve.box_width()+20;
 			}
 			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()+20 < vx.leftX()+d2) ||
 						d>0 && (i==v.size()-1 || ((Vertex)(v.elementAt(i+1))).leftX()-20 > 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=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(Integer.valueOf(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(Integer.valueOf(2));
 								else
 									/* two control points needed */
 									pos.addElement(Integer.valueOf(3));
 								y1=y2+box_height;
 							}
 							x1=x2;
 						} while (vx2.isDummy());
 						pos.addElement(Integer.valueOf(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(Integer.valueOf(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);
 		PrintWriter p = new PrintWriter(f, true);
 
 		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;
 	}
 }
 
diff --git a/src/Tools/GraphBrowser/GraphBrowser/GraphBrowser.java b/src/Tools/GraphBrowser/graphbrowser/GraphBrowser.java
rename from src/Tools/GraphBrowser/GraphBrowser/GraphBrowser.java
rename to src/Tools/GraphBrowser/graphbrowser/GraphBrowser.java
--- a/src/Tools/GraphBrowser/GraphBrowser/GraphBrowser.java
+++ b/src/Tools/GraphBrowser/graphbrowser/GraphBrowser.java
@@ -1,215 +1,215 @@
 /***************************************************************************
-  Title:      GraphBrowser/GraphBrowser.java
+  Title:      graphbrowser/GraphBrowser.java
   Author:     Stefan Berghofer, TU Muenchen
   Options:    :tabSize=4:
 
   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.1.x version of the JDK.
 ***************************************************************************/
 
-package GraphBrowser;
+package isabelle.graphbrowser;
 
 import java.awt.*;
 import java.applet.*;
 import java.io.*;
 import java.util.*;
 import java.net.*;
-import awtUtilities.*;
+import isabelle.awt.*;
 
 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(new Cursor(Cursor.WAIT_CURSOR));
 		}
 	}
 
 	public void showReadyMessage() {
 		if (isApplet)
 			getAppletContext().showStatus("ready !");
 		else {
 			f.setCursor(new Cursor(Cursor.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);
 				Reader rd;
 				BufferedReader br;
 				String line, text = "";
 
 				try {
 					rd = new BufferedReader(new InputStreamReader((new URL(fname)).openConnection().getInputStream()));
 				} catch (Exception exn) {
 					rd = new FileReader(path + fname);
 				}
 				br = new BufferedReader(rd);
 
 				while ((line = br.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];
 						} 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.setSize(500,600);
 				f.show();
 			}
 		} catch (Exception exn) {
 			System.err.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, boolean noAWT) {
 		try {
 			Font font = noAWT ? null : new Font("Helvetica", Font.PLAIN, 12);
 			TreeNode tn = new TreeNode("Root", "", -1, true);
 			gv = new GraphView(new Graph(is, tn), this, font);
 			tb = new TreeBrowser(tn, gv, font);
 			gv.setTreeBrowser(tb);
 			Vector v = new Vector(10,10);
 			tn.collapsedDirectories(v);
 			gv.collapseDir(v);
 
 			ScrollPane scrollp1 = new ScrollPane();
 			ScrollPane scrollp2 = new ScrollPane();
 			scrollp1.add(gv);
 			scrollp2.add(tb);
 			scrollp1.getHAdjustable().setUnitIncrement(20);
 			scrollp1.getVAdjustable().setUnitIncrement(20);
 			scrollp2.getHAdjustable().setUnitIncrement(20);
 			scrollp2.getVAdjustable().setUnitIncrement(20);
 			Component gv2 = new Border(scrollp1, 3);
 			Component tb2 = new Border(scrollp2, 3);
 			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.err.println("\nI/O error while reading graph file.");
 		} catch (ParseError exn) {
 			System.err.println("\nParse error in graph file:");
 			System.err.println(exn.getMessage());
 			System.err.println("\nSyntax:\n<vertexname> <vertexID> <dirname> [ + ] <path> [ < | > ] [ <vertexID> [ ... [ <vertexID> ] ... ] ] ;");
 		}
 	}		
 
 	public void init() {
 		isApplet=true;
 		gfname=getParameter("graphfile");
 		try {
 			InputStream is=(new URL(getDocumentBase(), gfname)).openConnection().getInputStream();
 			initBrowser(is, false);
 			is.close();
 		} catch (MalformedURLException exn) {
 			System.err.println("Invalid URL: "+gfname);
 		} catch (IOException exn) {
 			System.err.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, args.length > 1);
 				is.close();
 			}
 			if (args.length > 1) {
                             try {
 			      if (args[1].endsWith(".ps"))
                                 gb.gv.PS(args[1], true);
                               else if (args[1].endsWith(".eps"))
                                 gb.gv.PS(args[1], false);
                               else
                                 System.err.println("Unknown file type: " + args[1]);
                             } catch (IOException exn) {
                               System.err.println("Unable to write file " + args[1]);
                             }
                         } else {
 			    f=new GraphBrowserFrame(gb);
 			    f.setSize(700,500);
 			    f.show();
                         }
 		} catch (IOException exn) {
 			System.err.println("Can't open graph file "+args[0]);
 		}
 	}
 }
 
diff --git a/src/Tools/GraphBrowser/GraphBrowser/GraphBrowserFrame.java b/src/Tools/GraphBrowser/graphbrowser/GraphBrowserFrame.java
rename from src/Tools/GraphBrowser/GraphBrowser/GraphBrowserFrame.java
rename to src/Tools/GraphBrowser/graphbrowser/GraphBrowserFrame.java
--- a/src/Tools/GraphBrowser/GraphBrowser/GraphBrowserFrame.java
+++ b/src/Tools/GraphBrowser/graphbrowser/GraphBrowserFrame.java
@@ -1,125 +1,125 @@
 /***************************************************************************
-  Title:      GraphBrowser/GraphBrowserFrame.java
+  Title:      graphbrowser/GraphBrowserFrame.java
   Author:     Stefan Berghofer, TU Muenchen
   Options:    :tabSize=2:
 
   This class is the frame for the stand-alone application. It contains
   methods for handling menubar events.
 ***************************************************************************/
 
-package GraphBrowser;
+package isabelle.graphbrowser;
 
 import java.awt.*;
 import java.awt.event.*;
 import java.io.*;
-import awtUtilities.*;
+import isabelle.awt.*;
 
 public class GraphBrowserFrame extends Frame implements ActionListener {
 	GraphBrowser gb;
 	MenuItem i1, i2;
 	String graphDir, psDir;
 
 	public void checkMenuItems() {
 		if (gb.isEmpty()) {
 			i1.setEnabled(false);
 			i2.setEnabled(false);
 		} else {
 			i1.setEnabled(true);
 			i2.setEnabled(true);
 		}
 	}
 
 	public void actionPerformed(ActionEvent evt) {
 		String label = evt.getActionCommand();
 		if (label.equals("Quit"))
 			System.exit(0);
 		else if (label.equals("Export to PostScript")) {
 			PS(true, label);
 			return;
 		} else if (label.equals("Export to EPS")) {
 			PS(false, label);
 			return;
 		} else if (label.equals("Open ...")) {
 			FileDialog fd = new FileDialog(this, "Open graph file", FileDialog.LOAD);
 			if (graphDir != null)
 				fd.setDirectory(graphDir);
 			fd.setVisible(true);
 			if (fd.getFile() == null) return;
 			graphDir = fd.getDirectory();
 			String fname = graphDir + fd.getFile();
 			GraphBrowser gb2 = new GraphBrowser(fname);
 			try {
 				InputStream is = new FileInputStream(fname);
 				gb2.initBrowser(is, false);
 				is.close();
 			} catch (IOException exn) {
 				String button[] = {"OK"};
 				MessageDialog md = new MessageDialog(this, "Error",
 					"Can't open file " + fname + ".", button);
 				md.setSize(350, 200);
 				md.setVisible(true);
 				return;
 			}
 			remove(gb);
 			add("Center", gb2);
 			gb = gb2;
 			checkMenuItems();
 			validate();
 		}
 	}
 
 	public void PS(boolean printable,String label) {
 		FileDialog fd=new FileDialog(this,label,FileDialog.SAVE);
 		if (psDir!=null)
 			fd.setDirectory(psDir);
 		fd.setVisible(true);
 		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.setSize(350,200);
 			md.setVisible(true);
 			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.setSize(350,200);
 			md.setVisible(true);
 		}
 	}
 
 	public GraphBrowserFrame(GraphBrowser br) {
 		super("GraphBrowser");
 		MenuItem i3, i4;
 		gb = br;
 		MenuBar mb = new MenuBar();
 		Menu m1 = new Menu("File");
 		m1.add(i3 = new MenuItem("Open ..."));
 		m1.add(i1 = new MenuItem("Export to PostScript"));
 		m1.add(i2 = new MenuItem("Export to EPS"));
 		m1.add(i4 = new MenuItem("Quit"));
 		i1.addActionListener(this);
 		i2.addActionListener(this);
 		i3.addActionListener(this);
 		i4.addActionListener(this);
 		checkMenuItems();
 		mb.add(m1);
 		setMenuBar(mb);
 		add("Center", br);
     addWindowListener( new WindowAdapter() {
       public void windowClosing(WindowEvent e) {
         System.exit(0);
       }
     });
 	}
 }
diff --git a/src/Tools/GraphBrowser/GraphBrowser/GraphView.java b/src/Tools/GraphBrowser/graphbrowser/GraphView.java
rename from src/Tools/GraphBrowser/GraphBrowser/GraphView.java
rename to src/Tools/GraphBrowser/graphbrowser/GraphView.java
--- a/src/Tools/GraphBrowser/GraphBrowser/GraphView.java
+++ b/src/Tools/GraphBrowser/graphbrowser/GraphView.java
@@ -1,276 +1,276 @@
 /***************************************************************************
-  Title:      GraphBrowser/GraphView.java
+  Title:      graphbrowser/GraphView.java
   Author:     Stefan Berghofer, TU Muenchen
   Options:    :tabSize=4:
 
   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;
+package isabelle.graphbrowser;
 
 import java.awt.*;
 import java.awt.event.*;
 import java.io.*;
 import java.util.*;
 
 public class GraphView extends Canvas implements MouseListener, MouseMotionListener {
 	Graph gra, gra2;
 	GraphBrowser browser;
 	Vertex v = null;
 	Vector collapsed = new Vector(10,10);
 	Vector collapsedDirs = new Vector(10,10);
 	TreeBrowser tb;
 	long timestamp;
 	Vertex highlighted = null;
 	Dimension size;
 	boolean parent_needs_layout;
 	Font font;
 
 	public void setTreeBrowser(TreeBrowser br) {
 		tb=br;
 	}
 
 	public GraphBrowser getBrowser() { return browser; }
 
 	public Graph getGraph() { return gra; }
 
 	public Graph getOriginalGraph() { return gra2; }
 
 	public GraphView(Graph gr, GraphBrowser br, Font f) {
 		gra2=gr;
 		browser=br;
 		gra=(Graph)(gra2.clone());
 		parent_needs_layout = true;
 		size = new Dimension(0, 0);
 		font = f;
 		addMouseListener(this);
 		addMouseMotionListener(this);
 	}
 
 	public void PS(String fname,boolean printable) throws IOException {
 	    Graph gra3 = (Graph)gra.clone();
 	    gra3.layout(null);
 	    gra3.PS(fname,printable);
 	}
 
 	public void paint(Graphics g) {
 		g.setFont(font);
 		gra.draw(g);
 		if (highlighted!=null) highlighted.drawBox(g,Color.white);
 		size = new Dimension(gra.max_x-gra.min_x, gra.max_y-gra.min_y);
 		if (parent_needs_layout) {
 			parent_needs_layout = false;
 			getParent().doLayout();
 		}
 	}
 
 	public Dimension getPreferredSize() {
 		return size;
 	}
 
 	public void mouseMoved(MouseEvent evt) {
 		int x = evt.getX() + gra.min_x;
 		int y = evt.getY() + gra.min_y;
 
 		Vertex v2=gra.vertexAt(x,y);
 		Graphics g=getGraphics();
 		g.setFont(font);
 		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;
 		}
 	}
 
 	public void mouseDragged(MouseEvent evt) {}
 
 	/*****************************************************************/
 	/* 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() {
 		Graphics g = getGraphics();
 		g.setFont(font);
 		browser.showWaitMessage();
 		highlighted=null;
 		gra.layout(g);
 		v=null;
 		parent_needs_layout = true;
 		update(g);
 		browser.showReadyMessage();
 	}
 
 	public void focusToVertex(int n) {
 		Vertex vx=gra.getVertexByNum(n);
 		if (vx!=null) {
 			ScrollPane scrollp = (ScrollPane)(getParent());
 			Dimension vpsize = scrollp.getViewportSize();
 
                         int x = vx.getX()-gra.min_x;
                         int y = vx.getY()-gra.min_y;
 			int offset_x = Math.min(scrollp.getHAdjustable().getMaximum(),
 				Math.max(0,x-vpsize.width/2));
 			int offset_y = Math.min(scrollp.getVAdjustable().getMaximum(),
 				Math.max(0,y-vpsize.height/2));
 
 			Graphics g=getGraphics();
 			g.setFont(font);
 			g.translate(-gra.min_x,-gra.min_y);
 			if (highlighted!=null) highlighted.drawBox(g,Color.lightGray);
 			vx.drawBox(g,Color.white);
 			highlighted=vx;
 			scrollp.setScrollPosition(offset_x, offset_y);
 		}
 	}
 
 	/*****************************************************************/
 	/*             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 void mouseClicked(MouseEvent evt) {
 		Vector code = null;
 		Vertex v2;
 		int x = evt.getX() + gra.min_x;
 		int y = evt.getY() + 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.getWhen()-timestamp < 400 && !(v.getPath().equals("")))
 					browser.viewFile(v.getPath());
 				timestamp=evt.getWhen();
 			}
 		}
 	}
 
 	public void mouseExited(MouseEvent evt) {
 		Graphics g=getGraphics();
 		g.setFont(font);
 		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;
 	}
 
 	public void mouseEntered(MouseEvent evt) {}
 
 	public void mousePressed(MouseEvent evt) {}
 
 	public void mouseReleased(MouseEvent evt) {}
 }
diff --git a/src/Tools/GraphBrowser/GraphBrowser/NormalVertex.java b/src/Tools/GraphBrowser/graphbrowser/NormalVertex.java
rename from src/Tools/GraphBrowser/GraphBrowser/NormalVertex.java
rename to src/Tools/GraphBrowser/graphbrowser/NormalVertex.java
--- a/src/Tools/GraphBrowser/GraphBrowser/NormalVertex.java
+++ b/src/Tools/GraphBrowser/graphbrowser/NormalVertex.java
@@ -1,154 +1,154 @@
 /***************************************************************************
-  Title:      GraphBrowser/NormalVertex.java
+  Title:      graphbrowser/NormalVertex.java
   Author:     Stefan Berghofer, TU Muenchen
   Options:    :tabSize=4:
 
   This class represents an ordinary vertex. It contains methods for
   drawing and PostScript output.
 ***************************************************************************/
 
-package GraphBrowser;
+package isabelle.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()-box_width2(); }
 
 	public int rightX() { return getX()+box_width2(); }
 
 	public void drawBox(Graphics g,Color boxColor) {
 		FontMetrics fm = g.getFontMetrics(g.getFont());
 		int h=fm.getAscent()+fm.getDescent();
 
 		g.setColor(boxColor);
 		g.fillRect(getX()-box_width2(),getY(),box_width(),gra.box_height);
 		g.setColor(Color.black);
 		g.drawRect(getX()-box_width2(),getY(),box_width(),gra.box_height);
 		if (getNumber()<0)
 			g.setColor(Color.red);
 
 		g.drawString(label,
 		             (int)Math.round((box_width()-fm.stringWidth(label))/2.0)+getX()-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(PrintWriter p) {
 		p.print(leftX()+" "+getY()+" "+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");
 		}
 	}	
 }
 		
diff --git a/src/Tools/GraphBrowser/GraphBrowser/ParseError.java b/src/Tools/GraphBrowser/graphbrowser/ParseError.java
rename from src/Tools/GraphBrowser/GraphBrowser/ParseError.java
rename to src/Tools/GraphBrowser/graphbrowser/ParseError.java
--- a/src/Tools/GraphBrowser/GraphBrowser/ParseError.java
+++ b/src/Tools/GraphBrowser/graphbrowser/ParseError.java
@@ -1,5 +1,5 @@
-package GraphBrowser;
+package isabelle.graphbrowser;
 
 class ParseError extends Exception {
 	public ParseError(String s) { super(s); }
 }
diff --git a/src/Tools/GraphBrowser/GraphBrowser/Region.java b/src/Tools/GraphBrowser/graphbrowser/Region.java
rename from src/Tools/GraphBrowser/GraphBrowser/Region.java
rename to src/Tools/GraphBrowser/graphbrowser/Region.java
--- a/src/Tools/GraphBrowser/GraphBrowser/Region.java
+++ b/src/Tools/GraphBrowser/graphbrowser/Region.java
@@ -1,89 +1,89 @@
 /***************************************************************************
-  Title:      GraphBrowser/Region.java
+  Title:      graphbrowser/Region.java
   Author:     Stefan Berghofer, TU Muenchen
   Options:    :tabSize=4:
 
   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;
+package isabelle.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()-
 			20;
 	}
 
 	public boolean touching(Region r2) {
 		return spaceBetween(r2)==0;
 	}
 }
diff --git a/src/Tools/GraphBrowser/GraphBrowser/Spline.java b/src/Tools/GraphBrowser/graphbrowser/Spline.java
rename from src/Tools/GraphBrowser/GraphBrowser/Spline.java
rename to src/Tools/GraphBrowser/graphbrowser/Spline.java
--- a/src/Tools/GraphBrowser/GraphBrowser/Spline.java
+++ b/src/Tools/GraphBrowser/graphbrowser/Spline.java
@@ -1,120 +1,120 @@
 /***************************************************************************
-  Title:      GraphBrowser/Spline.java
+  Title:      graphbrowser/Spline.java
   Author:     Stefan Berghofer, TU Muenchen
   Options:    :tabSize=4:
 
   This class is used for drawing spline curves (which are not yet
   supported by the Java AWT).
 ***************************************************************************/
 
-package GraphBrowser;
+package isabelle.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(PrintWriter 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");
 	}
 }
diff --git a/src/Tools/GraphBrowser/GraphBrowser/TreeBrowser.java b/src/Tools/GraphBrowser/graphbrowser/TreeBrowser.java
rename from src/Tools/GraphBrowser/GraphBrowser/TreeBrowser.java
rename to src/Tools/GraphBrowser/graphbrowser/TreeBrowser.java
--- a/src/Tools/GraphBrowser/GraphBrowser/TreeBrowser.java
+++ b/src/Tools/GraphBrowser/graphbrowser/TreeBrowser.java
@@ -1,94 +1,94 @@
 /***************************************************************************
-  Title:      GraphBrowser/TreeBrowser.java
+  Title:      graphbrowser/TreeBrowser.java
   Author:     Stefan Berghofer, TU Muenchen
   Options:    :tabSize=4:
 
   This class defines the browser window which is used to display directory
   trees. It contains methods for handling events.
 ***************************************************************************/
 
-package GraphBrowser;
+package isabelle.graphbrowser;
 
 import java.awt.*;
 import java.awt.event.*;
 import java.util.*;
 
 
 public class TreeBrowser extends Canvas implements MouseListener
 {
 	TreeNode t;
 	TreeNode selected;
 	GraphView gv;
 	long timestamp;
 	Dimension size;
 	boolean parent_needs_layout;
 	Font font;
 
 	public TreeBrowser(TreeNode tn, GraphView gr, Font f) {
 		t = tn; gv = gr; font = f;
 		size = new Dimension(0, 0);
 		parent_needs_layout = true;
 		addMouseListener(this);
 	}
 
 	public Dimension getPreferredSize() {
 		return size;
 	}
 
 	public void mouseEntered(MouseEvent evt) {}
 
 	public void mouseExited(MouseEvent evt) {}
 
 	public void mouseReleased(MouseEvent evt) {}
 
 	public void mousePressed(MouseEvent evt) {}
 
 	public void mouseClicked(MouseEvent e)
 	{
 		TreeNode l=t.lookup(e.getY());
 
 		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.getWhen()-timestamp < 400 && !(vx.getPath().equals("")))
 					gv.getBrowser().viewFile(vx.getPath());
 				timestamp=e.getWhen();
 
 			}
 			selected=l;
 			parent_needs_layout = true;
 			repaint();
 		}
 	}
 
 	public void selectNode(TreeNode nd) {
 		Vector v=new Vector(10,10);
 		nd.select();
 		t.collapsedDirectories(v);
 		gv.collapseDir(v);
 		gv.relayout();
 		selected=nd;
 		parent_needs_layout = true;
 		repaint();
 	}
 
 	public void paint(Graphics g)
 	{
 		g.setFont(font);
 		Dimension d = t.draw(g,5,5,selected);
 		if (parent_needs_layout) {
 			size = new Dimension(5+d.width, 5+d.height);
 			parent_needs_layout = false;
 			getParent().doLayout();
 		}
 	}
 }
 
diff --git a/src/Tools/GraphBrowser/GraphBrowser/TreeNode.java b/src/Tools/GraphBrowser/graphbrowser/TreeNode.java
rename from src/Tools/GraphBrowser/GraphBrowser/TreeNode.java
rename to src/Tools/GraphBrowser/graphbrowser/TreeNode.java
--- a/src/Tools/GraphBrowser/GraphBrowser/TreeNode.java
+++ b/src/Tools/GraphBrowser/graphbrowser/TreeNode.java
@@ -1,168 +1,168 @@
 /***************************************************************************
-  Title:      GraphBrowser/TreeNode.java
+  Title:      graphbrowser/TreeNode.java
   Author:     Stefan Berghofer, TU Muenchen
   Options:    :tabSize=4:
 
   This class contains methods for storing and manipulating directory
   trees (e.g. collapsing / uncollapsing directory branches).
 ***************************************************************************/
 
-package GraphBrowser;
+package isabelle.graphbrowser;
 
 import java.awt.*;
 import java.util.*;
 
 
 public class TreeNode
 {
 	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;
 		/*Integer.valueOf
 		for(int i=0;i<leaves.size();i++)
 			((Tree)leaves.elementAt(i)).collapse();
 		*/
 	}
 
 	void collapsedNodes(Vector v) {
 		if (number>=0) v.addElement(Integer.valueOf(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(g.getFont());
 		int h=fm.getHeight();
 		int e=(int) (h / 10) + 1;
 		int down_x[]={x + e, x + h - e, x + (int)(h / 2)};
 		int down_y[]={y + e, y + e, y + (int)(3 * h / 4) - e};
 		int right_x[]={x + e, x + (int)(3 * h / 4) - e, x + e};
 		int right_y[]={y + e, y + (int)(h / 2), y + h - e};
 		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+4,y+fm.getAscent());
 			starty=y;endy=y+h;
 			dx=Math.max(dx,x+h+4+fm.stringWidth(name));
 			y+=h+5;
 			for(int i=0;i<leaves.size();i++)
 			{
 				Dimension d=((TreeNode)leaves.elementAt(i)).draw(g,x+h+4,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+4,y,fm.stringWidth(name),h);
 			}
 			g.setColor(Color.black);
 			g.drawString(name,x+h+4,y+fm.getAscent());
 			starty=y;endy=y+h;
 			dx=Math.max(dx,x+h+4+fm.stringWidth(name));
 			y+=h+5;
 		}
 		return new Dimension(dx,y);
 	}
 }
 
 
diff --git a/src/Tools/GraphBrowser/GraphBrowser/Vertex.java b/src/Tools/GraphBrowser/graphbrowser/Vertex.java
rename from src/Tools/GraphBrowser/GraphBrowser/Vertex.java
rename to src/Tools/GraphBrowser/graphbrowser/Vertex.java
--- a/src/Tools/GraphBrowser/GraphBrowser/Vertex.java
+++ b/src/Tools/GraphBrowser/graphbrowser/Vertex.java
@@ -1,213 +1,213 @@
 /***************************************************************************
-  Title:      GraphBrowser/Vertex.java
+  Title:      graphbrowser/Vertex.java
   Author:     Stefan Berghofer, TU Muenchen
   Options:    :tabSize=4:
 
   This class contains attributes and methods common to all kinds of
   vertices (e.g. coordinates, successors, predecessors).
 ***************************************************************************/
 
-package GraphBrowser;
+package isabelle.graphbrowser;
 
 import java.util.*;
 import java.awt.*;
 import java.io.*;
 
 abstract class Vertex {
 	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 Box getLabelSize(Graphics g) {
 		AbstractFontMetrics fm = g == null ? 
       (AbstractFontMetrics) new DefaultFontMetrics(12) : 
       (AbstractFontMetrics) new AWTFontMetrics(g.getFontMetrics(g.getFont()));
 		
 		return new Box(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 preds=new Vector(10,10);
 	    Vector todo=(Vector)(parents.clone());
 	    Vertex vx1,vx2;
 	    Enumeration e;
 
 	    while (!todo.isEmpty()) {
 		vx1=(Vertex)(todo.lastElement());
 		todo.removeElementAt(todo.size()-1);
 		preds.addElement(vx1);
 		e=vx1.parents.elements();
 		while (e.hasMoreElements()) {
 		    vx2=(Vertex)(e.nextElement());
 		    if (preds.indexOf(vx2)<0 && todo.indexOf(vx2)<0)
 			todo.addElement(vx2);
 		}
 	    }
 
 	    return preds;
 	}
 
 	/********************************************************************/
 	/*                     get all successor vertices                   */
 	/********************************************************************/
 
 	public Vector getSuccs() {
 	    Vector succs=new Vector(10,10);
 	    Vector todo=(Vector)(children.clone());
 	    Vertex vx1,vx2;
 	    Enumeration e;
 
 	    while (!todo.isEmpty()) {
 		vx1=(Vertex)(todo.lastElement());
 		todo.removeElementAt(todo.size()-1);
 		succs.addElement(vx1);
 		e=vx1.children.elements();
 		while (e.hasMoreElements()) {
 		    vx2=(Vertex)(e.nextElement());
 		    if (succs.indexOf(vx2)<0 && todo.indexOf(vx2)<0)
 			todo.addElement(vx2);
 		}
 	    }
 
 	    return succs;
 	}
 
 	public int box_width() { return getLabelSize(gra.gfx).width+8; }
 
 	public int box_width2() { return box_width()/2; }
 
 	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(PrintWriter p) {}
 }
diff --git a/src/Tools/GraphBrowser/lib/Tools/browser b/src/Tools/GraphBrowser/lib/Tools/browser
--- a/src/Tools/GraphBrowser/lib/Tools/browser
+++ b/src/Tools/GraphBrowser/lib/Tools/browser
@@ -1,108 +1,108 @@
 #!/usr/bin/env bash
 #
 # Author: Markus Wenzel, TU Muenchen
 #
 # DESCRIPTION: Isabelle graph browser
 
 
 PRG="$(basename "$0")"
 
 function usage()
 {
   echo
   echo "Usage: isabelle $PRG [OPTIONS] [GRAPHFILE]"
   echo
   echo "  Options are:"
   echo "    -b           Admin/build only"
   echo "    -c           cleanup -- remove GRAPHFILE after use"
   echo "    -o FILE      output to FILE (ps, eps, pdf)"
   echo
   exit 1
 }
 
 function fail()
 {
   echo "$1" >&2
   exit 2
 }
 
 
 ## process command line
 
 # options
 
 ADMIN_BUILD=""
 CLEAN=""
 OUTFILE=""
 
 while getopts "bco:" OPT
 do
   case "$OPT" in
     b)
       ADMIN_BUILD=true
       ;;
     c)
       CLEAN=true
       ;;
     o)
       OUTFILE="$OPTARG"
       ;;
     \?)
       usage
       ;;
   esac
 done
 
 shift $(($OPTIND - 1))
 
 
 # args
 
 GRAPHFILE=""
 [ "$#" -gt 0 ] && { GRAPHFILE="$1"; shift; }
 [ "$#" -ne 0 ] && usage
 
 
 ## main
 
 isabelle_admin_build jars || exit $?
 
 if [ -n "$GRAPHFILE" ]; then
   PRIVATE_FILE="${ISABELLE_TMP:-${TMPDIR:-/tmp}}/$$"$(basename "$GRAPHFILE")
   if [ -n "$CLEAN" ]; then
     mv -f "$GRAPHFILE" "$PRIVATE_FILE" || fail "Cannot move file: $GRAPHFILE"
   else
     cp -f "$GRAPHFILE" "$PRIVATE_FILE" || fail "Cannot copy file: $GRAPHFILE"
   fi
 
   PDF=""
   case "$OUTFILE" in
     *.pdf)
       OUTFILE="${OUTFILE%%.pdf}.eps"
       PDF=true
       ;;
   esac
 
   if [ -z "$OUTFILE" ]; then
-    isabelle java GraphBrowser.GraphBrowser "$(platform_path "$PRIVATE_FILE")"
+    isabelle java isabelle.graphbrowser.GraphBrowser "$(platform_path "$PRIVATE_FILE")"
   else
-    isabelle java GraphBrowser.Console "$(platform_path "$PRIVATE_FILE")" "$(platform_path "$OUTFILE")"
+    isabelle java isabelle.graphbrowser.Console "$(platform_path "$PRIVATE_FILE")" "$(platform_path "$OUTFILE")"
   fi
   RC="$?"
 
   if [ -n "$PDF" ]; then
     (
       cd "$(dirname "$OUTFILE")"
       "$ISABELLE_EPSTOPDF" "$(basename "$OUTFILE")" || fail "Failed to produce pdf output"
     )
   fi
 
   rm -f "$PRIVATE_FILE"
 elif [ -z "$ADMIN_BUILD" ]; then
   [ -d "$ISABELLE_BROWSER_INFO" ] && cd "$ISABELLE_BROWSER_INFO"
-  exec isabelle java GraphBrowser.GraphBrowser
+  exec isabelle java isabelle.graphbrowser.GraphBrowser
 else
   RC=0
 fi
 
 exit "$RC"