private static class ProofTreeViewFilter.HideClosedSubtreesFilter extends ProofTreeViewFilter
ProofTreeViewFilter.NodeFilter
ALL, HIDE_CLOSED_SUBTREES, HIDE_INTERMEDIATE, ONLY_INTERACTIVE
Modifier | Constructor and Description |
---|---|
private |
HideClosedSubtreesFilter() |
Modifier and Type | Method and Description |
---|---|
(package private) boolean |
global()
Returns whether the filter's scope is on the whole tree (like hiding subtrees).
|
boolean |
isActive()
Whether the filter is currently active.
|
java.lang.String |
name()
Name of the filter used in GUI elements.
|
(package private) void |
setActive(boolean active)
Should only be called through GUIProofTreeNode#setFilter().
|
public boolean isActive()
ProofTreeViewFilter
isActive
in class ProofTreeViewFilter
void setActive(boolean active)
ProofTreeViewFilter
setActive
in class ProofTreeViewFilter
public java.lang.String name()
ProofTreeViewFilter
name
in class ProofTreeViewFilter
boolean global()
ProofTreeViewFilter
global
in class ProofTreeViewFilter