Package | Description |
---|---|
de.uka.ilkd.key.api |
This package gives an high-level entry point to the KeY world.
|
de.uka.ilkd.key.macros.scripts |
Proof script commands are a simple proof automation facility.
|
Modifier and Type | Method and Description |
---|---|
<T> ScriptResults |
ScriptApi.executeScriptCommand(ProofScriptCommandCall<T> call,
ProjectedNode onNode)
Execute ScriptCommand onto goal node
|
Modifier and Type | Class and Description |
---|---|
class |
ProofAlreadyClosedException
Thrown if during the execution of a command, the proof is already closed.
|
Modifier and Type | Method and Description |
---|---|
void |
AutoCommand.execute(AbstractUserInterfaceControl uiControl,
AutoCommand.Parameters arguments,
EngineState state) |
void |
CutCommand.execute(AbstractUserInterfaceControl uiControl,
CutCommand.Parameters args,
EngineState state) |
void |
EchoCommand.execute(AbstractUserInterfaceControl uiControl,
EchoCommand.Parameters args,
EngineState state) |
void |
InstantiateCommand.execute(AbstractUserInterfaceControl uiControl,
InstantiateCommand.Parameters params,
EngineState state) |
void |
MacroCommand.execute(AbstractUserInterfaceControl uiControl,
MacroCommand.Parameters args,
EngineState state) |
void |
SaveInstCommand.execute(AbstractUserInterfaceControl uiControl,
java.util.Map<java.lang.String,java.lang.String> args,
EngineState stateMap) |
void |
LetCommand.execute(AbstractUserInterfaceControl uiControl,
java.util.Map<java.lang.String,java.lang.String> args,
EngineState stateMap) |
void |
ProofScriptEngine.execute(AbstractUserInterfaceControl uiControl,
Proof proof) |
void |
RewriteCommand.execute(AbstractUserInterfaceControl uiControl,
RewriteCommand.Parameters args,
EngineState state) |
void |
RuleCommand.execute(AbstractUserInterfaceControl uiControl,
RuleCommand.Parameters args,
EngineState state) |
void |
SaveNewNameCommand.execute(AbstractUserInterfaceControl uiControl,
SaveNewNameCommand.Parameters params,
EngineState stateMap) |
void |
SetEchoCommand.execute(AbstractUserInterfaceControl uiControl,
SetEchoCommand.Parameters args,
EngineState state) |
void |
SetFailOnClosedCommand.execute(AbstractUserInterfaceControl uiControl,
SetFailOnClosedCommand.Parameters args,
EngineState state) |
void |
ProofScriptCommand.execute(AbstractUserInterfaceControl uiControl,
T args,
EngineState stateMap) |
void |
AbstractCommand.execute(AbstractUserInterfaceControl uiControl,
T args,
EngineState stateMap) |
void |
SkipCommand.execute(AbstractUserInterfaceControl uiControl,
java.lang.Void args,
EngineState stateMap) |
void |
LeaveCommand.execute(AbstractUserInterfaceControl uiControl,
java.lang.Void args,
EngineState state) |
void |
ActivateCommand.execute(AbstractUserInterfaceControl uiControl,
java.lang.Void args,
EngineState state) |
void |
ExitCommand.execute(AbstractUserInterfaceControl uiControl,
java.lang.Void args,
EngineState stateMap) |
void |
AssertCommand.execute(AssertCommand.Parameters args) |
void |
AssumeCommand.execute(AssumeCommand.FormulaParameter parameter) |
void |
AxiomCommand.execute(AxiomCommand.FormulaParameter parameter) |
void |
FocusOnSelectionAndHideCommand.execute(de.uka.ilkd.key.macros.scripts.FocusOnSelectionAndHideCommand.Parameters s) |
void |
JavascriptCommand.execute(JavascriptCommand.Parameters args) |
void |
SchemaVarCommand.execute(SchemaVarCommand.Parameters args) |
void |
ScriptCommand.execute(ScriptCommand.Parameters args) |
void |
SelectCommand.execute(SelectCommand.Parameters args) |
void |
SetCommand.execute(SetCommand.Parameters args) |
void |
SMTCommand.execute(SMTCommand.SMTCommandArguments args) |
protected void |
AbstractCommand.execute(T args) |
void |
TryCloseCommand.execute(TryCloseCommand.TryCloseArguments args) |
static PosInOccurrence |
MacroCommand.extractMatchingPio(Sequent sequent,
java.lang.String matchRegEx,
Services services)
TODO
|
Goal |
EngineState.getFirstOpenAutomaticGoal() |
Goal |
EngineState.getFirstOpenGoal(boolean checkAutomatic)
Returns the first open goal, which has to be automatic iff checkAutomatic
is true.
|
Sequent |
JavascriptCommand.JavascriptInterface.getSelectedGoal() |
static void |
ScriptTreeParser.main(java.lang.String[] args) |
static ScriptNode |
ScriptTreeParser.parse(java.io.Reader reader) |
void |
JavascriptCommand.JavascriptInterface.setVar(java.lang.String var,
java.lang.String term) |
void |
JavascriptCommand.JavascriptInterface.setVar(java.lang.String var,
Term term) |
Sequent |
EngineState.toSequent(java.lang.String sequent) |
Sort |
EngineState.toSort(java.lang.String sortName) |
Term |
EngineState.toTerm(java.lang.String string,
Sort sort) |
Copyright © 2003-2019 The KeY-Project.