lib/browser/GraphBrowser/DummyVertex.java
author boehmes
Tue, 07 Dec 2010 14:53:12 +0100
changeset 41059 d2b1fc1b8e19
parent 33686 8e33ca8832b1
child 50473 ca4088bf8365
permissions -rw-r--r--
centralized handling of built-in types and constants; also store types and constants which are rewritten during preprocessing; interfaces are identified by classes (supporting inheritance, at least on the level of built-in symbols); removed term_eq in favor of type replacements: term-level occurrences of type bool are replaced by type term_bool (only for the translation)

/***************************************************************************
  Title:      GraphBrowser/DummyVertex.java
  Author:     Stefan Berghofer, TU Muenchen

  This class represents a dummy vertex, which is used to simplify the
  layout algorithm.
***************************************************************************/

package 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) {}
}