de.uka.ilkd.key.core

Class KeYSelectionModel

java.lang.Object

de.uka.ilkd.key.core.KeYSelectionModel

public class KeYSelectionModel
extends java.lang.Object

Nested Class Summary

Nested Classes

Modifier and Type	Class and Description
protected class	KeYSelectionModel.DefaultSelectionIterator enumerate the possible goal selections, starting with the best one

Field Summary

Fields

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 Summary

Constructors

Constructor and Description
KeYSelectionModel()

Method Summary

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

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Field Detail

proof

private Proof proof

the proof to listen to

goalIsValid

private boolean goalIsValid

if true the selectedGoal field below can be trusted

selectedGoal

private Goal selectedGoal

is the selected node a goal

selectedNode

private Node selectedNode

the current displayed node

listenerList

private final java.util.List<KeYSelectionListener> listenerList

the listeners to this model

selectionEvent

private KeYSelectionEvent selectionEvent

cached selected node event

Constructor Detail

KeYSelectionModel

public KeYSelectionModel()

Method Detail

setProof

public void setProof(Proof p)

Does not take care of GUI effects

setSelectedProof

public void setSelectedProof(Proof p)

sets the selected proof

Parameters:

p - the Proof that is selected

getSelectedProof

public Proof getSelectedProof()

returns the proof that is selected by the user

Returns:

the proof that is selected by the user

setSelectedNode

public void setSelectedNode(Node n)

sets the node that is focused by the user

Parameters:

n - the selected node

setSelectedGoal

public void setSelectedGoal(Goal g)

sets the node that is focused by the user

Parameters:

g - the Goal that contains the selected node

getSelectedNode

public Node getSelectedNode()

returns the node that is selected by the user

Returns:

the node that is selected by the user

getSelectedGoal

public Goal getSelectedGoal()

returns the goal the selected node belongs to, null if it is an inner node

Returns:

the goal the selected node belongs to, null if it is an inner node

isGoal

public boolean isGoal()

returns true iff the selected node is a goal

Returns:

true iff the selected node is a goal

defaultSelection

public void defaultSelection()

selects the first goal in the goal list of proof if available if not it selects a leaf of the proof tree

nearestOpenGoalSelection

public void nearestOpenGoalSelection(Node old)

selects the first open goal below the given node old if no open goal is available node old is selected. In case that old has been removed from the proof the proof root is selected

Parameters:

old - the Node to start looking for open goals

getFirstOpenGoalBelow

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

Parameters:

n - the Node where to start from

Returns:

the goal containing the first leaf of the subtree starting at n, which is not already closed. null is returned if no such goal exists.

addKeYSelectionListener

public void addKeYSelectionListener(KeYSelectionListener listener)

removeKeYSelectionListener

public void removeKeYSelectionListener(KeYSelectionListener listener)

fireSelectedNodeChanged

public void fireSelectedNodeChanged()

fireSelectedProofChanged

public void fireSelectedProofChanged()