/*************************************************************************** Title: graphbrowser/TreeNode.java Author: Stefan Berghofer, TU Muenchen Options: :tabSize=4:
This class contains methods for storing and manipulating directory trees (e.g. collapsing / uncollapsing directory branches).
***************************************************************************/
package isabelle.graphbrowser;
import java.awt.*; import java.util.*;
publicclass TreeNode
{ int starty,endy,number;
String name,path;
void collapsedNodes(Vector v) { if (number>=0) v.addElement(Integer.valueOf(number));
Enumeration e1=leaves.elements(); while (e1.hasMoreElements())
((TreeNode)(e1.nextElement())).collapsedNodes(v);
}
publicvoid collapsedDirectories(Vector v) { if (!unfold) {
Vector v2=new Vector(10,10);
v.addElement(new Directory(this,name,v2));
collapsedNodes(v2);
} else {
Enumeration e1=leaves.elements(); while (e1.hasMoreElements()) {
TreeNode tn=(TreeNode)(e1.nextElement()); if (!tn.leaves.isEmpty())
tn.collapsedDirectories(v);
}
}
}
public Dimension draw(Graphics g,int x,int y,TreeNode t)
{
FontMetrics fm=g.getFontMetrics(g.getFont()); int h=fm.getHeight(); int e=(int) (h / 10) + 1; int down_x[]={x + e, x + h - e, x + (int)(h / 2)}; int down_y[]={y + e, y + e, y + (int)(3 * h / 4) - e}; int right_x[]={x + e, x + (int)(3 * h / 4) - e, x + e}; int right_y[]={y + e, y + (int)(h / 2), y + h - e}; int dx=0;
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.