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
!
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() |
<T> void |
deregister(T obj,
java.lang.Class<T> service)
Remove a previous registered user-defined data.
|
void |
enableWhenProofLoaded(javax.swing.AbstractButton a)
Deprecated.
|
void |
enableWhenProofLoaded(javax.swing.Action a) |
boolean |
ensureProofLoaded() |
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. |
javax.swing.DefaultListModel<Proof> |
getCurrentlyOpenedProofs()
Provides a list of currently opened view.
|
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
|
Lookup |
getUserData()
Get the assocated lookup of user-defined data.
|
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.
|
<T> T |
lookup(java.lang.Class<T> service)
Retrieves a user-defined data.
|
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
|
<T> void |
register(T obj,
java.lang.Class<T> service)
Register a user-defined data in this node info.
|
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)
Selects the specified proof and initializes it.
|
Namespace<Sort> |
sort_ns()
returns the sort namespace
|
void |
startInterface(boolean fullStop) |
void |
stopInterface(boolean fullStop) |
Namespace<QuantifiableVariable> |
var_ns()
returns the variable namespace
|
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)
public void setProof(Proof p)
p
- the proof to select.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 <T> T lookup(java.lang.Class<T> service)
T
- any classservice
- the class for which the data were registeredregister(Object, Class)
public <T> void register(T obj, java.lang.Class<T> service)
T
- obj
- an object to be registeredservice
- the key under it should be registeredpublic <T> void deregister(T obj, java.lang.Class<T> service)
T
- arbitray objectobj
- registered objectservice
- the key under which the data was registered@Nonnull public Lookup getUserData()
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)
@Nonnull public javax.swing.DefaultListModel<Proof> getCurrentlyOpenedProofs()
You can use this instance directly inside your components or add a listener to observe changes.
AbstractListModel.addListDataListener(javax.swing.event.ListDataListener)
Copyright © 2003-2019 The KeY-Project.