public class RuleCommand extends AbstractCommand
Modifier and Type | Class and Description |
---|---|
private static class |
RuleCommand.Parameters |
private static class |
RuleCommand.TacletNameFilter |
ABBREV_KEY, GOAL_KEY
Constructor and Description |
---|
RuleCommand() |
Modifier and Type | Method and Description |
---|---|
void |
execute(AbstractUserInterfaceControl uiControl,
Proof proof,
Map<String,String> args,
Map<String,Object> state) |
private List<TacletApp> |
filterList(RuleCommand.Parameters p,
ImmutableList<TacletApp> list) |
private ImmutableList<TacletApp> |
findAllTacletApps(Proof proof,
RuleCommand.Parameters p,
Map<String,Object> state) |
private TacletApp |
findTacletApp(Proof proof,
RuleCommand.Parameters p,
Map<String,Object> state) |
String |
getName() |
private TacletApp |
makeNoFindTacletApp(Taclet taclet,
Proof proof,
RuleCommand.Parameters p,
Map<String,Object> state) |
private TacletApp |
makeTacletApp(Proof proof,
RuleCommand.Parameters p,
Map<String,Object> state) |
private static RuleCommand.Parameters |
parseArgs(Proof proof,
Map<String,String> args,
Map<String,Object> state) |
getFirstOpenGoal, getGoal, getMaxAutomaticSteps, setMaxAutomaticSteps, toSort, toTerm
public String getName()
public void execute(AbstractUserInterfaceControl uiControl, Proof proof, Map<String,String> args, Map<String,Object> state) throws ScriptException, InterruptedException
ScriptException
InterruptedException
private TacletApp makeTacletApp(Proof proof, RuleCommand.Parameters p, Map<String,Object> state) throws ScriptException
ScriptException
private TacletApp makeNoFindTacletApp(Taclet taclet, Proof proof, RuleCommand.Parameters p, Map<String,Object> state)
private TacletApp findTacletApp(Proof proof, RuleCommand.Parameters p, Map<String,Object> state) throws ScriptException
ScriptException
private ImmutableList<TacletApp> findAllTacletApps(Proof proof, RuleCommand.Parameters p, Map<String,Object> state) throws ScriptException
ScriptException
private List<TacletApp> filterList(RuleCommand.Parameters p, ImmutableList<TacletApp> list)
private static RuleCommand.Parameters parseArgs(Proof proof, Map<String,String> args, Map<String,Object> state) throws ScriptException
ScriptException