001: // This file is part of KeY - Integrated Deductive Software Design
002: // Copyright (C) 2001-2007 Universitaet Karlsruhe, Germany
003: // Universitaet Koblenz-Landau, Germany
004: // Chalmers University of Technology, Sweden
005: //
006: // The KeY system is protected by the GNU General Public License.
007: // See LICENSE.TXT for details.
008: package de.uka.ilkd.key.gui.nodeviews;
009:
010: import java.util.Collection;
011: import java.util.Comparator;
012: import java.util.TreeSet;
013:
014: import javax.swing.JFrame;
015:
016: import de.uka.ilkd.key.java.Services;
017: import de.uka.ilkd.key.logic.Sequent;
018: import de.uka.ilkd.key.pp.NotationInfo;
019: import de.uka.ilkd.key.rule.ListOfTacletGoalTemplate;
020: import de.uka.ilkd.key.rule.NoFindTaclet;
021: import de.uka.ilkd.key.rule.Taclet;
022: import de.uka.ilkd.key.rule.TacletApp;
023:
024: /**
025: * This menu item groups all taclets which allow to insert class invariants
026: */
027: public class InsertSystemInvariantTacletMenuItem extends
028: InsertionTacletBrowserMenuItem {
029:
030: /**
031: * creates an instance of the insert hidden menu item
032: * @param parent the JFrame with the parent frame
033: * @param notInfo the NotationInfo to be used for pretty printing
034: * the apps
035: * @param services the Services
036: */
037: public InsertSystemInvariantTacletMenuItem(JFrame parent,
038: NotationInfo notInfo, Services services) {
039: super ("Insert Class Invariant", parent, notInfo, services);
040: }
041:
042: /**
043: * determines the sequent with the formulas to be added
044: * or null if the given taclet is not thought to be displayed
045: * by this component
046: * @param t the Taclet
047: * @return the sequent with the formulas to be added
048: * or null
049: */
050: protected Sequent checkTaclet(Taclet t) {
051: if (!(t instanceof NoFindTaclet)
052: || !t.displayName().startsWith("Insert invariants of")) {
053: return null;
054: }
055:
056: final ListOfTacletGoalTemplate goalTemplates = t
057: .goalTemplates();
058: if (goalTemplates.size() != 1)
059: return null;
060: return goalTemplates.head().sequent();
061: }
062:
063: /**
064: * show the taclets sorted
065: */
066: protected Collection createInsertionList() {
067: return new TreeSet(new Lexicographical());
068: }
069:
070: public TacletAppListItem createListItem(TacletApp app) {
071: return new ClassInvAppItem(app, checkTaclet(app.taclet()),
072: notInfo, services);
073: }
074:
075: final static class Lexicographical implements Comparator {
076: public int compare(Object arg0, Object arg1) {
077:
078: return ((TacletAppListItem) arg0).shortDescription()
079: .compareTo(
080: ((TacletAppListItem) arg1)
081: .shortDescription());
082: }
083: }
084:
085: /**
086: * inner class to pretty print the formulas to be added
087: */
088: static class ClassInvAppItem extends TacletAppListItem {
089:
090: public ClassInvAppItem(TacletApp app, Sequent seq,
091: NotationInfo notInfo, Services services) {
092: super (app, seq, notInfo, services);
093: }
094:
095: public String shortDescription() {
096: final String displayName = getTacletApp().taclet()
097: .displayName();
098: return displayName
099: .replaceFirst("Insert invariants of ", "");
100: }
101:
102: public String toString() {
103: return shortDescription();
104: }
105: }
106:
107: }
|