public class ConsoleUserInterfaceControl extends AbstractMediatorUserInterfaceControl
UserInterfaceControl
used by command line interface of KeY.ProgressMonitor.Empty
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 |
saveOnly
Constructor and Description |
---|
ConsoleUserInterfaceControl(boolean verbose,
boolean loadOnly) |
ConsoleUserInterfaceControl(byte verbosity,
boolean loadOnly) |
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) |
applyMacro, confirmTaskRemoval, createProofControl, createProofEnvironmentAndRegisterProof, getMacro, getProblemLoader, getProofControl, isSaveOnly, macroChosen, macroFinished, macroSideProofDisposing, notifyAutoModeBeingStarted, notifyAutomodeStopped, proofDisposed, proofRegistered, proofUnregistered, setMacro, setSaveOnly
addProverTaskListener, createProof, fireTaskFinished, fireTaskProgress, fireTaskStarted, isAtLeastOneMacroRunning, load, loadingFinished, loadingStarted, macroStarted, proofCreated, removeProverTaskListener
private static final int PROGRESS_BAR_STEPS
private static final java.lang.String PROGRESS_MARK
ImmutableList<Proof> proofStack
final byte verbosity
final KeYMediator mediator
int progressMax
private final boolean loadOnly
private java.io.File keyProblemFile
public boolean allProofsSuccessful
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.public ConsoleUserInterfaceControl(byte verbosity, boolean loadOnly)
public ConsoleUserInterfaceControl(boolean verbose, boolean loadOnly)
private void printResults(int openGoals, TaskFinishedInfo info, java.lang.Object result2)
public void taskFinished(TaskFinishedInfo info)
ProverTaskListener
taskFinished
in interface ProverTaskListener
taskFinished
in class AbstractUserInterfaceControl
info
- a TaskFinishedInfo object with additional informationpublic void taskStarted(TaskStartedInfo info)
taskStarted
in interface ProverTaskListener
taskStarted
in class AbstractUserInterfaceControl
public void loadProblem(java.io.File file)
AbstractMediatorUserInterfaceControl
loadProblem
in class AbstractMediatorUserInterfaceControl
file
- the File with the problem description or the proofpublic void registerProofAggregate(ProofAggregate pa)
AbstractMediatorUserInterfaceControl
ProofAggregate
in this UserInterfaceControl
.registerProofAggregate
in interface UserInterfaceControl
registerProofAggregate
in class AbstractMediatorUserInterfaceControl
pa
- The ProofAggregate
to register.void finish(Proof proof)
public final void progressStarted(java.lang.Object sender)
public final void progressStopped(java.lang.Object sender)
public final void reportException(java.lang.Object sender, ProofOblInput input, java.lang.Exception e)
public final void reportStatus(java.lang.Object sender, java.lang.String status, int progress)
public final void reportStatus(java.lang.Object sender, java.lang.String status)
public final void resetStatus(java.lang.Object sender)
public final 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 final void setMaximum(int maximum)
ProgressMonitor
maximum
- maximum number of steps, >=0.public final 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 completeAndApplyTacletMatch(TacletInstantiationModel[] models, Goal goal)
RuleCompletionHandler
models
- the partial models with all different possible instantiations found automaticallygoal
- the Goal where to applypublic final void openExamples()
AbstractMediatorUserInterfaceControl
openExamples
in class AbstractMediatorUserInterfaceControl
public final ProblemInitializer createProblemInitializer(Profile profile)
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.
createProblemInitializer
in class AbstractUserInterfaceControl
profile
- The Profile
to use.ProblemInitializer
.public void proofDisposing(ProofDisposedEvent e)
Proof
is going to be disposed.proofDisposing
in interface ProofDisposedListener
proofDisposing
in class AbstractMediatorUserInterfaceControl
e
- The event.public final 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 KeYMediator getMediator()
KeYMediator
.getMediator
in class AbstractMediatorUserInterfaceControl
KeYMediator
.public void notify(NotificationEvent event)
notify
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 void reportWarnings(ImmutableSet<PositionedString> warnings)
warnings
- The occurred warnings.public static boolean saveProof(java.lang.Object result, Proof proof, java.io.File keyProblemFile)
public TermLabelVisibilityManager getTermLabelVisibilityManager()
UserInterfaceControl
TermLabelVisibilityManager
.TermLabelVisibilityManager
.