de.uka.ilkd.key.macros.scripts

Class FocusOnSelectionAndHideCommand

java.lang.Object

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

de.uka.ilkd.key.macros.scripts.FocusOnSelectionAndHideCommand

All Implemented Interfaces:

ProofScriptCommand<FocusOnSelectionAndHideCommand.Parameters>

public class FocusOnSelectionAndHideCommand
extends AbstractCommand<FocusOnSelectionAndHideCommand.Parameters>

Hide all formulas that are not selected Parameter: * The sequent with those formulas that should not be hidden Created by sarah on 1/12/17.

Nested Class Summary

Nested Classes

Modifier and Type	Class and Description
(package private) static class	FocusOnSelectionAndHideCommand.Parameters

Field Summary

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

documentation, log, proof, service, state, uiControl

Constructor Summary

Constructors

Constructor and Description
FocusOnSelectionAndHideCommand()

Method Summary

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

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

evaluateArguments, execute, getArguments, getDocumentation

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Constructor Detail

FocusOnSelectionAndHideCommand

public FocusOnSelectionAndHideCommand()

Method Detail

execute

public void execute(FocusOnSelectionAndHideCommand.Parameters s)
             throws ScriptException,
                    java.lang.InterruptedException

Overrides:

execute in class AbstractCommand<FocusOnSelectionAndHideCommand.Parameters>

Throws:

ScriptException

java.lang.InterruptedException

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

hideAll

private void hideAll(Sequent toKeep)
              throws ParserException,
                     ScriptException

Hide all formulas of the sequent that are not focus sequent

Parameters:

toKeep -

Throws:

ParserException

ScriptException

getTaclet

private Taclet getTaclet(Term t,
                         java.lang.String pos)
                  throws ScriptException

Throws:

ScriptException

iterateThroughSequentAndFindNonMatch

private SequentFormula iterateThroughSequentAndFindNonMatch(Goal g,
                                                            Sequent toKeep)
                                                     throws ScriptException,
                                                            ParserException

Iterate through sequent and find first formula that is not in the list of formulas to keep and return this formula

Parameters:

g -

toKeep -

Returns:

formula to hide, if all formulas in the sequent should be kept, returns null

Throws:

ScriptException

ParserException

makeTacletApp

private void makeTacletApp(Goal g,
                           SequentFormula toHide,
                           Taclet tac,
                           boolean antec)
                    throws ScriptException

Make tacletApp for one sequent formula to hide on the sequent

Parameters:

g - the goal on which this hide rule should be applied to

toHide - the sequent formula to hide

tac - the taclet top apply (either hide_left or hide_right)

antec - whether the formula is in the antecedent

Throws:

ScriptException