public class WindowUserInterfaceControl extends AbstractMediatorUserInterfaceControl
UserInterfaceControl
which controls the MainWindow
with the typical user interface of KeY.ProgressMonitor.Empty
Modifier and Type | Field and Description |
---|---|
private java.util.LinkedList<InteractiveRuleApplicationCompletion> |
completions |
private MainWindow |
mainWindow |
saveOnly
Constructor and Description |
---|
WindowUserInterfaceControl(MainWindow mainWindow) |
Modifier and Type | Method and Description |
---|---|
void |
completeAndApplyTacletMatch(TacletInstantiationModel[] models,
Goal goal)
called to complete and apply a taclet instantiations
|
IBuiltInRuleApp |
completeBuiltInRuleApp(IBuiltInRuleApp app,
Goal goal,
boolean forced)
completes rule applications of built in rules
|
boolean |
confirmTaskRemoval(java.lang.String string)
asks if removal of a task is completed.
|
protected MediatorProofControl |
createProofControl() |
protected static Pair<java.io.File,java.lang.String> |
fileName(Proof proof,
java.lang.String fileExtension) |
KeYMediator |
getMediator()
Returns the used
KeYMediator . |
TermLabelVisibilityManager |
getTermLabelVisibilityManager()
Returns the
TermLabelVisibilityManager . |
protected boolean |
inStopAtFirstUncloseableGoalMode(Proof proof) |
AbstractProblemLoader |
load(Profile profile,
java.io.File file,
java.util.List<java.io.File> classPath,
java.io.File bootClassPath,
java.util.List<java.io.File> includes,
java.util.Properties poPropertiesToForce,
boolean forceNewProfileOfNewProofs)
Opens a java file in this
UserInterfaceControl and returns the instantiated AbstractProblemLoader
which can be used to instantiated proofs programmatically. |
void |
loadingFinished(AbstractProblemLoader loader,
IPersistablePO.LoadedPOContainer poContainer,
ProofAggregate proofList,
AbstractProblemLoader.ReplayResult result)
The loading has stopped.
|
void |
loadingStarted(AbstractProblemLoader loader)
The loading has started.
|
static KeYEnvironment<WindowUserInterfaceControl> |
loadInMainWindow(java.io.File location,
java.util.List<java.io.File> classPaths,
java.io.File bootClassPath,
java.util.List<java.io.File> includes,
boolean makeMainWindowVisible)
Loads the given location and returns all required references as
KeYEnvironment
with KeY's MainWindow . |
static KeYEnvironment<WindowUserInterfaceControl> |
loadInMainWindow(Profile profile,
java.io.File location,
java.util.List<java.io.File> classPaths,
java.io.File bootClassPath,
java.util.List<java.io.File> includes,
boolean forceNewProfileOfNewProofs,
boolean makeMainWindowVisible)
Loads the given location and returns all required references as
KeYEnvironment
with KeY's MainWindow . |
void |
loadProblem(java.io.File file)
loads the problem or proof from the given file
|
void |
loadProblem(java.io.File file,
java.util.List<java.io.File> classPath,
java.io.File bootClassPath,
java.util.List<java.io.File> includes)
loads the problem or proof from the given file
|
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
|
void |
openExamples()
called to open the build in examples
|
void |
progressStarted(java.lang.Object sender) |
void |
progressStopped(java.lang.Object sender) |
void |
proofDisposing(ProofDisposedEvent e)
When a
Proof is going to be disposed. |
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) |
java.io.File |
saveProof(Proof proof,
java.lang.String fileExtension)
save proof in file.
|
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.
|
void |
taskFinished(TaskFinishedInfo info)
Called when a task is finished.
|
void |
taskProgress(int position)
Called when progress is made on a task.
|
void |
taskStarted(TaskStartedInfo info) |
applyMacro, createProofEnvironmentAndRegisterProof, getMacro, getProblemLoader, getProofControl, isSaveOnly, macroChosen, macroFinished, macroSideProofDisposing, proofDisposed, proofRegistered, proofUnregistered, setMacro, setSaveOnly
addProverTaskListener, createProblemInitializer, createProof, fireTaskFinished, fireTaskProgress, fireTaskStarted, isAtLeastOneMacroRunning, macroStarted, proofCreated, removeProverTaskListener
private final MainWindow mainWindow
private final java.util.LinkedList<InteractiveRuleApplicationCompletion> completions
public WindowUserInterfaceControl(MainWindow mainWindow)
protected MediatorProofControl createProofControl()
createProofControl
in class AbstractMediatorUserInterfaceControl
public void loadProblem(java.io.File file, java.util.List<java.io.File> classPath, java.io.File bootClassPath, java.util.List<java.io.File> includes)
file
- the File with the problem description or the proofclassPath
- the class path entries to use.bootClassPath
- the boot class path to use.public void loadProblem(java.io.File file)
AbstractMediatorUserInterfaceControl
loadProblem
in class AbstractMediatorUserInterfaceControl
file
- the File with the problem description or the proofpublic void progressStarted(java.lang.Object sender)
public void progressStopped(java.lang.Object sender)
public void reportException(java.lang.Object sender, ProofOblInput input, java.lang.Exception e)
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 taskFinished(TaskFinishedInfo info)
ProverTaskListener
taskFinished
in interface ProverTaskListener
taskFinished
in class AbstractUserInterfaceControl
info
- a TaskFinishedInfo object with additional informationprotected boolean inStopAtFirstUncloseableGoalMode(Proof proof)
public void taskProgress(int position)
ProverTaskListener
taskProgress
in interface ProverTaskListener
taskProgress
in class AbstractUserInterfaceControl
position
- indicates how much work has been done relative to the value of
size
passed in ProverTaskListener.taskStarted(TaskStartedInfo)
.public void taskStarted(TaskStartedInfo info)
taskStarted
in interface ProverTaskListener
taskStarted
in class AbstractUserInterfaceControl
public void setMaximum(int maximum)
ProgressMonitor
maximum
- maximum number of steps, >=0.public void setProgress(int progress)
ProgressMonitor
progress
has to be >=0 and <= to the maximum
value previously set with ProgressMonitor.setMaximum(int)
.progress
- number of steps completedpublic void notifyAutoModeBeingStarted()
AbstractMediatorUserInterfaceControl
notifyAutoModeBeingStarted
in class AbstractMediatorUserInterfaceControl
public void notifyAutomodeStopped()
AbstractMediatorUserInterfaceControl
notifyAutomodeStopped
in class AbstractMediatorUserInterfaceControl
public void completeAndApplyTacletMatch(TacletInstantiationModel[] models, Goal goal)
RuleCompletionHandler
models
- the partial models with all different possible instantiations found automaticallygoal
- the Goal where to applypublic boolean confirmTaskRemoval(java.lang.String string)
AbstractMediatorUserInterfaceControl
confirmTaskRemoval
in class AbstractMediatorUserInterfaceControl
public void openExamples()
AbstractMediatorUserInterfaceControl
openExamples
in class AbstractMediatorUserInterfaceControl
public IBuiltInRuleApp completeBuiltInRuleApp(IBuiltInRuleApp app, Goal goal, boolean forced)
RuleCompletionHandler
app
- the DefaultBuiltInRuleApp to be completedgoal
- the Goal where the app will later be applied toforced
- a boolean indicating if the rule should be applied without any
additional interaction from the user provided that the application object can be
made complete automaticallypublic KeYMediator getMediator()
KeYMediator
.getMediator
in class AbstractMediatorUserInterfaceControl
KeYMediator
.public AbstractProblemLoader load(Profile profile, java.io.File file, java.util.List<java.io.File> classPath, java.io.File bootClassPath, java.util.List<java.io.File> includes, java.util.Properties poPropertiesToForce, boolean forceNewProfileOfNewProofs) throws ProblemLoaderException
Opens a java file in this UserInterfaceControl
and returns the instantiated AbstractProblemLoader
which can be used to instantiated proofs programmatically.
The loading is performed in the Thread
of the caller!
load
in interface UserInterfaceControl
load
in class AbstractUserInterfaceControl
profile
- An optional Profile
to use. If it is null
the default profile AbstractProfile.getDefaultProfile()
is used.file
- The java file to open.classPath
- The class path entries to use.bootClassPath
- The boot class path to use.includes
- Optional includes to consider.poPropertiesToForce
- Some optional Properties
for the PO which extend or overwrite saved PO Properties
.forceNewProfileOfNewProofs
- true
AbstractProblemLoader.profileOfNewProofs
will be used as
Profile
of new proofs, false
Profile
specified by problem file will be used for new proofs.AbstractProblemLoader
.ProblemLoaderException
- Occurred Exception.public java.io.File saveProof(Proof proof, java.lang.String fileExtension)
protected static Pair<java.io.File,java.lang.String> fileName(Proof proof, java.lang.String fileExtension)
public void proofDisposing(ProofDisposedEvent e)
Proof
is going to be disposed.proofDisposing
in interface ProofDisposedListener
proofDisposing
in class AbstractMediatorUserInterfaceControl
e
- The event.public boolean selectProofObligation(InitConfig initConfig)
ProblemLoaderControl
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 registerProofAggregate(ProofAggregate pa)
AbstractMediatorUserInterfaceControl
ProofAggregate
in this UserInterfaceControl
.registerProofAggregate
in interface UserInterfaceControl
registerProofAggregate
in class AbstractMediatorUserInterfaceControl
pa
- The ProofAggregate
to register.public void loadingStarted(AbstractProblemLoader loader)
ProblemLoaderControl
loadingStarted
in interface ProblemLoaderControl
loadingStarted
in class AbstractUserInterfaceControl
loader
- The source AbstractProblemLoader
.public void loadingFinished(AbstractProblemLoader loader, IPersistablePO.LoadedPOContainer poContainer, ProofAggregate proofList, AbstractProblemLoader.ReplayResult result) throws ProblemLoaderException
ProblemLoaderControl
loadingFinished
in interface ProblemLoaderControl
loadingFinished
in class AbstractUserInterfaceControl
loader
- The source AbstractProblemLoader
.poContainer
- The loaded IPersistablePO.LoadedPOContainer
.proofList
- The created ProofAggregate
.result
- The occurred AbstractProblemLoader.ReplayResult
.ProblemLoaderException
- Occurred Exception.public static KeYEnvironment<WindowUserInterfaceControl> loadInMainWindow(java.io.File location, java.util.List<java.io.File> classPaths, java.io.File bootClassPath, java.util.List<java.io.File> includes, boolean makeMainWindowVisible) throws ProblemLoaderException
KeYEnvironment
with KeY's MainWindow
.location
- The location to load.classPaths
- The class path entries to use.bootClassPath
- The boot class path to use.includes
- Optional includes to consider.makeMainWindowVisible
- Make KeY's MainWindow
visible if it is not already visible?KeYEnvironment
which contains all references to the loaded location.ProblemLoaderException
- Occurred Exceptionpublic static KeYEnvironment<WindowUserInterfaceControl> loadInMainWindow(Profile profile, java.io.File location, java.util.List<java.io.File> classPaths, java.io.File bootClassPath, java.util.List<java.io.File> includes, boolean forceNewProfileOfNewProofs, boolean makeMainWindowVisible) throws ProblemLoaderException
KeYEnvironment
with KeY's MainWindow
.profile
- The Profile
to use.location
- The location to load.classPaths
- The class path entries to use.bootClassPath
- The boot class path to use.includes
- Optional includes to consider.makeMainWindowVisible
- Make KeY's MainWindow
visible if it is not already visible?forceNewProfileOfNewProofs
- true #profileOfNewProofs
will be used as Profile
of new proofs, false
Profile
specified by problem file will be used for new proofs.KeYEnvironment
which contains all references to the loaded location.ProblemLoaderException
- Occurred Exceptionpublic void notify(NotificationEvent event)
notify
in class AbstractMediatorUserInterfaceControl
public void reportWarnings(ImmutableSet<PositionedString> warnings)
ProblemLoaderControl
warnings
- The occurred warnings.public TermLabelVisibilityManager getTermLabelVisibilityManager()
TermLabelVisibilityManager
.TermLabelVisibilityManager
.