de.uka.ilkd.key.macros.scripts

Class ActivateCommand

java.lang.Object

de.uka.ilkd.key.macros.scripts.NoArgumentCommand

de.uka.ilkd.key.macros.scripts.ActivateCommand

All Implemented Interfaces:

ProofScriptCommand<java.lang.Void>

public class ActivateCommand
extends NoArgumentCommand

Command for re-activating the first open (not necessarily enabled) Goal after a "leave" command. Can be useful for complicated proofs where "tryclose" should not apply on certain branches temporarily, but where one still wants to finish the proof.

Author:

Dominic Steinhoefel

Constructor Summary

Constructors

Constructor and Description
ActivateCommand()

Method Summary

Modifier and Type	Method and Description
void	execute(AbstractUserInterfaceControl uiControl, java.lang.Void args, EngineState state)
java.lang.String	getName() Returns the name of this proof command.

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

evaluateArguments, getArguments, getDocumentation

Methods inherited from class java.lang.Object

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

Constructor Detail

ActivateCommand

public ActivateCommand()

Method Detail

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

execute

public void execute(AbstractUserInterfaceControl uiControl,
                    java.lang.Void args,
                    EngineState state)
             throws ScriptException,
                    java.lang.InterruptedException

Parameters:

uiControl - the current ui controller

args - the script arguments

state - the current state

Throws:

ScriptException - if something bad happens

java.lang.InterruptedException - if something bad happens