src/Tools/GraphBrowser/graphbrowser/DummyVertex.java
author wenzelm
Mon, 29 Aug 2022 19:26:27 +0200
changeset 76019 f3d8da992445
parent 74015 12b1f4649ab1
permissions -rw-r--r--
provide cvc5-1.0.2 (inactive);

/***************************************************************************
  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) {}
}