Package | Description |
---|---|
de.uka.ilkd.key.control | |
de.uka.ilkd.key.gui |
This package contains classes forming the graphical user interface of KeY.
|
de.uka.ilkd.key.informationflow.macros | |
de.uka.ilkd.key.macros | |
de.uka.ilkd.key.proof.io |
Classes related to loading and saving proof files.
|
de.uka.ilkd.key.prover | |
de.uka.ilkd.key.prover.impl | |
de.uka.ilkd.key.ui | |
de.uka.ilkd.key.util |
This package is a grab bag of miscellaneous useful code fragments.
|
Modifier and Type | Class and Description |
---|---|
static class |
AbstractProofControl.FocussedAutoModeTaskListener
TODO
|
class |
AbstractUserInterfaceControl
Provides a basic implementation of
UserInterfaceControl . |
class |
CompositePTListener
A composite structure for prover task listeners.
|
class |
DefaultUserInterfaceControl
The
DefaultUserInterfaceControl which allows proving in case
that no specific user interface is available. |
Modifier and Type | Method and Description |
---|---|
ProverTaskListener |
AbstractProofControl.getDefaultProverTaskListener()
Returns the default
ProverTaskListener which will be added to all started ApplyStrategy instances. |
ProverTaskListener |
ProofControl.getDefaultProverTaskListener()
Returns the default
ProverTaskListener which will be added to all started ApplyStrategy instances. |
Modifier and Type | Method and Description |
---|---|
void |
AbstractUserInterfaceControl.addProverTaskListener(ProverTaskListener ptl)
Registers the given
ProverTaskListener which will be informed about all events. |
void |
UserInterfaceControl.addProverTaskListener(ProverTaskListener ptl)
Registers the given
ProverTaskListener which will be informed about all events. |
void |
AbstractUserInterfaceControl.removeProverTaskListener(ProverTaskListener ptl)
Removes the given
ProverTaskListener . |
void |
UserInterfaceControl.removeProverTaskListener(ProverTaskListener ptl)
Removes the given
ProverTaskListener . |
void |
DefaultProofControl.startAutoMode(Proof proof,
ImmutableList<Goal> goals,
ProverTaskListener ptl) |
protected abstract void |
AbstractProofControl.startAutoMode(Proof proof,
ImmutableList<Goal> goals,
ProverTaskListener ptl) |
Constructor and Description |
---|
AbstractProofControl(ProverTaskListener defaultProverTaskListener)
Constructor.
|
AbstractProofControl(ProverTaskListener defaultProverTaskListener,
RuleCompletionHandler ruleCompletionHandler)
Constructor.
|
CompositePTListener(ProverTaskListener[] l) |
CompositePTListener(ProverTaskListener ptl1,
ProverTaskListener ptl2) |
Modifier and Type | Class and Description |
---|---|
class |
WindowUserInterfaceControl
Implementation of
UserInterfaceControl which controls the MainWindow
with the typical user interface of KeY. |
Modifier and Type | Class and Description |
---|---|
static class |
ProofMacro.ProgressBarListener
This observer acts as intermediate instance between the reports by the
strategy and the UI reporting progress.
|
class |
ProofMacroListener
Listener for the application of proof macros (which may be run in
a separate worker thread).
|
Constructor and Description |
---|
ProgressBarListener(int size,
int numberSteps,
ProverTaskListener listener) |
ProofMacroListener(java.lang.String macroName,
ProverTaskListener listener) |
Modifier and Type | Class and Description |
---|---|
class |
AutoSaver
Saves intermediate proof artifacts during strategy execution.
|
Constructor and Description |
---|
ProblemLoader(java.io.File file,
java.util.List<java.io.File> classPath,
java.io.File bootClassPath,
java.util.List<java.io.File> includes,
Profile profileOfNewProofs,
boolean forceNewProfileOfNewProofs,
KeYMediator mediator,
boolean askUiToSelectAProofObligationIfNotDefinedByLoadedFile,
java.util.Properties poPropertiesToForce,
ProverTaskListener ptl) |
Modifier and Type | Method and Description |
---|---|
void |
ProverCore.addProverTaskObserver(ProverTaskListener observer)
adds a task listener
|
void |
ProverCore.removeProverTaskObserver(ProverTaskListener observer)
removes a task listener
|
Modifier and Type | Method and Description |
---|---|
void |
AbstractProverCore.addProverTaskObserver(ProverTaskListener observer)
adds a listener to the prover
|
void |
AbstractProverCore.removeProverTaskObserver(ProverTaskListener observer)
removes a listener from the prover
|
Modifier and Type | Class and Description |
---|---|
class |
AbstractMediatorUserInterfaceControl
Provides a basic implementation of
UserInterfaceControl for
user interfaces in which a KeYMediator is available. |
class |
ConsoleUserInterfaceControl
Implementation of
UserInterfaceControl used by command line interface of KeY. |
Modifier and Type | Method and Description |
---|---|
void |
MediatorProofControl.startAutoMode(Proof proof,
ImmutableList<Goal> goals,
ProverTaskListener ptl) |
Constructor and Description |
---|
ProofStarter(ProverTaskListener ptl,
boolean useAutoSaver)
creates an instance of the ProofStarter
|
Copyright © 2003-2019 The KeY-Project.