public class ProofEvent
extends java.lang.Object
Constructor and Description |
---|
ProofEvent(Proof source)
creates a new proof event the interactive prover where the event initially
occured
|
ProofEvent(Proof source,
RuleAppInfo rai,
ImmutableList<Goal> newGoals)
creates a proof event for a change triggered by a rule applications
|
Modifier and Type | Method and Description |
---|---|
ImmutableList<Goal> |
getNewGoals()
returns the list of new goals (empty if a goal was closed) in case of a rule
application otherwise null
|
RuleAppInfo |
getRuleAppInfo()
This information should have its own event, but is currently propagated via
this one
|
Proof |
getSource()
the proof from where this even to originated
|
public ProofEvent(Proof source)
source
- the source eventpublic ProofEvent(Proof source, RuleAppInfo rai, ImmutableList<Goal> newGoals)
source
- the Proof where the rule was appliedrai
- the RuleAppInfo object with further information about the changesnewGoals
- the list of newly created goals (empty in case a goal was closed)public Proof getSource()
public RuleAppInfo getRuleAppInfo()
public ImmutableList<Goal> getNewGoals()
Copyright © 2003-2019 The KeY-Project.