de.uka.ilkd.key.macros.scripts

Class SaveInstCommand

java.lang.Object

de.uka.ilkd.key.macros.scripts.AbstractCommand<java.util.Map<java.lang.String,java.lang.String>>

de.uka.ilkd.key.macros.scripts.SaveInstCommand

All Implemented Interfaces:

ProofScriptCommand<java.util.Map<java.lang.String,java.lang.String>>

public class SaveInstCommand
extends AbstractCommand<java.util.Map<java.lang.String,java.lang.String>>

Special "Let" usually to be applied immediately after a manual rule application. Saves the instantiation of a SchemaVariable by the last TacletApp into an abbreviation for later use. A nice use case is a manual loop invariant rule application, where the newly introduced anonymizing Skolem constants can be saved for later interactive instantiations. As for the LetCommand, it is not allowed to call this command multiple times with the same name argument (all names used for remembering instantiations are "final").

Author:

Dominic Steinhoefel

Field Summary

Fields inherited from class de.uka.ilkd.key.macros.scripts.AbstractCommand

documentation, log, proof, service, state, uiControl

Constructor Summary

Constructors

Constructor and Description
SaveInstCommand()

Method Summary

Modifier and Type	Method and Description
java.util.Map<java.lang.String,java.lang.String>	evaluateArguments(EngineState state, java.util.Map<java.lang.String,java.lang.String> arguments)
void	execute(AbstractUserInterfaceControl uiControl, java.util.Map<java.lang.String,java.lang.String> args, EngineState stateMap)
java.lang.String	getName() Returns the name of this proof command.

Methods inherited from class de.uka.ilkd.key.macros.scripts.AbstractCommand

execute, getArguments, getDocumentation

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Constructor Detail

SaveInstCommand

public SaveInstCommand()

Method Detail

evaluateArguments

public java.util.Map<java.lang.String,java.lang.String> evaluateArguments(EngineState state,
                                                                          java.util.Map<java.lang.String,java.lang.String> arguments)

Specified by:

evaluateArguments in interface ProofScriptCommand<java.util.Map<java.lang.String,java.lang.String>>

Overrides:

evaluateArguments in class AbstractCommand<java.util.Map<java.lang.String,java.lang.String>>

Returns:

execute

public void execute(AbstractUserInterfaceControl uiControl,
                    java.util.Map<java.lang.String,java.lang.String> args,
                    EngineState stateMap)
             throws ScriptException,
                    java.lang.InterruptedException

Specified by:

execute in interface ProofScriptCommand<java.util.Map<java.lang.String,java.lang.String>>

Overrides:

execute in class AbstractCommand<java.util.Map<java.lang.String,java.lang.String>>

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

public java.lang.String getName()

Description copied from interface: ProofScriptCommand

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