public abstract class AbstractMediatorUserInterfaceControl extends AbstractUserInterfaceControl implements RuleCompletionHandler, ProofEnvironmentListener, ProofDisposedListener
UserInterfaceControl
for
user interfaces in which a KeYMediator
is available.ProgressMonitor.Empty
Modifier and Type | Field and Description |
---|---|
private ProofMacro |
autoMacro |
private MediatorProofControl |
proofControl |
protected boolean |
saveOnly |
Constructor and Description |
---|
AbstractMediatorUserInterfaceControl() |
Modifier and Type | Method and Description |
---|---|
boolean |
applyMacro() |
boolean |
confirmTaskRemoval(java.lang.String string)
asks if removal of a task is completed.
|
protected MediatorProofControl |
createProofControl() |
ProofEnvironment |
createProofEnvironmentAndRegisterProof(ProofOblInput proofOblInput,
ProofAggregate proofList,
InitConfig initConfig)
registers the proof aggregate at the UI
|
ProofMacro |
getMacro() |
abstract KeYMediator |
getMediator()
Returns the used
KeYMediator . |
protected ProblemLoader |
getProblemLoader(java.io.File file,
java.util.List<java.io.File> classPath,
java.io.File bootClassPath,
java.util.List<java.io.File> includes,
KeYMediator mediator) |
MediatorProofControl |
getProofControl()
Returns the used
ProofControl . |
boolean |
isSaveOnly() |
abstract void |
loadProblem(java.io.File file)
loads the problem or proof from the given file
|
boolean |
macroChosen() |
protected void |
macroFinished(ProofMacroFinishedInfo info) |
protected void |
macroSideProofDisposing(ProofMacroFinishedInfo initiatingInfo,
Proof initiatingProof,
Proof sideProof) |
abstract void |
notify(NotificationEvent event) |
void |
notifyAutoModeBeingStarted()
these methods are called immediately before automode is started to ensure that
the GUI can respond in a reasonable way, e.g., change the cursor to a waiting cursor
|
void |
notifyAutomodeStopped()
these methods are called when automode has been stopped to ensure that
the GUI can respond in a reasonable way, e.g., change the cursor to the default
|
abstract void |
openExamples()
called to open the build in examples
|
void |
proofDisposed(ProofDisposedEvent e)
When a
Proof was disposed via Proof.dispose() . |
void |
proofDisposing(ProofDisposedEvent e)
When a
Proof is going to be disposed. |
void |
proofRegistered(ProofEnvironmentEvent event) |
void |
proofUnregistered(ProofEnvironmentEvent event) |
void |
registerProofAggregate(ProofAggregate pa)
Registers an already created
ProofAggregate in this UserInterfaceControl . |
private void |
saveSideProof(Proof proof)
Try to save a side proof.
|
void |
setMacro(ProofMacro macro) |
void |
setSaveOnly(boolean s) |
addProverTaskListener, createProblemInitializer, createProof, fireTaskFinished, fireTaskProgress, fireTaskStarted, isAtLeastOneMacroRunning, load, loadingFinished, loadingStarted, macroStarted, proofCreated, removeProverTaskListener, taskFinished, taskProgress, taskStarted
clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait
completeAndApplyTacletMatch, completeBuiltInRuleApp
getTermLabelVisibilityManager
reportWarnings, selectProofObligation
progressStarted, progressStopped, reportException, reportStatus, reportStatus, resetStatus
setMaximum, setProgress
protected boolean saveOnly
private final MediatorProofControl proofControl
private ProofMacro autoMacro
public AbstractMediatorUserInterfaceControl()
public MediatorProofControl getProofControl()
UserInterfaceControl
ProofControl
.getProofControl
in interface UserInterfaceControl
ProofControl
.protected MediatorProofControl createProofControl()
public void setSaveOnly(boolean s)
public boolean isSaveOnly()
public void setMacro(ProofMacro macro)
public ProofMacro getMacro()
public boolean macroChosen()
public abstract void openExamples()
public abstract KeYMediator getMediator()
KeYMediator
.KeYMediator
.public abstract void loadProblem(java.io.File file)
file
- the File with the problem description or the proofprotected ProblemLoader getProblemLoader(java.io.File file, java.util.List<java.io.File> classPath, java.io.File bootClassPath, java.util.List<java.io.File> includes, KeYMediator mediator)
public boolean applyMacro()
protected void macroFinished(ProofMacroFinishedInfo info)
macroFinished
in class AbstractUserInterfaceControl
protected void macroSideProofDisposing(ProofMacroFinishedInfo initiatingInfo, Proof initiatingProof, Proof sideProof)
private void saveSideProof(Proof proof)
proof
- 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 void proofUnregistered(ProofEnvironmentEvent event)
proofUnregistered
in interface ProofEnvironmentListener
public void notifyAutoModeBeingStarted()
public void notifyAutomodeStopped()
public abstract void notify(NotificationEvent event)
public boolean confirmTaskRemoval(java.lang.String string)
message
- public void proofDisposing(ProofDisposedEvent e)
Proof
is going to be disposed.proofDisposing
in interface ProofDisposedListener
e
- The event.public void proofDisposed(ProofDisposedEvent e)
Proof
was disposed via Proof.dispose()
.proofDisposed
in interface ProofDisposedListener
e
- The event.public void proofRegistered(ProofEnvironmentEvent event)
proofRegistered
in interface ProofEnvironmentListener
public void registerProofAggregate(ProofAggregate pa)
ProofAggregate
in this UserInterfaceControl
.registerProofAggregate
in interface UserInterfaceControl
pa
- The ProofAggregate
to register.