public interface UserInterfaceControl
#load(Profile, File, List, File, List, Properties,
boolean)
.Proof
s via createProof(InitConfig, ProofOblInput)
.Proof
s in the user interface via registerProofAggregate(ProofAggregate)
.ProofControl
via getProofControl()
.Modifier and Type | Method and Description |
---|---|
void |
addProverTaskListener(ProverTaskListener ptl)
Registers the given
ProverTaskListener which will be informed about all events. |
Proof |
createProof(InitConfig initConfig,
ProofOblInput input)
Instantiates a new
Proof in this UserInterfaceControl for the given
ProofOblInput based on the InitConfig . |
ProofControl |
getProofControl()
Returns the used
ProofControl . |
TermLabelVisibilityManager |
getTermLabelVisibilityManager()
Returns the
TermLabelVisibilityManager . |
AbstractProblemLoader |
load(Profile profile,
java.io.File file,
java.util.List<java.io.File> classPaths,
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 |
registerProofAggregate(ProofAggregate pa)
Registers an already created
ProofAggregate in this UserInterfaceControl . |
void |
removeProverTaskListener(ProverTaskListener ptl)
Removes the given
ProverTaskListener . |
void addProverTaskListener(ProverTaskListener ptl)
ProverTaskListener
which will be informed about all events.ptl
- The ProverTaskListener
to add.void removeProverTaskListener(ProverTaskListener ptl)
ProverTaskListener
.ptl
- The ProverTaskListener
to remove.AbstractProblemLoader load(Profile profile, java.io.File file, java.util.List<java.io.File> classPaths, 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!
profile
- An optional Profile
to use. If it is null
the default profile AbstractProfile.getDefaultProfile()
is used.file
- The java file to open.classPaths
- 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.Proof createProof(InitConfig initConfig, ProofOblInput input) throws ProofInputException
Proof
in this UserInterfaceControl
for the given
ProofOblInput
based on the InitConfig
.initConfig
- The InitConfig
which provides the source code.input
- The description of the Proof
to instantiate.Proof
.ProofInputException
- Occurred Exception.void registerProofAggregate(ProofAggregate pa)
ProofAggregate
in this UserInterfaceControl
.pa
- The ProofAggregate
to register.ProofControl getProofControl()
ProofControl
.ProofControl
.TermLabelVisibilityManager getTermLabelVisibilityManager()
TermLabelVisibilityManager
.TermLabelVisibilityManager
.