src/Tools/GraphBrowser/graphbrowser/Directory.java

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/GraphBrowser/graphbrowser/Directory.java	Fri Jul 16 12:55:02 2021 +0200
@@ -0,0 +1,21 @@
+package isabelle.graphbrowser;
+
+import java.util.Vector;
+
+class Directory {
+	TreeNode node;
+	String name;
+	Vector collapsed;
+
+	public Directory(TreeNode nd,String n,Vector col) {
+		collapsed=col;
+		name=n;
+		node=nd;
+	}
+
+	public TreeNode getNode() { return node; }
+
+	public String getName() { return name; }
+
+	public Vector getCollapsed() { return collapsed; }
+}