lib/browser/GraphBrowser/Directory.java
author blanchet
Tue, 22 Mar 2011 19:04:32 +0100
changeset 42064 f4e53c8630c0
parent 13973 9170772bf420
permissions -rw-r--r--
added first-order TPTP version of Nitpick to Isabelle, so that its sources stay in sync with Isabelle and it is easier to install new versions for SystemOnTPTP and CASC -- the tool is called "isabelle nitrox" but is deliberately omitted from the tool list unless the component is explicitly enabled, to avoid clutter
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
13973
9170772bf420 fixed javac warning
kleing
parents:
diff changeset
     1
package GraphBrowser;
9170772bf420 fixed javac warning
kleing
parents:
diff changeset
     2
9170772bf420 fixed javac warning
kleing
parents:
diff changeset
     3
import java.util.Vector;
9170772bf420 fixed javac warning
kleing
parents:
diff changeset
     4
9170772bf420 fixed javac warning
kleing
parents:
diff changeset
     5
class Directory {
9170772bf420 fixed javac warning
kleing
parents:
diff changeset
     6
	TreeNode node;
9170772bf420 fixed javac warning
kleing
parents:
diff changeset
     7
	String name;
9170772bf420 fixed javac warning
kleing
parents:
diff changeset
     8
	Vector collapsed;
9170772bf420 fixed javac warning
kleing
parents:
diff changeset
     9
9170772bf420 fixed javac warning
kleing
parents:
diff changeset
    10
	public Directory(TreeNode nd,String n,Vector col) {
9170772bf420 fixed javac warning
kleing
parents:
diff changeset
    11
		collapsed=col;
9170772bf420 fixed javac warning
kleing
parents:
diff changeset
    12
		name=n;
9170772bf420 fixed javac warning
kleing
parents:
diff changeset
    13
		node=nd;
9170772bf420 fixed javac warning
kleing
parents:
diff changeset
    14
	}
9170772bf420 fixed javac warning
kleing
parents:
diff changeset
    15
9170772bf420 fixed javac warning
kleing
parents:
diff changeset
    16
	public TreeNode getNode() { return node; }
9170772bf420 fixed javac warning
kleing
parents:
diff changeset
    17
9170772bf420 fixed javac warning
kleing
parents:
diff changeset
    18
	public String getName() { return name; }
9170772bf420 fixed javac warning
kleing
parents:
diff changeset
    19
9170772bf420 fixed javac warning
kleing
parents:
diff changeset
    20
	public Vector getCollapsed() { return collapsed; }
9170772bf420 fixed javac warning
kleing
parents:
diff changeset
    21
}