public class KeYMediator
extends java.lang.Object
KeYMediator
provides control logic for the user interface implemented in Swing.
Attention: Logic to apply rules has to be implemented user interface independent in the ProofControl
!
Modifier and Type | Class and Description |
---|---|
private class |
KeYMediator.KeYMediatorProofListener |
(package private) class |
KeYMediator.KeYMediatorProofTreeListener |
(package private) class |
KeYMediator.KeYMediatorSelectionListener |
Modifier and Type | Field and Description |
---|---|
private AutoSaver |
autoSaver
An optional used
AutoSaver . |
private TacletFilter |
filterForInteractiveProving |
private int |
goalsClosedByAutoMode |
private boolean |
inAutoMode
boolean flag indicating if the GUI is in auto mode
|
private KeYSelectionModel |
keySelectionModel
current proof and node the user works with.
|
private javax.swing.event.EventListenerList |
listenerList
listenerList with to gui listeners
|
private NotationInfo |
notationInfo
the notation info used to print sequents
|
private KeYMediator.KeYMediatorProofListener |
proofListener
listens to the proof
|
private KeYMediator.KeYMediatorProofTreeListener |
proofTreeListener
listens to the ProofTree
|
private AbstractMediatorUserInterfaceControl |
ui
The user interface
|
Constructor and Description |
---|
KeYMediator(AbstractMediatorUserInterfaceControl ui)
creates the KeYMediator with a reference to the application's
main frame and the current proof settings
|
Modifier and Type | Method and Description |
---|---|
void |
addGUIListener(GUIListener listener)
adds a listener to GUI events
|
void |
addInterruptedListener(InterruptListener listener) |
void |
addKeYSelectionListener(KeYSelectionListener listener)
adds a listener to the KeYSelectionModel, so that the listener
will be informed if the proof or node the user has selected
changed
|
Namespace<Choice> |
choice_ns()
returns the choice namespace
|
void |
closedAGoal() |
void |
enableWhenProofLoaded(javax.swing.AbstractButton a)
Deprecated.
|
void |
enableWhenProofLoaded(javax.swing.Action a) |
boolean |
ensureProofLoaded() |
private void |
finishSetBack(Proof proof) |
void |
fireModalDialogClosed(java.util.EventObject e)
fires that a GUI component that has asked for modal access
has been closed, so views can be enabled again
|
void |
fireModalDialogOpened(java.util.EventObject e)
fires the request of a GUI component for modal access
this can be used to disable all views even if the GUI component
has no built in modal support
|
void |
fireShutDown(java.util.EventObject e)
Fires the shut down event.
|
void |
freeModalAccess(java.lang.Object src)
called if no more modal access is needed
|
Namespace<Function> |
func_ns()
returns the function namespace
|
long |
getAutomaticApplicationTimeout()
besides the number of rule applications it is possible to define a timeout after which rule application
shall be terminated
|
AutoSaver |
getAutoSaver()
Returns the
AutoSaver to use. |
TacletFilter |
getFilterForInteractiveProving()
Returns a filter that is used for filtering taclets that should not be showed while
interactive proving.
|
JavaInfo |
getJavaInfo()
returns the JavaInfo with the java type information
|
int |
getMaxAutomaticSteps()
returns the maximum number of rule applications allowed in
automatic mode
|
NotationInfo |
getNotationInfo()
returns the used NotationInfo
|
int |
getNrGoalsClosedByAutoMode() |
Profile |
getProfile()
return the chosen profile
|
Goal |
getSelectedGoal()
returns the current selected goal
|
Node |
getSelectedNode()
returns the current selected node
|
Proof |
getSelectedProof()
returns the current selected proof
|
KeYSelectionModel |
getSelectionModel()
returns the current selected goal
|
Services |
getServices()
returns the Services with the java service classes
|
AbstractMediatorUserInterfaceControl |
getUI()
returns the user interface
|
void |
goalChosen(Goal goal)
sets the current goal
|
Namespace<RuleSet> |
heur_ns()
returns the heuristics namespace
|
void |
interrupt()
Interrupts all registered
InterruptListener s. |
boolean |
isInAutoMode()
Checks if the auto mode is currently running.
|
NamespaceSet |
namespaces()
returns the namespace set
|
void |
nonGoalNodeChosen(Node node)
notifies that a node that is not a goal has been chosen
|
void |
notify(NotificationEvent event)
takes a notification event and informs the notification
manager
|
boolean |
processDelayedCut(Node invokedNode) |
Namespace<IProgramVariable> |
progVar_ns()
returns the program variable namespace
|
void |
removeGUIListener(GUIListener listener)
adds a listener to GUI events
|
void |
removeInterruptedListener(InterruptListener listener) |
void |
removeKeYSelectionListener(KeYSelectionListener listener)
removes a listener from the KeYSelectionModel
|
void |
requestModalAccess(java.lang.Object src)
called to ask for modal access
|
void |
resetNrGoalsClosedByHeuristics() |
void |
setAutomaticApplicationTimeout(long timeout)
sets the time out after which automatic rule application stops
|
void |
setAutoSave(int interval) |
void |
setBack(Goal goal) |
void |
setBack(Node node) |
void |
setInteractive(boolean b)
Switches interactive mode on or off.
|
void |
setMaxAutomaticSteps(int steps)
sets the maximum number of rule applications allowed in
automatic mode
|
void |
setProof(Proof p)
initializes proof (this is Swing thread-safe)
|
private void |
setProofHelper(Proof newProof) |
Namespace<Sort> |
sort_ns()
returns the sort namespace
|
void |
startInterface(boolean fullStop) |
void |
stopInterface(boolean fullStop) |
Namespace<QuantifiableVariable> |
var_ns()
returns the variable namespace
|
private AbstractMediatorUserInterfaceControl ui
private final NotationInfo notationInfo
private javax.swing.event.EventListenerList listenerList
private KeYMediator.KeYMediatorProofListener proofListener
private KeYMediator.KeYMediatorProofTreeListener proofTreeListener
private KeYSelectionModel keySelectionModel
private TacletFilter filterForInteractiveProving
private boolean inAutoMode
private int goalsClosedByAutoMode
public KeYMediator(AbstractMediatorUserInterfaceControl ui)
public NotationInfo getNotationInfo()
public Namespace<QuantifiableVariable> var_ns()
public Namespace<IProgramVariable> progVar_ns()
public Namespace<Function> func_ns()
public Namespace<RuleSet> heur_ns()
public Namespace<Choice> choice_ns()
public NamespaceSet namespaces()
public JavaInfo getJavaInfo()
public Services getServices()
public void setAutoSave(int interval)
public boolean ensureProofLoaded()
public TacletFilter getFilterForInteractiveProving()
public void setBack(Node node)
public void setBack(Goal goal)
private void finishSetBack(Proof proof)
public void setProof(Proof p)
private void setProofHelper(Proof newProof)
public void setMaxAutomaticSteps(int steps)
steps
- an int setting the limitpublic int getMaxAutomaticSteps()
public void addKeYSelectionListener(KeYSelectionListener listener)
listener
- the KeYSelectionListener to addpublic void removeKeYSelectionListener(KeYSelectionListener listener)
listener
- the KeYSelectionListener to be removedpublic void addGUIListener(GUIListener listener)
listener
- the GUIListener to be addedpublic void removeGUIListener(GUIListener listener)
listener
- the GUIListener to be addedpublic void addInterruptedListener(InterruptListener listener)
public void removeInterruptedListener(InterruptListener listener)
public void goalChosen(Goal goal)
goal
- the Goal being displayed in the view of the sequentpublic AbstractMediatorUserInterfaceControl getUI()
public void nonGoalNodeChosen(Node node)
node
- the node being displayed in the view of the sequentpublic void requestModalAccess(java.lang.Object src)
src
- Object that is the asking componentpublic void freeModalAccess(java.lang.Object src)
src
- Object that is the asking componentpublic void fireModalDialogOpened(java.util.EventObject e)
public void fireModalDialogClosed(java.util.EventObject e)
public void fireShutDown(java.util.EventObject e)
public Proof getSelectedProof()
#getProof()
public Goal getSelectedGoal()
public KeYSelectionModel getSelectionModel()
public Node getSelectedNode()
public void interrupt()
InterruptListener
s.public void setInteractive(boolean b)
b
- true iff interactive mode is to be turned onpublic void closedAGoal()
public int getNrGoalsClosedByAutoMode()
public void resetNrGoalsClosedByHeuristics()
public void stopInterface(boolean fullStop)
public void startInterface(boolean fullStop)
public boolean isInAutoMode()
true
auto mode is running, false
auto mode is not
running.public void enableWhenProofLoaded(javax.swing.Action a)
@Deprecated public void enableWhenProofLoaded(javax.swing.AbstractButton a)
public void notify(NotificationEvent event)
event
- the NotificationEventpublic Profile getProfile()
public long getAutomaticApplicationTimeout()
public void setAutomaticApplicationTimeout(long timeout)
timeout
- a long specifying the timeout time in mspublic boolean processDelayedCut(Node invokedNode)