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 |
---|---|
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 . |
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
|
abstract void |
loadProofFromBundle(java.io.File proofBundle,
java.io.File proofFilename)
Loads the proof with the given filename from the proof bundle with the given path.
|
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 . |
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
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 proofpublic abstract void loadProofFromBundle(java.io.File proofBundle, java.io.File proofFilename)
proofBundle
- the File with the problem description or the proofproofFilename
- the filename of the proof in the bundlepublic 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)
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.Copyright © 2003-2019 The KeY-Project.