de.uka.ilkd.key.ui

Class ConsoleUserInterfaceControl

java.lang.Object

de.uka.ilkd.key.control.AbstractUserInterfaceControl

de.uka.ilkd.key.ui.AbstractMediatorUserInterfaceControl

de.uka.ilkd.key.ui.ConsoleUserInterfaceControl

All Implemented Interfaces:

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

public class ConsoleUserInterfaceControl
extends AbstractMediatorUserInterfaceControl

Implementation of UserInterfaceControl used by command line interface of KeY.

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
boolean	allProofsSuccessful We want to record whether there was a proof that could not be proven.
private java.io.File	keyProblemFile Current key problem file that is attempted to be proven.
private boolean	loadOnly
(package private) KeYMediator	mediator
private static int	PROGRESS_BAR_STEPS
private static java.lang.String	PROGRESS_MARK
(package private) int	progressMax
(package private) ImmutableList<Proof>	proofStack
(package private) byte	verbosity

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

saveOnly

Constructor Summary

Constructors

Constructor and Description
ConsoleUserInterfaceControl(boolean verbose, boolean loadOnly)
ConsoleUserInterfaceControl(byte verbosity, boolean loadOnly)

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
ProblemInitializer	createProblemInitializer(Profile profile) Creates a new ProblemInitializer instance which is configured for this UserInterfaceControl.
(package private) void	finish(Proof proof)
KeYMediator	getMediator() Returns the used KeYMediator.
TermLabelVisibilityManager	getTermLabelVisibilityManager() Returns the TermLabelVisibilityManager.
void	loadProblem(java.io.File file) loads the problem or proof from the given file
void	notify(NotificationEvent event)
void	openExamples() called to open the build in examples
private void	printResults(int openGoals, TaskFinishedInfo info, java.lang.Object result2)
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)
static boolean	saveProof(java.lang.Object result, Proof proof, java.io.File keyProblemFile)
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, confirmTaskRemoval, createProofControl, createProofEnvironmentAndRegisterProof, getMacro, getProblemLoader, getProofControl, isSaveOnly, macroChosen, macroFinished, macroSideProofDisposing, notifyAutoModeBeingStarted, notifyAutomodeStopped, proofDisposed, proofRegistered, proofUnregistered, setMacro, setSaveOnly

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

addProverTaskListener, createProof, fireTaskFinished, fireTaskProgress, fireTaskStarted, isAtLeastOneMacroRunning, load, loadingFinished, loadingStarted, macroStarted, proofCreated, removeProverTaskListener

Methods inherited from class java.lang.Object

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

Field Detail

PROGRESS_BAR_STEPS

private static final int PROGRESS_BAR_STEPS

See Also:

Constant Field Values

PROGRESS_MARK

private static final java.lang.String PROGRESS_MARK

See Also:

Constant Field Values

proofStack

ImmutableList<Proof> proofStack

verbosity

final byte verbosity

mediator

final KeYMediator mediator

progressMax

int progressMax

loadOnly

private final boolean loadOnly

keyProblemFile

private java.io.File keyProblemFile

Current key problem file that is attempted to be proven.

allProofsSuccessful

public boolean allProofsSuccessful

We want to record whether there was a proof that could not be proven. Main calls System.exit() after all files have been loaded with loadProblem(java.io.File). Program return value depends on whether there has been a proof attempt that was not successful.

Constructor Detail

ConsoleUserInterfaceControl

public ConsoleUserInterfaceControl(byte verbosity,
                                   boolean loadOnly)

ConsoleUserInterfaceControl

public ConsoleUserInterfaceControl(boolean verbose,
                                   boolean loadOnly)

Method Detail

printResults

private void printResults(int openGoals,
                          TaskFinishedInfo info,
                          java.lang.Object result2)

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

taskStarted

public void taskStarted(TaskStartedInfo info)

Specified by:

taskStarted in interface ProverTaskListener

Overrides:

taskStarted in class AbstractUserInterfaceControl

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

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.

finish

void finish(Proof proof)

progressStarted

public final void progressStarted(java.lang.Object sender)

progressStopped

public final void progressStopped(java.lang.Object sender)

reportException

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

reportStatus

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

reportStatus

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

resetStatus

public final void resetStatus(java.lang.Object sender)

taskProgress

public final 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).

setMaximum

public final 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 final 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

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

openExamples

public final void openExamples()

Description copied from class: AbstractMediatorUserInterfaceControl

called to open the build in examples

Specified by:

openExamples in class AbstractMediatorUserInterfaceControl

createProblemInitializer

public final ProblemInitializer createProblemInitializer(Profile profile)

Description copied from class: AbstractUserInterfaceControl

Creates a new ProblemInitializer instance which is configured for this UserInterfaceControl.

This method is used by nearly all Eclipse based product that uses KeY.

Overrides:

createProblemInitializer in class AbstractUserInterfaceControl

Parameters:

profile - The Profile to use.

Returns:

The instantiated ProblemInitializer.

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 final 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

getMediator

public KeYMediator getMediator()

Returns the used KeYMediator.

Specified by:

getMediator in class AbstractMediatorUserInterfaceControl

Returns:

The used KeYMediator.

notify

public void notify(NotificationEvent event)

Specified by:

notify 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

reportWarnings

public void reportWarnings(ImmutableSet<PositionedString> warnings)

Report the occurred warnings.

Parameters:

warnings - The occurred warnings.

saveProof

public static boolean saveProof(java.lang.Object result,
                                Proof proof,
                                java.io.File keyProblemFile)

getTermLabelVisibilityManager

public TermLabelVisibilityManager getTermLabelVisibilityManager()

Description copied from interface: UserInterfaceControl

Returns the TermLabelVisibilityManager.

Returns:

The TermLabelVisibilityManager.