de.uka.ilkd.key.macros.scripts

Class TryCloseCommand

java.lang.Object

de.uka.ilkd.key.macros.scripts.AbstractCommand<TryCloseCommand.TryCloseArguments>

de.uka.ilkd.key.macros.scripts.TryCloseCommand

All Implemented Interfaces:

ProofScriptCommand<TryCloseCommand.TryCloseArguments>

public class TryCloseCommand
extends AbstractCommand<TryCloseCommand.TryCloseArguments>

The script command tryclose" has two optional arguments:

• steps: INTEGER number of steps to use
• #2: STRING the branch which should be closed

TryClose tries to close the specified branch. If it is not successful within the specified number

Nested Class Summary

Nested Classes

Modifier and Type	Class and Description
static class	TryCloseCommand.TryCloseArguments

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
TryCloseCommand()

Method Summary

Modifier and Type	Method and Description
TryCloseCommand.TryCloseArguments	evaluateArguments(EngineState state, java.util.Map<java.lang.String,java.lang.String> arguments)
void	execute(TryCloseCommand.TryCloseArguments args)
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

TryCloseCommand

public TryCloseCommand()

Method Detail

evaluateArguments

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

Specified by:

evaluateArguments in interface ProofScriptCommand<TryCloseCommand.TryCloseArguments>

Overrides:

evaluateArguments in class AbstractCommand<TryCloseCommand.TryCloseArguments>

Returns:

Throws:

java.lang.Exception

execute

public void execute(TryCloseCommand.TryCloseArguments args)
             throws ScriptException,
                    java.lang.InterruptedException

Overrides:

execute in class AbstractCommand<TryCloseCommand.TryCloseArguments>

Throws:

ScriptException

java.lang.InterruptedException

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