T
- the argumentspublic interface ProofScriptCommand<T>
ProofScriptCommand
is an executable mutation on the given proof.
It abstracts complex operations, and made them accessible for an API.
ProofScriptCommand
are supported by the java.util.ServiceLoader
.
You can add new proof script commands by add a new entry to META-INF/service/de.uka.ilkd.key.macros.scripts.ProofScriptCommand
.
Version 2 (2017-03-28): change of the interface support for structured arguments.
Modifier and Type | Method and Description |
---|---|
T |
evaluateArguments(EngineState state,
java.util.Map<java.lang.String,java.lang.String> arguments) |
void |
execute(AbstractUserInterfaceControl uiControl,
T args,
EngineState stateMap) |
java.util.List<ProofScriptArgument> |
getArguments() |
java.lang.String |
getDocumentation()
A documentation for the commands.
|
java.lang.String |
getName()
Returns the name of this proof command.
|
java.util.List<ProofScriptArgument> getArguments()
T evaluateArguments(EngineState state, java.util.Map<java.lang.String,java.lang.String> arguments) throws java.lang.Exception
arguments
- java.lang.Exception
void execute(AbstractUserInterfaceControl uiControl, T args, EngineState stateMap) throws ScriptException, java.lang.InterruptedException
uiControl
- the current ui controllerargs
- the script argumentsstateMap
- the current stateScriptException
- if something bad happensjava.lang.InterruptedException
- if something bad happensjava.lang.String getName()
ProofScriptEngine
java.lang.String getDocumentation()