New Tactic Providers

From Event-B
Revision as of 10:04, 10 September 2009 by imported>Nicolas (Page bootstrap)
(diff) ← Older revision | Latest revision (diff) | Newer revision → (diff)
Jump to navigationJump to search

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