public class SelectCommand extends AbstractCommand<SelectCommand.Parameters>
Modifier and Type | Class and Description |
---|---|
class |
SelectCommand.Parameters |
documentation, log, proof, service, state, uiControl
Constructor and Description |
---|
SelectCommand() |
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.
|
execute, getArguments, getDocumentation
public SelectCommand.Parameters evaluateArguments(EngineState state, java.util.Map<java.lang.String,java.lang.String> arguments) throws java.lang.Exception
evaluateArguments
in interface ProofScriptCommand<SelectCommand.Parameters>
evaluateArguments
in class AbstractCommand<SelectCommand.Parameters>
java.lang.Exception
public void execute(SelectCommand.Parameters args) throws ScriptException, java.lang.InterruptedException
execute
in class AbstractCommand<SelectCommand.Parameters>
ScriptException
java.lang.InterruptedException
private Goal findGoalWith(java.lang.String branchTitle, Proof proof) throws ScriptException
ScriptException
private Goal findGoalWith(Term formula, Proof proof) throws ScriptException
ScriptException
private Goal findGoalWith(java.util.function.Function<Node,java.lang.Boolean> filter, java.util.function.Function<Node,Goal> goalRetriever, Proof proof) throws ScriptException
ScriptException
private boolean contains(Semisequent semiseq, Term formula)
public java.lang.String getName()
ProofScriptCommand
ProofScriptEngine