public class ProofEvent
extends java.lang.Object
Modifier and Type | Field and Description |
---|---|
private ImmutableList<Goal> |
newGoals
new goals created by an applied rule; empty if goal was closed and null if this event
does not relate to a rule application
|
private RuleAppInfo |
ruleAppInfo
if the proof event is the result of rule applications the following to fields
have a non-null value, otherwise null
|
private Proof |
source
the proof where an event happened
|
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
|
private final Proof source
private RuleAppInfo ruleAppInfo
private ImmutableList<Goal> newGoals
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()