public class FocusOnSelectionAndHideCommand extends AbstractCommand<FocusOnSelectionAndHideCommand.Parameters>
Modifier and Type | Class and Description |
---|---|
(package private) static class |
FocusOnSelectionAndHideCommand.Parameters |
documentation, log, proof, service, state, uiControl
Constructor and Description |
---|
FocusOnSelectionAndHideCommand() |
Modifier and Type | Method and Description |
---|---|
void |
execute(FocusOnSelectionAndHideCommand.Parameters s) |
java.lang.String |
getName()
Returns the name of this proof command.
|
private Taclet |
getTaclet(Term t,
java.lang.String pos) |
private void |
hideAll(Sequent toKeep)
Hide all formulas of the sequent that are not focus sequent
|
private SequentFormula |
iterateThroughSequentAndFindNonMatch(Goal g,
Sequent toKeep)
Iterate through sequent and find first formula that is not in the list of formulas to keep and return this formula
|
private void |
makeTacletApp(Goal g,
SequentFormula toHide,
Taclet tac,
boolean antec)
Make tacletApp for one sequent formula to hide on the sequent
|
evaluateArguments, execute, getArguments, getDocumentation
public void execute(FocusOnSelectionAndHideCommand.Parameters s) throws ScriptException, java.lang.InterruptedException
execute
in class AbstractCommand<FocusOnSelectionAndHideCommand.Parameters>
ScriptException
java.lang.InterruptedException
public java.lang.String getName()
ProofScriptCommand
ProofScriptEngine
private void hideAll(Sequent toKeep) throws ParserException, ScriptException
toKeep
- ParserException
ScriptException
private Taclet getTaclet(Term t, java.lang.String pos) throws ScriptException
ScriptException
private SequentFormula iterateThroughSequentAndFindNonMatch(Goal g, Sequent toKeep) throws ScriptException, ParserException
g
- toKeep
- ScriptException
ParserException
private void makeTacletApp(Goal g, SequentFormula toHide, Taclet tac, boolean antec) throws ScriptException
g
- the goal on which this hide rule should be applied totoHide
- the sequent formula to hidetac
- the taclet top apply (either hide_left or hide_right)antec
- whether the formula is in the antecedentScriptException