de.uka.ilkd.key.macros.scripts

Class SelectCommand

java.lang.Object

de.uka.ilkd.key.macros.scripts.AbstractCommand<SelectCommand.Parameters>

de.uka.ilkd.key.macros.scripts.SelectCommand

All Implemented Interfaces:

ProofScriptCommand<SelectCommand.Parameters>

public class SelectCommand
extends AbstractCommand<SelectCommand.Parameters>

Nested Class Summary

Nested Classes

Modifier and Type	Class and Description
class	SelectCommand.Parameters

Field Summary

Fields inherited from class de.uka.ilkd.key.macros.scripts.AbstractCommand

documentation, log, proof, service, state, uiControl

Constructor Summary

Constructors

Constructor and Description
SelectCommand()

Method Summary

Modifier and Type	Method and Description
private boolean	contains(Semisequent semiseq, Term formula)
private boolean	contains(Sequent seq, Term formula)
SelectCommand.Parameters	evaluateArguments(EngineState state, java.util.Map<java.lang.String,java.lang.String> arguments)
void	execute(SelectCommand.Parameters args)
private Goal	findGoalWith(java.util.function.Function<Node,java.lang.Boolean> filter, java.util.function.Function<Node,Goal> goalRetriever, Proof proof)
private Goal	findGoalWith(java.lang.String branchTitle, Proof proof)
private Goal	findGoalWith(Term formula, Proof proof)
private static Goal	getFirstSubtreeGoal(Node node, Proof proof)
java.lang.String	getName() Returns the name of this proof command.

Methods inherited from class de.uka.ilkd.key.macros.scripts.AbstractCommand

execute, getArguments, getDocumentation

Methods inherited from class java.lang.Object

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

Constructor Detail

SelectCommand

public SelectCommand()

Method Detail

evaluateArguments

public SelectCommand.Parameters evaluateArguments(EngineState state,
                                                  java.util.Map<java.lang.String,java.lang.String> arguments)
                                           throws java.lang.Exception

Specified by:

evaluateArguments in interface ProofScriptCommand<SelectCommand.Parameters>

Overrides:

evaluateArguments in class AbstractCommand<SelectCommand.Parameters>

Returns:

Throws:

java.lang.Exception

execute

public void execute(SelectCommand.Parameters args)
             throws ScriptException,
                    java.lang.InterruptedException

Overrides:

execute in class AbstractCommand<SelectCommand.Parameters>

Throws:

ScriptException

java.lang.InterruptedException

findGoalWith

private Goal findGoalWith(java.lang.String branchTitle,
                          Proof proof)
                   throws ScriptException

Throws:

ScriptException

getFirstSubtreeGoal

private static Goal getFirstSubtreeGoal(Node node,
                                        Proof proof)

findGoalWith

private Goal findGoalWith(Term formula,
                          Proof proof)
                   throws ScriptException

Throws:

ScriptException

findGoalWith

private Goal findGoalWith(java.util.function.Function<Node,java.lang.Boolean> filter,
                          java.util.function.Function<Node,Goal> goalRetriever,
                          Proof proof)
                   throws ScriptException

Throws:

ScriptException

contains

private boolean contains(Sequent seq,
                         Term formula)

contains

private boolean contains(Semisequent semiseq,
                         Term formula)

getName

public java.lang.String getName()

Description copied from interface: ProofScriptCommand

Returns the name of this proof command. The name should be constant and not be clash with the name of other commands. The name is essential for finding this command within an hashmap.

Returns:

a non-null, non-empty string

See Also:

ProofScriptEngine