updated to jedit_build-20181025 according to patches/macos (Java 11), patches/putenv;
proper update of jEdit environment -- avoid warnings in Java 11;
activate jdk-11+28;
package 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; }
}