lib/browser/GraphBrowser/TreeNode.java
author blanchet
Wed, 04 Aug 2010 23:27:27 +0200
changeset 38195 a8cef06e0480
parent 33686 8e33ca8832b1
child 50473 ca4088bf8365
permissions -rw-r--r--
Cycle breaking in the bounds takes care of singly recursive datatypes, so we don't need to do it again; the effect of removing the constraint varies on problem to problem, but it tends to be overwhelmingly negative in conjuction with the new datatype sym breaking stuff at high cardinalities
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
3599
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
     1
/***************************************************************************
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
     2
  Title:      GraphBrowser/TreeNode.java
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
     3
  Author:     Stefan Berghofer, TU Muenchen
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
     4
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
     5
  This class contains methods for storing and manipulating directory
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
     6
  trees (e.g. collapsing / uncollapsing directory branches).
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
     7
***************************************************************************/
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
     8
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
     9
package GraphBrowser;
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    10
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    11
import java.awt.*;
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    12
import java.util.*;
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    13
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    14
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    15
public class TreeNode
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    16
{
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    17
	int starty,endy,number;
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    18
	String name,path;
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    19
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    20
	Vector leaves=new Vector(10,10);
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    21
	boolean unfold=false;
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    22
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    23
	public void insertNode(String n,String d,String p,int num,boolean u) {
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    24
		if (d.length()==0) {
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    25
			leaves.addElement(new TreeNode(n,p,num));
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    26
			unfold=unfold||u;
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    27
		} else {
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    28
			unfold=unfold||u;
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    29
			String str1,str2;
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    30
			if (d.indexOf('/')<0) {
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    31
				str1=d;str2="";
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    32
			} else {
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    33
				str1=d.substring(0,d.indexOf('/'));
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    34
				str2=d.substring(d.indexOf('/')+1);
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    35
			}
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    36
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    37
			Enumeration e1=leaves.elements();
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    38
			TreeNode nd=null;
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    39
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    40
			while (e1.hasMoreElements()) {
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    41
				TreeNode nd2=(TreeNode)(e1.nextElement());
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    42
				if (nd2.name.equals(str1)) {
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    43
					nd=nd2;break;
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    44
				}
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    45
			}
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    46
			if (nd==null) {
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    47
				nd=new TreeNode(str1,"",-1);
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    48
				leaves.addElement(nd);
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    49
			}
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    50
			nd.insertNode(n,str2,p,num,u);
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    51
		}
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    52
	}
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    53
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    54
	public TreeNode(String n,String p,int num) {
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    55
		name=n;
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    56
		path=p;
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    57
		number=num;
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    58
	}
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    59
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    60
	public TreeNode(String n,String p,int num,boolean u) {
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    61
		this(n,p,num);
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    62
		unfold=u;
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    63
	}	
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    64
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    65
	public int getNumber() { return number; }
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    66
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    67
	public TreeNode lookup(int y)
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    68
	{
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    69
		if (y>=starty && y<endy) return this;
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    70
		else
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    71
		if (unfold)
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    72
			for (int i=0;i<leaves.size();i++)
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    73
			{
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    74
				TreeNode t=((TreeNode)leaves.elementAt(i)).lookup(y);
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    75
				if (t!=null) return t;
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    76
			}
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    77
		return null;
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    78
	}
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    79
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    80
	public boolean select()
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    81
	{
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    82
		if (!leaves.isEmpty()) {
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    83
			if (unfold) collapse();
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    84
			else unfold=true;
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    85
			return true;
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    86
		}
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    87
		return false; 
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    88
	}
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    89
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    90
	public void collapse()
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    91
	{
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    92
		unfold=false;
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    93
		/*
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    94
		for(int i=0;i<leaves.size();i++)
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    95
			((Tree)leaves.elementAt(i)).collapse();
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    96
		*/
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    97
	}
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    98
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    99
	void collapsedNodes(Vector v) {
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   100
		if (number>=0) v.addElement(new Integer(number));
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   101
		Enumeration e1=leaves.elements();
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   102
		while (e1.hasMoreElements())
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   103
			((TreeNode)(e1.nextElement())).collapsedNodes(v);
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   104
	}
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   105
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   106
	public void collapsedDirectories(Vector v) {
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   107
		if (!unfold) {
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   108
			Vector v2=new Vector(10,10);
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   109
			v.addElement(new Directory(this,name,v2));
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   110
			collapsedNodes(v2);
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   111
		} else {
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   112
			Enumeration e1=leaves.elements();
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   113
			while (e1.hasMoreElements()) {
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   114
				TreeNode tn=(TreeNode)(e1.nextElement());
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   115
				if (!tn.leaves.isEmpty())
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   116
					tn.collapsedDirectories(v);
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   117
			}
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   118
		}
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   119
	}
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   120
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   121
	public Dimension draw(Graphics g,int x,int y,TreeNode t)
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   122
	{
11873
38dc46b55d7e Moved font settings from TreeNode to TreeBrowser.
berghofe
parents: 9407
diff changeset
   123
		FontMetrics fm=g.getFontMetrics(g.getFont());
3599
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   124
		int h=fm.getHeight();
9407
e8f6d918fde9 renamed "Directories" to "Sessions";
wenzelm
parents: 6657
diff changeset
   125
		int e=(int) (h / 10) + 1;
e8f6d918fde9 renamed "Directories" to "Sessions";
wenzelm
parents: 6657
diff changeset
   126
		int down_x[]={x + e, x + h - e, x + (int)(h / 2)};
e8f6d918fde9 renamed "Directories" to "Sessions";
wenzelm
parents: 6657
diff changeset
   127
		int down_y[]={y + e, y + e, y + (int)(3 * h / 4) - e};
e8f6d918fde9 renamed "Directories" to "Sessions";
wenzelm
parents: 6657
diff changeset
   128
		int right_x[]={x + e, x + (int)(3 * h / 4) - e, x + e};
e8f6d918fde9 renamed "Directories" to "Sessions";
wenzelm
parents: 6657
diff changeset
   129
		int right_y[]={y + e, y + (int)(h / 2), y + h - e};
3599
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   130
		int dx=0;
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   131
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   132
		if (unfold)
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   133
		{
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   134
			g.setColor(Color.green);
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   135
			g.fillPolygon(down_x,down_y,3);
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   136
			g.setColor(Color.black);
6657
9627197bd9e1 tuned arrows;
wenzelm
parents: 6541
diff changeset
   137
			g.drawString(name,x+h+4,y+fm.getAscent());
3599
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   138
			starty=y;endy=y+h;
6657
9627197bd9e1 tuned arrows;
wenzelm
parents: 6541
diff changeset
   139
			dx=Math.max(dx,x+h+4+fm.stringWidth(name));
3599
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   140
			y+=h+5;
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   141
			for(int i=0;i<leaves.size();i++)
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   142
			{
6657
9627197bd9e1 tuned arrows;
wenzelm
parents: 6541
diff changeset
   143
				Dimension d=((TreeNode)leaves.elementAt(i)).draw(g,x+h+4,y,t);
3599
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   144
				y=d.height;
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   145
				dx=Math.max(dx,d.width);
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   146
			}
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   147
		}
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   148
		else
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   149
		{
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   150
			g.setColor(leaves.isEmpty() ? Color.blue : Color.red);
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   151
			g.fillPolygon(right_x,right_y,3);
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   152
			if (this==t && leaves.isEmpty())
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   153
			{
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   154
				g.setColor(Color.white);
6657
9627197bd9e1 tuned arrows;
wenzelm
parents: 6541
diff changeset
   155
				g.fillRect(x+h+4,y,fm.stringWidth(name),h);
3599
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   156
			}
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   157
			g.setColor(Color.black);
6657
9627197bd9e1 tuned arrows;
wenzelm
parents: 6541
diff changeset
   158
			g.drawString(name,x+h+4,y+fm.getAscent());
3599
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   159
			starty=y;endy=y+h;
6657
9627197bd9e1 tuned arrows;
wenzelm
parents: 6541
diff changeset
   160
			dx=Math.max(dx,x+h+4+fm.stringWidth(name));
3599
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   161
			y+=h+5;
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   162
		}
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   163
		return new Dimension(dx,y);
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   164
	}
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   165
}
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   166
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
   167