de.uka.ilkd.key.macros.scripts

Class MacroCommand

java.lang.Object

de.uka.ilkd.key.macros.scripts.AbstractCommand<MacroCommand.Parameters>

de.uka.ilkd.key.macros.scripts.MacroCommand

All Implemented Interfaces:

ProofScriptCommand<MacroCommand.Parameters>

public class MacroCommand
extends AbstractCommand<MacroCommand.Parameters>

Nested Class Summary

Nested Classes

Modifier and Type	Class and Description
static class	MacroCommand.Parameters

Field Summary

Fields

Modifier and Type	Field and Description
private static java.util.Map<java.lang.String,ProofMacro>	macroMap

Fields inherited from class de.uka.ilkd.key.macros.scripts.AbstractCommand

documentation, log, proof, service, state, uiControl

Constructor Summary

Constructors

Constructor and Description
MacroCommand()

Method Summary

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

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

Field Detail

macroMap

private static java.util.Map<java.lang.String,ProofMacro> macroMap

Constructor Detail

MacroCommand

public MacroCommand()

Method Detail

loadMacroMap

private static java.util.Map<java.lang.String,ProofMacro> loadMacroMap()

evaluateArguments

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

Specified by:

evaluateArguments in interface ProofScriptCommand<MacroCommand.Parameters>

Overrides:

evaluateArguments in class AbstractCommand<MacroCommand.Parameters>

Returns:

Throws:

java.lang.Exception

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,
                    MacroCommand.Parameters args,
                    EngineState state)
             throws ScriptException,
                    java.lang.InterruptedException

Specified by:

execute in interface ProofScriptCommand<MacroCommand.Parameters>

Overrides:

execute in class AbstractCommand<MacroCommand.Parameters>

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

extractMatchingPio

public static PosInOccurrence extractMatchingPio(Sequent sequent,
                                                 java.lang.String matchRegEx,
                                                 Services services)
                                          throws ScriptException

TODO

Parameters:

sequent -

matchRegEx -

services -

Returns:

Throws:

ScriptException

formatTermString

private static java.lang.String formatTermString(java.lang.String str)

Removes spaces and line breaks from the string representation of a term.

Parameters:

str - The string to "clean up".

Returns:

The original without spaces and line breaks.