public class MacroCommand extends AbstractCommand<MacroCommand.Parameters>
Modifier and Type | Class and Description |
---|---|
static class |
MacroCommand.Parameters |
Modifier and Type | Field and Description |
---|---|
private static java.util.Map<java.lang.String,ProofMacro> |
macroMap |
documentation, log, proof, service, state, uiControl
Constructor and Description |
---|
MacroCommand() |
Modifier and Type | Method and Description |
---|---|
MacroCommand.Parameters |
evaluateArguments(EngineState state,
java.util.Map<java.lang.String,java.lang.String> arguments) |
void |
execute(AbstractUserInterfaceControl uiControl,
MacroCommand.Parameters args,
EngineState state) |
static PosInOccurrence |
extractMatchingPio(Sequent sequent,
java.lang.String matchRegEx,
Services services)
TODO
|
private static java.lang.String |
formatTermString(java.lang.String str)
Removes spaces and line breaks from the string representation of a term.
|
java.lang.String |
getName()
Returns the name of this proof command.
|
private static java.util.Map<java.lang.String,ProofMacro> |
loadMacroMap() |
execute, getArguments, getDocumentation
private static java.util.Map<java.lang.String,ProofMacro> macroMap
private static java.util.Map<java.lang.String,ProofMacro> loadMacroMap()
public MacroCommand.Parameters evaluateArguments(EngineState state, java.util.Map<java.lang.String,java.lang.String> arguments) throws java.lang.Exception
evaluateArguments
in interface ProofScriptCommand<MacroCommand.Parameters>
evaluateArguments
in class AbstractCommand<MacroCommand.Parameters>
java.lang.Exception
public java.lang.String getName()
ProofScriptCommand
ProofScriptEngine
public void execute(AbstractUserInterfaceControl uiControl, MacroCommand.Parameters args, EngineState state) throws ScriptException, java.lang.InterruptedException
execute
in interface ProofScriptCommand<MacroCommand.Parameters>
execute
in class AbstractCommand<MacroCommand.Parameters>
uiControl
- the current ui controllerargs
- the script argumentsstate
- the current stateScriptException
- if something bad happensjava.lang.InterruptedException
- if something bad happenspublic static PosInOccurrence extractMatchingPio(Sequent sequent, java.lang.String matchRegEx, Services services) throws ScriptException
sequent
- matchRegEx
- services
- ScriptException
private static java.lang.String formatTermString(java.lang.String str)
str
- The string to "clean up".