src/Tools/GraphBrowser/graphbrowser/DummyVertex.java

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/GraphBrowser/graphbrowser/DummyVertex.java	Fri Jul 16 12:55:02 2021 +0200
@@ -0,0 +1,29 @@
+/***************************************************************************
+  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 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) {}
+}
+