de.uka.ilkd.key.gui

Class WindowUserInterfaceControl

java.lang.Object

de.uka.ilkd.key.control.AbstractUserInterfaceControl

de.uka.ilkd.key.ui.AbstractMediatorUserInterfaceControl

de.uka.ilkd.key.gui.WindowUserInterfaceControl

All Implemented Interfaces:

RuleCompletionHandler, UserInterfaceControl, ProofDisposedListener, ProblemInitializer.ProblemInitializerListener, ProblemLoaderControl, ProofEnvironmentListener, ProverTaskListener, ProgressMonitor, java.util.EventListener

public class WindowUserInterfaceControl
extends AbstractMediatorUserInterfaceControl

Implementation of UserInterfaceControl which controls the MainWindow with the typical user interface of KeY.

Author:

Mattias Ulbrich

Nested Class Summary

Nested classes/interfaces inherited from interface de.uka.ilkd.key.util.ProgressMonitor

ProgressMonitor.Empty

Field Summary

Fields

Modifier and Type	Field and Description
private java.util.LinkedList<InteractiveRuleApplicationCompletion>	completions
private MainWindow	mainWindow

Fields inherited from class de.uka.ilkd.key.ui.AbstractMediatorUserInterfaceControl

saveOnly

Constructor Summary

Constructors

Constructor and Description
WindowUserInterfaceControl(MainWindow mainWindow)

Method Summary

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)

Methods inherited from class de.uka.ilkd.key.ui.AbstractMediatorUserInterfaceControl

applyMacro, createProofEnvironmentAndRegisterProof, getMacro, getProblemLoader, getProofControl, isSaveOnly, macroChosen, macroFinished, macroSideProofDisposing, proofDisposed, proofRegistered, proofUnregistered, setMacro, setSaveOnly

Methods inherited from class de.uka.ilkd.key.control.AbstractUserInterfaceControl

addProverTaskListener, createProblemInitializer, createProof, fireTaskFinished, fireTaskProgress, fireTaskStarted, isAtLeastOneMacroRunning, macroStarted, proofCreated, removeProverTaskListener

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Field Detail

mainWindow

private final MainWindow mainWindow

completions

private final java.util.LinkedList<InteractiveRuleApplicationCompletion> completions

Constructor Detail

WindowUserInterfaceControl

public WindowUserInterfaceControl(MainWindow mainWindow)

Method Detail

createProofControl

protected MediatorProofControl createProofControl()

Overrides:

createProofControl in class AbstractMediatorUserInterfaceControl

loadProblem

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)

loads the problem or proof from the given file

Parameters:

file - the File with the problem description or the proof

classPath - the class path entries to use.

bootClassPath - the boot class path to use.

loadProblem

public void loadProblem(java.io.File file)

Description copied from class: AbstractMediatorUserInterfaceControl

loads the problem or proof from the given file

Specified by:

loadProblem in class AbstractMediatorUserInterfaceControl

Parameters:

file - the File with the problem description or the proof

progressStarted

public void progressStarted(java.lang.Object sender)

progressStopped

public void progressStopped(java.lang.Object sender)

reportException

public void reportException(java.lang.Object sender,
                            ProofOblInput input,
                            java.lang.Exception e)

reportStatus

public void reportStatus(java.lang.Object sender,
                         java.lang.String status,
                         int progress)

reportStatus

public void reportStatus(java.lang.Object sender,
                         java.lang.String status)

resetStatus

public void resetStatus(java.lang.Object sender)

taskFinished

public void taskFinished(TaskFinishedInfo info)

Description copied from interface: ProverTaskListener

Called when a task is finished.

Specified by:

taskFinished in interface ProverTaskListener

Overrides:

taskFinished in class AbstractUserInterfaceControl

Parameters:

info - a TaskFinishedInfo object with additional information

inStopAtFirstUncloseableGoalMode

protected boolean inStopAtFirstUncloseableGoalMode(Proof proof)

taskProgress

public void taskProgress(int position)

Description copied from interface: ProverTaskListener

Called when progress is made on a task. This method is called after every single step of the task

Specified by:

taskProgress in interface ProverTaskListener

Overrides:

taskProgress in class AbstractUserInterfaceControl

Parameters:

position - indicates how much work has been done relative to the value of size passed in ProverTaskListener.taskStarted(TaskStartedInfo).

taskStarted

public void taskStarted(TaskStartedInfo info)

Specified by:

taskStarted in interface ProverTaskListener

Overrides:

taskStarted in class AbstractUserInterfaceControl

setMaximum

public void setMaximum(int maximum)

Description copied from interface: ProgressMonitor

Set the maximum number of steps for this task.

Parameters:

maximum - maximum number of steps, >=0.

setProgress

public void setProgress(int progress)

Description copied from interface: ProgressMonitor

Set the progress achieved so far. The parameter progress has to be >=0 and <= to the maximum value previously set with ProgressMonitor.setMaximum(int).

Parameters:

progress - number of steps completed

notifyAutoModeBeingStarted

public void notifyAutoModeBeingStarted()

Description copied from class: AbstractMediatorUserInterfaceControl

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

Overrides:

notifyAutoModeBeingStarted in class AbstractMediatorUserInterfaceControl

notifyAutomodeStopped

public void notifyAutomodeStopped()

Description copied from class: AbstractMediatorUserInterfaceControl

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

Overrides:

