public class ScriptResult
extends java.lang.Object
Modifier and Type | Field and Description |
---|---|
private ProofScriptCommandCall<?> |
call
The scriptcommand that lead to this result
|
private java.util.Set<java.util.List<java.lang.String>> |
labels
The list of labels for the result
|
private java.util.List<PositionInfo> |
linenumbers
List with line numbers
|
private ProjectedNode |
newNode
The current goal node
|
private ProjectedNode |
parentNode
the parent scriptNode to which the scriptcommand was applied
|
Constructor and Description |
---|
ScriptResult() |
Modifier and Type | Method and Description |
---|---|
static <T> ScriptResult |
create(Node node,
ProjectedNode onNode,
ProofScriptCommandCall<T> call) |
ProofScriptCommandCall<?> |
getCall() |
java.util.Set<java.util.List<java.lang.String>> |
getLabels() |
java.util.List<PositionInfo> |
getLinenumbers() |
ProjectedNode |
getNewNode() |
ProjectedNode |
getParentNode() |
ProjectedNode |
getProjectedNode() |
ScriptResult |
setCall(ProofScriptCommandCall<?> call) |
ScriptResult |
setLabels(java.util.Set<java.util.List<java.lang.String>> labels) |
ScriptResult |
setLinenumbers(java.util.List<PositionInfo> linenumbers) |
ScriptResult |
setNewNode(ProjectedNode newNode) |
ScriptResult |
setParentNode(ProjectedNode parentNode) |
private ProjectedNode newNode
private ProjectedNode parentNode
private ProofScriptCommandCall<?> call
private java.util.Set<java.util.List<java.lang.String>> labels
private java.util.List<PositionInfo> linenumbers
public static <T> ScriptResult create(Node node, ProjectedNode onNode, ProofScriptCommandCall<T> call)
public ProjectedNode getNewNode()
public ScriptResult setNewNode(ProjectedNode newNode)
public ProjectedNode getParentNode()
public ScriptResult setParentNode(ProjectedNode parentNode)
public ProofScriptCommandCall<?> getCall()
public ScriptResult setCall(ProofScriptCommandCall<?> call)
public java.util.Set<java.util.List<java.lang.String>> getLabels()
public ScriptResult setLabels(java.util.Set<java.util.List<java.lang.String>> labels)
public java.util.List<PositionInfo> getLinenumbers()
public ScriptResult setLinenumbers(java.util.List<PositionInfo> linenumbers)
public ProjectedNode getProjectedNode()