diff -r 3b8b1da2ff29 -r 12b1f4649ab1 src/Tools/GraphBrowser/GraphBrowser/Vertex.java
--- a/src/Tools/GraphBrowser/GraphBrowser/Vertex.java	Fri Jul 16 12:45:37 2021 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,213 +0,0 @@
-/***************************************************************************
-  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;
-
-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) {}
-}