New Tactic Providers
From Event-B
The purpose is to give more flexibility to tactic providers by allowing them to provide as many tactic applications as they will for a given proof node, even they apply to the same predicate and at the same position.
Proposed Framework
public interface ITacticProvider2 { List<ITacticApplication> getPossibleApplications(IUserSupport userSupport, IProofTreeNode node, Predicate hyp, String globalInput); }
public interface ITacticApplication { void apply(String[] inputs, String globalInput, IProgressMonitor monitor); }
public interface IPositionApplication extends ITacticApplication { Point getHyperlinkBounds(); String getHyperlinkLabel(); }
public interface IPredicateApplication extends ITacticApplication { Image getIcon(); String getTip(); }