public class ActivateCommand extends NoArgumentCommand
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.Constructor and Description |
---|
ActivateCommand() |
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.
|
evaluateArguments, getArguments, getDocumentation
public java.lang.String getName()
ProofScriptCommand
ProofScriptEngine
public void execute(AbstractUserInterfaceControl uiControl, java.lang.Void args, EngineState state) throws ScriptException, java.lang.InterruptedException
uiControl
- the current ui controllerargs
- the script argumentsstate
- the current stateScriptException
- if something bad happensjava.lang.InterruptedException
- if something bad happens