notifyAutomodeStopped in class AbstractMediatorUserInterfaceControl

completeAndApplyTacletMatch

public void completeAndApplyTacletMatch(TacletInstantiationModel[] models,
                                        Goal goal)

Description copied from interface: RuleCompletionHandler

called to complete and apply a taclet instantiations

Parameters:

models - the partial models with all different possible instantiations found automatically

goal - the Goal where to apply

confirmTaskRemoval

public boolean confirmTaskRemoval(java.lang.String string)

Description copied from class: AbstractMediatorUserInterfaceControl

asks if removal of a task is completed. This is useful to display a dialog to the user and asking her or if on command line to allow it always.

Overrides:

confirmTaskRemoval in class AbstractMediatorUserInterfaceControl

Returns:

true if removal has been granted

openExamples

public void openExamples()

Description copied from class: AbstractMediatorUserInterfaceControl

called to open the build in examples

Specified by:

openExamples in class AbstractMediatorUserInterfaceControl

completeBuiltInRuleApp

public IBuiltInRuleApp completeBuiltInRuleApp(IBuiltInRuleApp app,
                                              Goal goal,
                                              boolean forced)

Description copied from interface: RuleCompletionHandler

completes rule applications of built in rules

Parameters:

app - the DefaultBuiltInRuleApp to be completed

goal - the Goal where the app will later be applied to

forced - 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 automatically

Returns:

a complete app or null if no completion was possible

getMediator

public KeYMediator getMediator()

Returns the used KeYMediator.

Specified by:

getMediator in class AbstractMediatorUserInterfaceControl

Returns:

The used KeYMediator.

load

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!

Specified by:

load in interface UserInterfaceControl

Overrides:

load in class AbstractUserInterfaceControl

Parameters:

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.

Returns:

The opened AbstractProblemLoader.

Throws:

ProblemLoaderException - Occurred Exception.

saveProof

public java.io.File saveProof(Proof proof,
                              java.lang.String fileExtension)

save proof in file. If autoSave is on, this will potentially overwrite already existing proof files with the same name. Otherwise the save dialog pops up. For loaded proofs both are turned off by default, i.e. only manual saving is possible, and the save dialog never pops up automatically (except for hitting the "Save ..." or "Save current proof" button).

fileName

protected static Pair<java.io.File,java.lang.String> fileName(Proof proof,
                                                              java.lang.String fileExtension)

proofDisposing

public void proofDisposing(ProofDisposedEvent e)

When a Proof is going to be disposed.

Specified by:

proofDisposing in interface ProofDisposedListener

Overrides:

proofDisposing in class AbstractMediatorUserInterfaceControl

Parameters:

e - The event.

selectProofObligation

public boolean selectProofObligation(InitConfig initConfig)

Description copied from interface: ProblemLoaderControl

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.

Returns:

true if the proof obligation was selected, and false if action was aborted

registerProofAggregate

public void registerProofAggregate(ProofAggregate pa)

Description copied from class: AbstractMediatorUserInterfaceControl

Registers an already created ProofAggregate in this UserInterfaceControl.

Specified by:

registerProofAggregate in interface UserInterfaceControl

Overrides:

registerProofAggregate in class AbstractMediatorUserInterfaceControl

Parameters:

pa - The ProofAggregate to register.

loadingStarted

public void loadingStarted(AbstractProblemLoader loader)

Description copied from interface: ProblemLoaderControl

The loading has started.

Specified by:

loadingStarted in interface ProblemLoaderControl

Overrides:

loadingStarted in class AbstractUserInterfaceControl

Parameters:

loader - The source AbstractProblemLoader.

loadingFinished

public void loadingFinished(AbstractProblemLoader loader,
                            IPersistablePO.LoadedPOContainer poContainer,
                            ProofAggregate proofList,
                            AbstractProblemLoader.ReplayResult result)
                     throws ProblemLoaderException

Description copied from interface: ProblemLoaderControl

The loading has stopped.

Specified by:

loadingFinished in interface ProblemLoaderControl

Overrides:

loadingFinished in class AbstractUserInterfaceControl

Parameters:

loader - The source AbstractProblemLoader.

poContainer - The loaded IPersistablePO.LoadedPOContainer.

proofList - The created ProofAggregate.

result - The occurred AbstractProblemLoader.ReplayResult.

Throws:

ProblemLoaderException - Occurred Exception.

loadInMainWindow

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

Loads the given location and returns all required references as KeYEnvironment with KeY's MainWindow.

Parameters:

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?

Returns:

The KeYEnvironment which contains all references to the loaded location.

Throws:

ProblemLoaderException - Occurred Exception

loadInMainWindow

public 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

Loads the given location and returns all required references as KeYEnvironment with KeY's MainWindow.

Parameters:

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.

Returns:

The KeYEnvironment which contains all references to the loaded location.

Throws:

ProblemLoaderException - Occurred Exception

notify

public void notify(NotificationEvent event)

Specified by:

notify in class AbstractMediatorUserInterfaceControl

reportWarnings

public void reportWarnings(ImmutableSet<PositionedString> warnings)

Description copied from interface: ProblemLoaderControl

Report the occurred warnings.

Parameters:

warnings - The occurred warnings.

getTermLabelVisibilityManager

public TermLabelVisibilityManager getTermLabelVisibilityManager()

Returns the TermLabelVisibilityManager.

Returns:

The TermLabelVisibilityManager.