public class AutoCommand extends AbstractCommand<AutoCommand.Parameters>
Modifier and Type | Class and Description |
---|---|
static class |
AutoCommand.Parameters |
documentation, log, proof, service, state, uiControl
Constructor and Description |
---|
AutoCommand() |
Modifier and Type | Method and Description |
---|---|
AutoCommand.Parameters |
evaluateArguments(EngineState state,
java.util.Map<java.lang.String,java.lang.String> arguments) |
void |
execute(AbstractUserInterfaceControl uiControl,
AutoCommand.Parameters arguments,
EngineState state) |
java.lang.String |
getName()
Returns the name of this proof command.
|
private void |
setupFocussedBreakpointStrategy(java.util.Optional<java.lang.String> maybeMatchesRegEx,
java.util.Optional<java.lang.String> breakpointArg,
Goal goal,
ProverCore proverCore,
Services services)
Sets up a focused automatic strategy.
|
execute, getArguments, getDocumentation
public java.lang.String getName()
ProofScriptCommand
ProofScriptEngine
public AutoCommand.Parameters evaluateArguments(EngineState state, java.util.Map<java.lang.String,java.lang.String> arguments)
evaluateArguments
in interface ProofScriptCommand<AutoCommand.Parameters>
evaluateArguments
in class AbstractCommand<AutoCommand.Parameters>
public void execute(AbstractUserInterfaceControl uiControl, AutoCommand.Parameters arguments, EngineState state) throws ScriptException, java.lang.InterruptedException
execute
in interface ProofScriptCommand<AutoCommand.Parameters>
execute
in class AbstractCommand<AutoCommand.Parameters>
uiControl
- the current ui controllerarguments
- the script argumentsstate
- the current stateScriptException
- if something bad happensjava.lang.InterruptedException
- if something bad happensprivate void setupFocussedBreakpointStrategy(java.util.Optional<java.lang.String> maybeMatchesRegEx, java.util.Optional<java.lang.String> breakpointArg, Goal goal, ProverCore proverCore, Services services) throws ScriptException
maybeMatchesRegEx
- The RegEx which should match on the sequent formula to focus.breakpointArg
- An optional breakpoint argument.goal
- The Goal
to apply the strategy on, needed for the rule
application manager.proverCore
- The ProverCore
, needed for resetting the strategy
afterward.services
- The Services
object.ScriptException