de.uka.ilkd.key.proof.io

Class ProblemLoader

java.lang.Object

de.uka.ilkd.key.proof.io.AbstractProblemLoader

de.uka.ilkd.key.proof.io.ProblemLoader

public final class ProblemLoader
extends AbstractProblemLoader

This class extends the functionality of the AbstractProblemLoader. It allows to do the loading process as SwingWorker3 Thread and it opens the proof obligation browser it is not possible to instantiate a proof configured by the opened file.

Author:

Martin Hentschel

Nested Class Summary

Nested classes/interfaces inherited from class de.uka.ilkd.key.proof.io.AbstractProblemLoader

AbstractProblemLoader.ReplayResult

Field Summary

Fields

Modifier and Type	Field and Description
private KeYMediator	mediator
private ProverTaskListener	ptl

Constructor Summary

Constructors

Constructor and Description
ProblemLoader(java.io.File file, java.util.List<java.io.File> classPath, java.io.File bootClassPath, java.util.List<java.io.File> includes, Profile profileOfNewProofs, boolean forceNewProfileOfNewProofs, KeYMediator mediator, boolean askUiToSelectAProofObligationIfNotDefinedByLoadedFile, java.util.Properties poPropertiesToForce, ProverTaskListener ptl)

Method Summary

Modifier and Type	Method and Description
private java.lang.Throwable	doWork()
private void	fireTaskFinished(long runningTime, java.lang.Throwable message)
private void	fireTaskStarted()
void	runAsynchronously() Launch a loading process asynchronously (on a swingworker thread).
void	runSynchronously()

Methods inherited from class de.uka.ilkd.key.proof.io.AbstractProblemLoader

createEnvInput, createInitConfig, createProblemInitializer, createProof, createProofObligationContainer, getBootClassPath, getClassPath, getEnvInput, getFile, getInitConfig, getProblemInitializer, getProof, getProofScript, getResult, hasProofScript, load, readProofScript, recoverParserErrorMessage

Methods inherited from class java.lang.Object

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

Field Detail

ptl

private final ProverTaskListener ptl

mediator

private final KeYMediator mediator

Constructor Detail

ProblemLoader

public ProblemLoader(java.io.File file,
                     java.util.List<java.io.File> classPath,
                     java.io.File bootClassPath,
                     java.util.List<java.io.File> includes,
                     Profile profileOfNewProofs,
                     boolean forceNewProfileOfNewProofs,
                     KeYMediator mediator,
                     boolean askUiToSelectAProofObligationIfNotDefinedByLoadedFile,
                     java.util.Properties poPropertiesToForce,
                     ProverTaskListener ptl)

Method Detail

runSynchronously

public void runSynchronously()

doWork

private java.lang.Throwable doWork()

fireTaskStarted

private void fireTaskStarted()

fireTaskFinished

private void fireTaskFinished(long runningTime,
                              java.lang.Throwable message)

runAsynchronously

public void runAsynchronously()

Launch a loading process asynchronously (on a swingworker thread). The start is announced by invoking ProverTaskListener#taskStarted(String, int) on the registered listener. Termination is announced by invoking ProverTaskListener.taskFinished(TaskFinishedInfo) on the registered listener.