de.uka.ilkd.key.api

Class ScriptResult

java.lang.Object

de.uka.ilkd.key.api.ScriptResult

public class ScriptResult
extends java.lang.Object

Object that represents one result goal of a script command It holds a reference to its parent node and to the list of variables and their values for this result Created by S. Grebing

Field Summary

Fields

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 Summary

Constructors

Constructor and Description
ScriptResult()

Method Summary

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)

Methods inherited from class java.lang.Object

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

Field Detail

newNode

private ProjectedNode newNode

The current goal node

parentNode

private ProjectedNode parentNode

the parent scriptNode to which the scriptcommand was applied

call

private ProofScriptCommandCall<?> call

The scriptcommand that lead to this result

labels

private java.util.Set<java.util.List<java.lang.String>> labels

The list of labels for the result

linenumbers

private java.util.List<PositionInfo> linenumbers

List with line numbers

Constructor Detail

ScriptResult

ScriptResult()

Method Detail

create

public static <T> ScriptResult create(Node node,
                                      ProjectedNode onNode,
                                      ProofScriptCommandCall<T> call)

getNewNode

public ProjectedNode getNewNode()

setNewNode

public ScriptResult setNewNode(ProjectedNode newNode)

getParentNode

public ProjectedNode getParentNode()

setParentNode

public ScriptResult setParentNode(ProjectedNode parentNode)

getCall

public ProofScriptCommandCall<?> getCall()

setCall

public ScriptResult setCall(ProofScriptCommandCall<?> call)

getLabels

public java.util.Set<java.util.List<java.lang.String>> getLabels()

setLabels

public ScriptResult setLabels(java.util.Set<java.util.List<java.lang.String>> labels)

getLinenumbers

public java.util.List<PositionInfo> getLinenumbers()

setLinenumbers

public ScriptResult setLinenumbers(java.util.List<PositionInfo> linenumbers)

getProjectedNode

public ProjectedNode getProjectedNode()