public class PruneInteraction extends NodeInteraction
Interaction.InteractionGraphicStyle
graphicalStyle
Constructor and Description |
---|
PruneInteraction() |
PruneInteraction(Node node) |
Modifier and Type | Method and Description |
---|---|
java.lang.String |
getMarkdown() |
java.lang.String |
getProofScriptRepresentation() |
void |
reapply(WindowUserInterfaceControl uic,
Goal goal) |
java.lang.String |
toString() |
getNode, getNodeId, getSerialNr, setNodeId
getCreated, getGraphicalStyle, isFavoured, setCreated, setFavoured
public PruneInteraction()
public PruneInteraction(Node node)
public java.lang.String toString()
toString
in class java.lang.Object
public java.lang.String getMarkdown()
public java.lang.String getProofScriptRepresentation()
public void reapply(WindowUserInterfaceControl uic, Goal goal) throws java.lang.Exception
java.lang.Exception
Copyright © 2003-2019 The KeY-Project.