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:
009: package de.uka.ilkd.key.gui.nodeviews;
010:
011: import java.awt.Point;
012: import java.awt.datatransfer.Transferable;
013: import java.awt.datatransfer.UnsupportedFlavorException;
014: import java.awt.dnd.DropTargetAdapter;
015: import java.awt.dnd.DropTargetDragEvent;
016: import java.awt.dnd.DropTargetDropEvent;
017: import java.awt.event.ActionEvent;
018: import java.awt.event.ActionListener;
019: import java.io.IOException;
020:
021: import javax.swing.JPopupMenu;
022:
023: import de.uka.ilkd.key.gui.KeYMediator;
024: import de.uka.ilkd.key.gui.configuration.ProofSettings;
025: import de.uka.ilkd.key.java.Services;
026: import de.uka.ilkd.key.logic.Constraint;
027: import de.uka.ilkd.key.logic.PosInOccurrence;
028: import de.uka.ilkd.key.logic.PosInTerm;
029: import de.uka.ilkd.key.logic.Sequent;
030: import de.uka.ilkd.key.logic.op.SchemaVariable;
031: import de.uka.ilkd.key.pp.PosInSequent;
032: import de.uka.ilkd.key.rule.*;
033: import de.uka.ilkd.key.rule.inst.IllegalInstantiationException;
034:
035: /**
036: * <p>
037: * The DragNDropInstantiator interpretes drag'n drop actions as taclet
038: * instantiations. The behaviour is described below (excluding some
039: * "optimisation" details)
040: * </p>
041: * <p>
042: * Let "source" denote the formula/term which is dragged and dropped on another
043: * term called "target". The DragNDropInstantiation of a taclet "t" is now
044: * defined as follows:
045: * <ol>
046: * <li>t must have exactly one formula/term in the <tt>find</tt> part and
047: * <tt>assumes</tt> sequent (in particular it must have an <tt>assumes</tt> -part)
048: * </li>
049: * <li>and
050: * <ol>
051: * <li>if t's goal descriptions do not contain any <tt>replacewith</tt> then
052: * "source" is matched against the <tt>find</tt> part of the taclet and
053: * "target" has to match the "if" part.</li>
054: * <li>if t's goal descriptions contain at least <em>one</em> replacewith
055: * then "target" is matched against the <tt>find</tt> part and "source"
056: * against the <tt>assumes</tt> part</li>*
057: * </ol>
058: * or
059: * <li>t must have a <tt>find</tt> part, no <tt>assumes</tt> and at least one
060: * addrule. In this case source is merged against <tt>find</tt> part and
061: * target has to be the complete sequent. Dropping on the sequent arrow is
062: * interpreted as applying an addrule(treats hide rules)</li>
063: * </ol>
064: * The DragNDropInstantiator now determines all taclets, which have a valid
065: * drag'n drop instantiation for a given (source, target) position pair. If
066: * there is only one taclet with a valid dnd-instantiation this one is executed
067: * otherwise the user is presented a list of possible taclets from which she/he
068: * can select one.
069: * </p>
070: */
071: public class DragNDropInstantiator extends DropTargetAdapter {
072:
073: /** the sequentview where dnd has been initiated */
074: private SequentView seqView;
075:
076: DragNDropInstantiator(SequentView seqView) {
077: this .seqView = seqView;
078: }
079:
080: public void drop(DropTargetDropEvent event) {
081:
082: Point dropLocation = event.getLocation();
083:
084: try {
085: Transferable transferable = event.getTransferable();
086: if (transferable
087: .isDataFlavorSupported(PosInSequentTransferable.POS_IN_SEQUENT_TRANSFER)) {
088: interpreteDragAndDropInstantiation(event, dropLocation,
089: transferable);
090: } else {
091: event.rejectDrop();
092: }
093: } catch (IOException exception) {
094: // just reject drop do not bother the user
095: event.rejectDrop();
096: } catch (UnsupportedFlavorException ufException) {
097: // just reject drop do not bother the user
098: event.rejectDrop();
099: }
100:
101: seqView.requestFocus();
102: }
103:
104: public void dragOver(DropTargetDragEvent dtde) {
105: seqView.autoscroll(dtde.getLocation());
106: seqView.paintHighlights(dtde.getLocation());
107: }
108:
109: /**
110: * Interpretes the drag and drop gesture. Checks which taclets could be
111: * meant by the drag'n drop and applies if the app can be uniquely
112: * determined, otherwise a selection menu is presented to the user
113: */
114: private void interpreteDragAndDropInstantiation(
115: DropTargetDropEvent event, Point dropLocation,
116: Transferable transferable)
117: throws UnsupportedFlavorException, IOException {
118:
119: final PosInSequent sourcePos = (PosInSequent) transferable
120: .getTransferData(PosInSequentTransferable.POS_IN_SEQUENT_TRANSFER);
121:
122: final PosInSequent targetPos = seqView
123: .getPosInSequent(dropLocation);
124:
125: if (targetPos == null || sourcePos == null
126: || sourcePos.isSequent()) {
127: event.rejectDrop();
128: return;
129: }
130:
131: final Services services = seqView.mediator().getServices();
132:
133: ListOfPosTacletApp applicableApps = getAllApplicableApps(
134: sourcePos, targetPos, services);
135:
136: if (applicableApps.isEmpty()
137: && !targetPos.isSequent()
138: && targetPos.getPosInOccurrence().posInTerm() != PosInTerm.TOP_LEVEL) {
139: // if no applicable taclet is found we relax the target position a bit
140: applicableApps = getAllApplicableApps(sourcePos,
141: PosInSequent.createCfmaPos(targetPos
142: .getPosInOccurrence().up()), services);
143: }
144:
145: // in case of an equal source and target position the selection list is shown
146: // even if only one rule is applicable in order to avoid an accidently
147: // rule appliciation of replace_knwon_* rules and entering
148: // the hell of non-confluence..
149: final boolean equalTargetPosition = sourcePos
150: .getPosInOccurrence().equals(
151: targetPos.getPosInOccurrence());
152:
153: if (!equalTargetPosition && applicableApps.size() == 1) {
154: execute(applicableApps.head());
155: } else if (applicableApps.size() >= 1) {
156: // open a pop up menu for user selection
157: SimpleTacletSelectionMenu menu = new SimpleTacletSelectionMenu(
158: applicableApps, seqView.mediator()
159: .getNotationInfo(), new PopupListener());
160:
161: JPopupMenu pm = menu.getPopupMenu();
162: pm.show(seqView, (int) dropLocation.getX(),
163: (int) dropLocation.getY());
164: } else {
165: // no rule applicable
166: event.rejectDrop();
167: return;
168: }
169: event.getDropTargetContext().dropComplete(true);
170: }
171:
172: /**
173: * retrieves all drag'n drop instantiable taclet applications
174: * @param sourcePos the PosInSequent where the drag started
175: * @param targetPos the PosInSequent where the drop occured
176: * @param services theServices providing access to the program model
177: * @return all drag'n drop instantiable taclet applications
178: */
179: private ListOfPosTacletApp getAllApplicableApps(
180: final PosInSequent sourcePos, final PosInSequent targetPos,
181: final Services services) {
182: final Sequent sequent = seqView.mediator().getSelectedGoal()
183: .sequent();
184:
185: final Constraint userConstraint = seqView.mediator()
186: .getUserConstraint().getConstraint();
187: ListOfPosTacletApp applicableApps = SLListOfPosTacletApp.EMPTY_LIST;
188: if (targetPos.isSequent()) {
189: // collects all applicable taclets at the source position
190: // which have an addrule section
191: applicableApps = applicableApps
192: .prepend(completeIfInstantiations(
193: getApplicableTaclets(
194: sourcePos,
195: TacletFilter.TACLET_WITH_NO_IF_FIND_AND_ADDRULE),
196: sequent, targetPos.getPosInOccurrence(),
197: userConstraint, services));
198: } else {
199: if (ProofSettings.DEFAULT_SETTINGS.getGeneralSettings()
200: .isDndDirectionSensitive()) {
201: applicableApps = applicableApps
202: .prepend(getDirectionDependentApps(sourcePos,
203: targetPos, services, sequent,
204: userConstraint));
205: } else {
206: applicableApps = applicableApps
207: .prepend(getDirectionIndependentApps(sourcePos,
208: targetPos, services, sequent,
209: userConstraint));
210: }
211: }
212: return applicableApps;
213: }
214:
215: /**
216: * returns all applicable apps respecting direction information in drag an drop
217: * @param sourcePos PosInSequent where the drag gesture started
218: * @param targetPos PosInSequent where the drop action took place
219: * @param services the Services
220: * @param sequent the Sequent
221: * @param userConstraint the user Constraint
222: * @return all applicable apps respecting direction information in drag an drop
223: */
224: private ListOfPosTacletApp getDirectionDependentApps(
225: final PosInSequent sourcePos, final PosInSequent targetPos,
226: final Services services, final Sequent sequent,
227: final Constraint userConstraint) {
228:
229: ListOfPosTacletApp applicableApps = SLListOfPosTacletApp.EMPTY_LIST;
230: // all applicable taclets where the drag source has been interpreted
231: // as
232: // the find part and the drop position as the one of the
233: // in this case only taclets with no replacewith part are considered
234: applicableApps = applicableApps
235: .prepend(completeIfInstantiations(
236: getApplicableTaclets(
237: sourcePos,
238: TacletFilter.TACLET_WITH_IF_FIND_AND_NO_REPLACEWITH),
239: sequent, targetPos.getPosInOccurrence(),
240: userConstraint, services));
241:
242: // switch source and target interpretation
243: // source is now the "If" instantiation and target the one of the
244: // find part in this case only the taclets with at least one
245: // replacewith part are considered
246: applicableApps = applicableApps
247: .prepend(completeIfInstantiations(
248: getApplicableTaclets(
249: targetPos,
250: TacletFilter.TACLET_WITH_IF_FIND_AND_REPLACEWITH),
251: sequent, sourcePos.getPosInOccurrence(),
252: userConstraint, services));
253:
254: // get those without an if sequent, in these we will try to apply this rule
255: // if: * one sv instantiation is missing
256: // * the term dropped on is a legal instantiation for this sv
257: applicableApps = applicableApps.prepend(completeInstantiations(
258: getApplicableTaclets(sourcePos,
259: TacletFilter.TACLET_WITH_NO_IF), targetPos
260: .getPosInOccurrence(), services));
261:
262: return applicableApps;
263: }
264:
265: /**
266: * returns all applicable apps without
267: * respecting direction information in drag an drop
268: * @param sourcePos PosInSequent where the drag gesture started
269: * @param targetPos PosInSequent where the drop action took place
270: * @param services the Services
271: * @param sequent the Sequent
272: * @param userConstraint the user Constraint
273: * @return all applicable apps respecting direction information in drag an drop
274: */
275: private ListOfPosTacletApp getDirectionIndependentApps(
276: PosInSequent sourcePos, PosInSequent targetPos,
277: final Services services, final Sequent sequent,
278: final Constraint userConstraint) {
279:
280: ListOfPosTacletApp applicableApps = SLListOfPosTacletApp.EMPTY_LIST;
281:
282: applicableApps = getDirectionDependentApps(sourcePos,
283: targetPos, services, sequent, userConstraint).prepend(
284: getDirectionDependentApps(targetPos, sourcePos,
285: services, sequent, userConstraint));
286:
287: return applicableApps;
288: }
289:
290: /**
291: * retrieves all taclets applicable on the given position and select those
292: * that fulfill the given filter condition. The filter selects taclets
293: * satisfying certain syntactic categories (for example, taclets with at
294: * least one replacewith in their goal description or those without any
295: * replacewith).
296: *
297: * @param findPos
298: * the PosInSequent specifying the formula/term that has to be
299: * matched by the find part of a taclet
300: * @param filter
301: * the TacletFilter specifying syntactic restrictions on the
302: * taclets to be returned
303: * @return the list of taclets which match the term at the given position
304: * and satisfy the filter condition
305: */
306: private ListOfPosTacletApp getApplicableTaclets(
307: PosInSequent findPos, TacletFilter filter) {
308:
309: if (findPos == null || findPos.isSequent()) {
310: return SLListOfPosTacletApp.EMPTY_LIST;
311: }
312:
313: ListOfTacletApp allTacletsAtFindPosition = SLListOfTacletApp.EMPTY_LIST;
314:
315: final IteratorOfTacletApp it = seqView.mediator()
316: .getFindTaclet(findPos).iterator();
317: // if in replaceWithMode only apps that contain at least one replacewith
318: // are collected. Otherwise only those without a replacewith.
319: while (it.hasNext()) {
320: final TacletApp app = it.next();
321: if (filter.satisfiesFilterCondition(app.taclet())) {
322: allTacletsAtFindPosition = allTacletsAtFindPosition
323: .prepend(app);
324: }
325: }
326:
327: return addPositionInformation(allTacletsAtFindPosition, findPos
328: .getPosInOccurrence());
329: }
330:
331: /**
332: * the taclet applications is given the correct position information where
333: * their "find" has been matched
334: *
335: * @param tacletApps
336: * the ListOfTacletApp with taclet applications to be enriched by
337: * position information
338: * @param findPos
339: * the PosInOccurrence against which the find part has been
340: * matched
341: * @return the taclet apps as given in <tt>tacletApps</tt> but with
342: * position information
343: */
344: private ListOfPosTacletApp addPositionInformation(
345: ListOfTacletApp tacletApps, PosInOccurrence findPos) {
346:
347: ListOfPosTacletApp applicableApps = SLListOfPosTacletApp.EMPTY_LIST;
348: IteratorOfTacletApp it = tacletApps.iterator();
349: while (it.hasNext()) {
350: TacletApp app = it.next();
351: if (app instanceof NoPosTacletApp) {
352: app = PosTacletApp.createPosTacletApp((FindTaclet) app
353: .taclet(), app.matchConditions(), findPos);
354: }
355: applicableApps = applicableApps.prepend((PosTacletApp) app);
356: }
357: return applicableApps;
358: }
359:
360: /**
361: * tries to complete the (partial) taclet instantantiation of the
362: * applications given in <tt>apps</tt>. The resulting applications are
363: * returned. The given apps must have either all an if part or none of them.
364: *
365: * @param apps
366: * the ListOfPosTacletApp with all apps whose if sequent has to
367: * be matched against the formula specified by the pair
368: * <tt>seq</tt> and <tt>ifPIO</tt>
369: * @param seq
370: * the Sequent to which the position information in <tt>ifPIO<tt>
371: * is relative to
372: * @param ifPIO the PosInOccurrence describing the position of the term to
373: * be matched against the if sequent of the taclets
374: * @param userConstraint the Constraint describing user instantiations of
375: * metavariables
376: * @param services the Services
377: * @return the ListOfPosTacletApp that have been matched successfully
378: */
379: private ListOfPosTacletApp completeIfInstantiations(
380: ListOfPosTacletApp apps, Sequent seq,
381: PosInOccurrence ifPIO, Constraint userConstraint,
382: Services services) {
383:
384: ListOfPosTacletApp result = SLListOfPosTacletApp.EMPTY_LIST;
385:
386: final ListOfIfFormulaInstantiation ifFmlInst;
387:
388: if (ifPIO == null || !ifPIO.isTopLevel()) {
389: // if formula have to be top level formulas
390: // TODO: should update prefix be allowed?
391: ifFmlInst = null;
392: } else {
393: final IfFormulaInstSeq ifInst = new IfFormulaInstSeq(seq,
394: ifPIO.isInAntec(), ifPIO.constrainedFormula());
395: ifFmlInst = SLListOfIfFormulaInstantiation.EMPTY_LIST
396: .prepend(ifInst);
397: }
398:
399: final IteratorOfPosTacletApp it = apps.iterator();
400: while (it.hasNext()) {
401: PosTacletApp app = it.next();
402:
403: final Sequent ifSequent = app.taclet().ifSequent();
404: if (ifSequent != null && !ifSequent.isEmpty()) {
405: if (ifSequent.size() != 1) {
406: // currently dnd is only supported for taclets with exact one formula
407: // in the if sequent
408: app = null;
409: } else if (ifFmlInst == null) {
410: // as either all taclets have an if sequent or none
411: // we can exit here
412: return SLListOfPosTacletApp.EMPTY_LIST;
413: } else {
414: // the right side is not checked in tacletapp
415: // not sure where to incorporate the check...
416: if (((IfFormulaInstSeq) ifFmlInst.head()).inAntec() == (ifSequent
417: .succedent().size() == 0)) {
418: app = (PosTacletApp) app
419: .setIfFormulaInstantiations(ifFmlInst,
420: services, userConstraint);
421: }
422: }
423: }
424: if (app != null && app.complete()) {
425: //allow use of sufficientlyComplete here?
426: result = result.prepend(app);
427: }
428: }
429: return result;
430: }
431:
432: /**
433: * tries to complete the (partial) taclet instantantiation of the
434: * applications given in <tt>apps</tt>. The resulting applications are
435: * returned.
436: *
437: * @param apps
438: * the ListOfPosTacletApp with all apps whose if sequent has to
439: * be matched against the formula specified by the pair
440: * <tt>seq</tt> and <tt>ifPIO</tt>
441: * @param seq
442: * the Sequent to which the position information in <tt>ifPIO<tt>
443: * is relative to
444: * @param missingSVPIO the PosInOccurrence describing the position of the term an
445: * uninstantiated SV will be matched against
446: * @param userConstraint the Constraint describing user instantiations of
447: * metavariables
448: * @param services the Services
449: * @return the ListOfPosTacletApp that have been matched successfully
450: */
451: private ListOfPosTacletApp completeInstantiations(
452: ListOfPosTacletApp apps, PosInOccurrence missingSVPIO,
453: Services services) {
454:
455: ListOfPosTacletApp result = SLListOfPosTacletApp.EMPTY_LIST;
456: if (missingSVPIO == null) {
457: return SLListOfPosTacletApp.EMPTY_LIST;
458: }
459:
460: final IteratorOfPosTacletApp it = apps.iterator();
461: while (it.hasNext()) {
462: PosTacletApp app = it.next();
463:
464: final SchemaVariable missingSV;
465: final Sequent ifSequent = app.taclet().ifSequent();
466:
467: if ((ifSequent != null && !ifSequent.isEmpty())
468: || app.uninstantiatedVars().size() != 1) {
469: continue;
470: } else {
471: missingSV = app.uninstantiatedVars().iterator().next();
472: }
473: try {
474: app = (PosTacletApp) app.addCheckedInstantiation(
475: missingSV, missingSVPIO.subTerm(), services,
476: true);
477: } catch (IllegalInstantiationException ie) {
478: app = null;
479: }
480:
481: if (app != null && app.sufficientlyComplete()) {
482: result = result.prepend(app);
483: }
484: }
485: return result;
486: }
487:
488: /**
489: * applies the given app
490: *
491: * @param app
492: * the PosTacletApp to be applied
493: */
494: private void execute(PosTacletApp app) {
495: if (app == null) {
496: return;
497: }
498: final KeYMediator mediator = seqView.mediator();
499: mediator.applyInteractive(app, mediator.getSelectedGoal());
500: }
501:
502: /**
503: * This popup listener listens to the taclet app selection listener and
504: * executes the selected app if necessary
505: */
506: private class PopupListener implements ActionListener {
507:
508: /*
509: * (non-Javadoc)
510: *
511: * @see java.awt.event.ActionListener#actionPerformed(java.awt.event.ActionEvent)
512: */
513: public void actionPerformed(ActionEvent e) {
514: if (e.getSource() instanceof DefaultTacletMenuItem) {
515: final TacletMenuItem item = (TacletMenuItem) e
516: .getSource();
517: DragNDropInstantiator.this .execute((PosTacletApp) item
518: .connectedTo());
519: }
520: }
521: }
522:
523: /**
524: * This interface is impemented by filters selecting certain kinds of
525: * taclets depending on their syntactic structure
526: */
527: protected interface TacletFilter {
528:
529: /**
530: * This filter selects all Taclet which have an <tt>assumes</tt>,
531: * <tt>find</tt> and at least one <tt>replacewith</tt> part.
532: */
533: TacletFilter TACLET_WITH_IF_FIND_AND_REPLACEWITH = new TacletWithIfFindAndReplacewith();
534:
535: /**
536: * This filter selects all Taclet which have an <tt>assumes</tt>,
537: * <tt>find</tt> and <em>no</em> <tt>replacewith</tt> part.
538: */
539: TacletFilter TACLET_WITH_IF_FIND_AND_NO_REPLACEWITH = new TacletWithIfFindAndNoReplacewith();
540:
541: /**
542: * This filter selects all Taclet which have an <tt>assumes</tt>,
543: * <tt>find</tt> and <em>no</em> <tt>replacewith</tt> part.
544: */
545: TacletFilter TACLET_WITH_NO_IF_FIND_AND_ADDRULE = new TacletWithNoIfFindAndAddrule();
546:
547: /**
548: * This filter selects all Taclets which have no <tt>assumes</tt>,
549: * sequent but a <tt>find</tt>part.
550: */
551: TacletFilter TACLET_WITH_NO_IF = new TacletWithNoIf();
552:
553: /**
554: * checks if the taclet satisfies certain syntactic criterias
555: *
556: * @param taclet
557: * the Taclet to be tested
558: * @return true if filter condition is fulfilled
559: */
560: boolean satisfiesFilterCondition(Taclet taclet);
561:
562: /**
563: * This filter selects all Taclet which have an <tt>assumes</tt>,
564: * <tt>find</tt> and at least one <tt>replacewith</tt> part.
565: */
566: class TacletWithIfFindAndReplacewith implements TacletFilter {
567:
568: private TacletWithIfFindAndReplacewith() {
569: }
570:
571: /**
572: * tests if the given taclet consists of an <tt>assumes</tt>,
573: * <tt>find</tt> and <tt>replacewith</tt> part and returns true
574: * if the test is positive
575: */
576: public boolean satisfiesFilterCondition(Taclet taclet) {
577: return taclet.ifSequent() != null
578: && !taclet.ifSequent().isEmpty()
579: && taclet instanceof FindTaclet
580: && taclet.hasReplaceWith();
581: }
582: }
583:
584: /**
585: * This filter selects all Taclet which have an <tt>assumes</tt>,
586: * <tt>find</tt> and <em>no</em> <tt>replacewith</tt> part.
587: */
588: class TacletWithIfFindAndNoReplacewith implements TacletFilter {
589:
590: private TacletWithIfFindAndNoReplacewith() {
591: }
592:
593: /**
594: * tests if the given taclet consists of an <tt>assumes</tt>,
595: * <tt>find</tt> and <em>no</em> <tt>replacewith</tt> part and
596: * returns true if the test is positive
597: */
598: public boolean satisfiesFilterCondition(Taclet taclet) {
599: return taclet.ifSequent() != null
600: && !taclet.ifSequent().isEmpty()
601: && taclet instanceof FindTaclet
602: && !taclet.hasReplaceWith();
603: }
604: }
605:
606: /**
607: * This filter selects all Taclet which have no <tt>assumes</tt>, but a
608: * <tt>find</tt> and at least one <tt>addrule</tt> section.
609: */
610: class TacletWithNoIfFindAndAddrule implements TacletFilter {
611:
612: private TacletWithNoIfFindAndAddrule() {
613: }
614:
615: /**
616: * tests if the goal templates contain at least one addrule section
617: *
618: * @param goalDescriptions
619: * the ListOfTacletGoalTemplate to be looked through
620: * @return true if an addrule section has been found
621: */
622: private boolean goalTemplatesContainAddrules(
623: ListOfTacletGoalTemplate goalDescriptions) {
624: final IteratorOfTacletGoalTemplate it = goalDescriptions
625: .iterator();
626: while (it.hasNext()) {
627: final TacletGoalTemplate tgt = it.next();
628: if (tgt.rules().size() >= 1) {
629: return true;
630: }
631: }
632:
633: return false;
634: }
635:
636: /**
637: * tests if the given taclet consists of an <tt>assume</tt>,
638: * <tt>find</tt> and <em>no</em> <tt>replacewith</tt> part and
639: * returns true if the test is positive
640: */
641: public boolean satisfiesFilterCondition(Taclet taclet) {
642: // TODO: the null checks should be unneccessary
643: return (taclet.ifSequent() == null || taclet
644: .ifSequent().isEmpty())
645: && taclet instanceof FindTaclet
646: && goalTemplatesContainAddrules(taclet
647: .goalTemplates());
648: }
649: }
650:
651: /**
652: * This filter selects all Taclet which have no <tt>assume</tt>, but a
653: * <tt>find</tt>.
654: */
655: class TacletWithNoIf implements TacletFilter {
656:
657: private TacletWithNoIf() {
658: }
659:
660: /**
661: * checks if the taclet has a find part and no assumes sequent
662: */
663: public boolean satisfiesFilterCondition(Taclet taclet) {
664: // TODO: the null checks should be unneccessary
665: final Sequent ifSequent = taclet.ifSequent();
666: return ((ifSequent == null || ifSequent.isEmpty()) && taclet instanceof FindTaclet);
667:
668: }
669:
670: }
671:
672: }
673: }
|