public class KeYSelectionModel
extends java.lang.Object
Modifier and Type | Class and Description |
---|---|
protected class |
KeYSelectionModel.DefaultSelectionIterator
enumerate the possible goal selections, starting with the best
one
|
Modifier and Type | Field and Description |
---|---|
private boolean |
goalIsValid
if true the selectedGoal field below can be trusted
|
private java.util.List<KeYSelectionListener> |
listenerList
the listeners to this model
|
private Proof |
proof
the proof to listen to
|
private Goal |
selectedGoal
is the selected node a goal
|
private Node |
selectedNode
the current displayed node
|
private KeYSelectionEvent |
selectionEvent
cached selected node event
|
Constructor and Description |
---|
KeYSelectionModel() |
Modifier and Type | Method and Description |
---|---|
void |
addKeYSelectionListener(KeYSelectionListener listener) |
void |
defaultSelection()
selects the first goal in the goal list of proof if available
if not it selects a leaf of the proof tree
|
void |
fireSelectedNodeChanged() |
void |
fireSelectedProofChanged() |
private Goal |
getFirstOpenGoalBelow(Node n)
retrieves the first open goal below the given node, i.e. the goal
containing the first leaf of the subtree starting at
n which is not already closed |
Goal |
getSelectedGoal()
returns the goal the selected node belongs to, null if it is
an inner node
|
Node |
getSelectedNode()
returns the node that is selected by the user
|
Proof |
getSelectedProof()
returns the proof that is selected by the user
|
boolean |
isGoal()
returns true iff the selected node is a goal
|
void |
nearestOpenGoalSelection(Node old)
selects the first open goal below the given node old
if no open goal is available node old is selected.
|
void |
removeKeYSelectionListener(KeYSelectionListener listener) |
void |
setProof(Proof p)
Does not take care of GUI effects
|
void |
setSelectedGoal(Goal g)
sets the node that is focused by the user
|
void |
setSelectedNode(Node n)
sets the node that is focused by the user
|
void |
setSelectedProof(Proof p)
sets the selected proof
|
private Proof proof
private boolean goalIsValid
private Goal selectedGoal
private Node selectedNode
private final java.util.List<KeYSelectionListener> listenerList
private KeYSelectionEvent selectionEvent
public void setProof(Proof p)
public void setSelectedProof(Proof p)
p
- the Proof that is selectedpublic Proof getSelectedProof()
public void setSelectedNode(Node n)
n
- the selected nodepublic void setSelectedGoal(Goal g)
g
- the Goal that contains the selected nodepublic Node getSelectedNode()
public Goal getSelectedGoal()
public boolean isGoal()
public void defaultSelection()
public void nearestOpenGoalSelection(Node old)
old
- the Node to start looking for open goalsprivate Goal getFirstOpenGoalBelow(Node n)
n
which is not already closedn
- the Node where to start fromn
, which is not already closed.
null
is returned if no such goal exists.public void addKeYSelectionListener(KeYSelectionListener listener)
public void removeKeYSelectionListener(KeYSelectionListener listener)
public void fireSelectedNodeChanged()
public void fireSelectedProofChanged()