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