author | wenzelm |
Fri, 16 Jul 2021 12:55:02 +0200 | |
changeset 74015 | 12b1f4649ab1 |
parent 74011 | src/Tools/GraphBrowser/GraphBrowser/Directory.java@1d366486a812 |
permissions | -rw-r--r-- |
74015 | 1 |
package isabelle.graphbrowser; |
13973 | 2 |
|
3 |
import java.util.Vector; |
|
4 |
||
5 |
class Directory { |
|
6 |
TreeNode node; |
|
7 |
String name; |
|
8 |
Vector collapsed; |
|
9 |
||
10 |
public Directory(TreeNode nd,String n,Vector col) { |
|
11 |
collapsed=col; |
|
12 |
name=n; |
|
13 |
node=nd; |
|
14 |
} |
|
15 |
||
16 |
public TreeNode getNode() { return node; } |
|
17 |
||
18 |
public String getName() { return name; } |
|
19 |
||
20 |
public Vector getCollapsed() { return collapsed; } |
|
21 |
} |