public class DefaultUserInterfaceControl extends AbstractUserInterfaceControl
DefaultUserInterfaceControl
which allows proving in case
that no specific user interface is available.
In case that no user interface should be used see also KeYEnvironment
which provides static methods to load source code and to instantiate this
class.
KeYEnvironment
ProgressMonitor.Empty
Modifier and Type | Field and Description |
---|---|
private DefaultProofControl |
proofControl
The used
DefaultProofControl . |
private TermLabelVisibilityManager |
termLabelVisibilityManager
The used
TermLabelVisibilityManager . |
Constructor and Description |
---|
DefaultUserInterfaceControl()
Constructor.
|
DefaultUserInterfaceControl(RuleCompletionHandler customization)
Constructor.
|
Modifier and Type | Method and Description |
---|---|
ProofEnvironment |
createProofEnvironmentAndRegisterProof(ProofOblInput proofOblInput,
ProofAggregate proofList,
InitConfig initConfig)
registers the proof aggregate at the UI
|
DefaultProofControl |
getProofControl()
Returns the used
ProofControl . |
TermLabelVisibilityManager |
getTermLabelVisibilityManager()
Returns the
TermLabelVisibilityManager . |
void |
progressStarted(java.lang.Object sender) |
void |
progressStopped(java.lang.Object sender) |
void |
registerProofAggregate(ProofAggregate pa)
Registers an already created
ProofAggregate in this UserInterfaceControl . |
void |
reportException(java.lang.Object sender,
ProofOblInput input,
java.lang.Exception e) |
void |
reportStatus(java.lang.Object sender,
java.lang.String status) |
void |
reportStatus(java.lang.Object sender,
java.lang.String status,
int progress) |
void |
reportWarnings(ImmutableSet<PositionedString> warnings)
Report the occurred warnings.
|
void |
resetStatus(java.lang.Object sender) |
boolean |
selectProofObligation(InitConfig initConfig)
This method is called if no
IPersistablePO.LoadedPOContainer was created
via AbstractProblemLoader.createProofObligationContainer() and can be overwritten
for instance to open the proof management dialog as done by ProblemLoader . |
void |
setMaximum(int maximum)
Set the maximum number of steps for this task.
|
void |
setProgress(int progress)
Set the progress achieved so far.
|
addProverTaskListener, createProblemInitializer, createProof, fireTaskFinished, fireTaskProgress, fireTaskStarted, isAtLeastOneMacroRunning, load, loadingFinished, loadingStarted, macroFinished, macroStarted, proofCreated, removeProverTaskListener, taskFinished, taskProgress, taskStarted
private final TermLabelVisibilityManager termLabelVisibilityManager
TermLabelVisibilityManager
.private final DefaultProofControl proofControl
DefaultProofControl
.public DefaultUserInterfaceControl()
public DefaultUserInterfaceControl(RuleCompletionHandler customization)
customization
- An optional RuleCompletionHandler
.public DefaultProofControl getProofControl()
ProofControl
.ProofControl
.public ProofEnvironment createProofEnvironmentAndRegisterProof(ProofOblInput proofOblInput, ProofAggregate proofList, InitConfig initConfig)
createProofEnvironmentAndRegisterProof
in class AbstractUserInterfaceControl
proofOblInput
- the ProofOblInput
proofList
- the ProofAggregate
initConfig
- the InitConfig
to be usedProofEnvironment
where the ProofAggregate
has been registeredpublic boolean selectProofObligation(InitConfig initConfig)
IPersistablePO.LoadedPOContainer
was created
via AbstractProblemLoader.createProofObligationContainer()
and can be overwritten
for instance to open the proof management dialog as done by ProblemLoader
.public void progressStarted(java.lang.Object sender)
public void progressStopped(java.lang.Object sender)
public void reportStatus(java.lang.Object sender, java.lang.String status, int progress)
public void reportStatus(java.lang.Object sender, java.lang.String status)
public void resetStatus(java.lang.Object sender)
public void reportException(java.lang.Object sender, ProofOblInput input, java.lang.Exception e)
public void setProgress(int progress)
progress
has to be >=0 and <= to the maximum
value previously set with ProgressMonitor.setMaximum(int)
.progress
- number of steps completedpublic void setMaximum(int maximum)
maximum
- maximum number of steps, >=0.public void registerProofAggregate(ProofAggregate pa)
ProofAggregate
in this UserInterfaceControl
.pa
- The ProofAggregate
to register.public void reportWarnings(ImmutableSet<PositionedString> warnings)
warnings
- The occurred warnings.public TermLabelVisibilityManager getTermLabelVisibilityManager()
TermLabelVisibilityManager
.TermLabelVisibilityManager
.