/*************************************************************************** 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 isabelle.graphbrowser;
import java.util.*;
class Region {
Vector vertices=new Vector(10,10);
Graph gra;
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.