de.uka.ilkd.key.macros.scripts

Interface ProofScriptCommand<T>

Type Parameters:

T - the arguments

All Known Implementing Classes:

AbstractCommand, ActivateCommand, AssumeCommand, AutoCommand, CutCommand, EchoCommand, ExitCommand, FocusOnSelectionAndHideCommand, InstantiateCommand, JavascriptCommand, LeaveCommand, LetCommand, MacroCommand, NoArgumentCommand, RewriteCommand, RuleCommand, SaveInstCommand, SaveNewNameCommand, SchemaVarCommand, ScriptCommand, SelectCommand, SetCommand, SetEchoCommand, SettingsCommand, SkipCommand, SMTCommand, TryCloseCommand

public interface ProofScriptCommand<T>

A 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.

Author:

Mattias Ulbrich, Alexander Weigl

Method Summary

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.

Method Detail

getArguments

java.util.List<ProofScriptArgument> getArguments()

evaluateArguments

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

Parameters:

arguments -

Returns:

Throws:

java.lang.Exception

execute

void execute(AbstractUserInterfaceControl uiControl,
             T args,
             EngineState stateMap)
      throws ScriptException,
             java.lang.InterruptedException

Parameters:

uiControl - the current ui controller

args - the script arguments

stateMap - the current state

Throws:

ScriptException - if something bad happens

java.lang.InterruptedException - if something bad happens

getName

java.lang.String getName()

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

getDocumentation

java.lang.String getDocumentation()

A documentation for the commands.

Returns:

a non-null string