public class ExplorationModeModel
extends java.lang.Object
This class holds the data and the state of proof exploration.
For every KeYMediator
or MainWindow
should only exists one instance.
ExplorationExtension
Modifier and Type | Class and Description |
---|---|
static class |
ExplorationModeModel.ExplorationState
State whether whole application (with shown second branch) or
simplified with hidden branch app should be used
|
Modifier and Type | Field and Description |
---|---|
static java.lang.String |
PROP_EXPLORE_MODE |
static java.lang.String |
PROP_EXPLORE_TACLET_APP_STATE |
Constructor and Description |
---|
ExplorationModeModel() |
Modifier and Type | Method and Description |
---|---|
void |
addPropertyChangeListener(java.beans.PropertyChangeListener listener) |
void |
addPropertyChangeListener(java.lang.String propertyName,
java.beans.PropertyChangeListener listener) |
java.util.concurrent.atomic.AtomicInteger |
get(Proof p)
Return the number of tainted exploration nodes in a Proof
|
ExplorationModeModel.ExplorationState |
getExplorationTacletAppState()
Get the state which kind of taclet to use
|
boolean |
isExplorationModeSelected()
Check whether actions mode is selected
|
boolean |
isShowInteractiveBranches()
Returns whether the justification branch should be visible.
|
void |
removePropertyChangeListener(java.beans.PropertyChangeListener listener) |
void |
removePropertyChangeListener(java.lang.String propertyName,
java.beans.PropertyChangeListener listener) |
void |
setExplorationModeSelected(boolean explorationModeSelected)
Set selection of Exploration mode.
|
void |
setExplorationTacletAppState(ExplorationModeModel.ExplorationState explorationTacletAppState)
Set the state
|
void |
setShowInteractiveBranches(boolean showInteractiveBranches)
Triggers a property change event, and the rerendering of the proof tree.
|
public static final java.lang.String PROP_EXPLORE_MODE
public static final java.lang.String PROP_EXPLORE_TACLET_APP_STATE
@Nonnull public ExplorationModeModel.ExplorationState getExplorationTacletAppState()
public void setExplorationTacletAppState(ExplorationModeModel.ExplorationState explorationTacletAppState)
public boolean isExplorationModeSelected()
public void setExplorationModeSelected(boolean explorationModeSelected)
PROP_EXPLORE_MODE
public boolean isShowInteractiveBranches()
public java.util.concurrent.atomic.AtomicInteger get(Proof p)
public void setShowInteractiveBranches(boolean showInteractiveBranches)
isShowInteractiveBranches()
public void addPropertyChangeListener(java.beans.PropertyChangeListener listener)
public void removePropertyChangeListener(java.beans.PropertyChangeListener listener)
public void addPropertyChangeListener(java.lang.String propertyName, java.beans.PropertyChangeListener listener)
public void removePropertyChangeListener(java.lang.String propertyName, java.beans.PropertyChangeListener listener)
Copyright © 2003-2019 The KeY-Project.