0001: // This file is part of KeY - Integrated Deductive Software Design
0002: // Copyright (C) 2001-2007 Universitaet Karlsruhe, Germany
0003: // Universitaet Koblenz-Landau, Germany
0004: // Chalmers University of Technology, Sweden
0005: //
0006: // The KeY system is protected by the GNU General Public License.
0007: // See LICENSE.TXT for details.
0008: //
0009: //
0010:
0011: package de.uka.ilkd.key.gui;
0012:
0013: import java.awt.Component;
0014: import java.awt.Dimension;
0015: import java.awt.Point;
0016: import java.awt.event.ActionEvent;
0017: import java.awt.event.ActionListener;
0018:
0019: import javax.swing.*;
0020: import javax.swing.event.EventListenerList;
0021:
0022: import de.uka.ilkd.key.gui.configuration.ProofSettings;
0023: import de.uka.ilkd.key.gui.notification.events.NotificationEvent;
0024: import de.uka.ilkd.key.gui.notification.events.ProofClosedNotificationEvent;
0025: import de.uka.ilkd.key.java.JavaInfo;
0026: import de.uka.ilkd.key.java.Services;
0027: import de.uka.ilkd.key.logic.*;
0028: import de.uka.ilkd.key.pp.NotationInfo;
0029: import de.uka.ilkd.key.pp.PosInSequent;
0030: import de.uka.ilkd.key.proof.*;
0031: import de.uka.ilkd.key.proof.init.JavaProfile;
0032: import de.uka.ilkd.key.proof.init.Profile;
0033: import de.uka.ilkd.key.proof.mgt.GlobalProofMgt;
0034: import de.uka.ilkd.key.proof.reuse.ReusePoint;
0035: import de.uka.ilkd.key.rule.*;
0036: import de.uka.ilkd.key.unittest.UnitTestBuilder;
0037: import de.uka.ilkd.key.util.Debug;
0038: import de.uka.ilkd.key.util.ExtList;
0039: import de.uka.ilkd.key.util.KeYExceptionHandler;
0040: import de.uka.ilkd.key.util.KeYRecoderExcHandler;
0041: import de.uka.ilkd.key.visualization.ProofVisualization;
0042:
0043: public class KeYMediator {
0044:
0045: private Main mainFrame;
0046:
0047: private InteractiveProver interactiveProver;
0048:
0049: /** the update simplifier (may be moved to nodes)*/
0050: private UpdateSimplifier upd_simplifier;
0051:
0052: /** the notation info used to print sequents */
0053: private final NotationInfo notationInfo;
0054:
0055: /** the proof the mediator handles with */
0056: private Proof proof;
0057:
0058: /** listenerList with to gui listeners */
0059: private EventListenerList listenerList = new EventListenerList();
0060:
0061: /** listens to the proof */
0062: private KeYMediatorProofListener proofListener;
0063:
0064: /** listens to the ProofTree */
0065: private KeYMediatorProofTreeListener proofTreeListener;
0066:
0067: /** current proof and node the user works with. All user
0068: * interaction is relative to this model
0069: */
0070: private KeYSelectionModel keySelectionModel;
0071:
0072: private KeYExceptionHandler defaultExceptionHandler;
0073:
0074: private boolean stupidMode; // minimize user interaction
0075:
0076: private boolean autoMode; // autoModeStarted has been fired
0077:
0078: /** creates the KeYMediator with a reference to the application's
0079: * main frame and the current proof settings
0080: */
0081: public KeYMediator(Main mainFrame) {
0082: this .mainFrame = mainFrame;
0083: notationInfo = NotationInfo.createInstance();
0084: proofListener = new KeYMediatorProofListener();
0085: proofTreeListener = new KeYMediatorProofTreeListener();
0086: keySelectionModel = new KeYSelectionModel();
0087: interactiveProver = new InteractiveProver(this );
0088: new SkolemAbbreviator(this ); // SkolemAbbreviator registers itself
0089: addRuleAppListener(proofListener);
0090: addAutoModeListener(proofListener);
0091: GlobalProofMgt.getInstance().setMediator(this );
0092: defaultExceptionHandler = new KeYRecoderExcHandler();
0093: }
0094:
0095: /** returns the used NotationInfo
0096: * @return the used NotationInfo
0097: */
0098: public NotationInfo getNotationInfo() {
0099: return notationInfo;
0100: }
0101:
0102: public KeYExceptionHandler getExceptionHandler() {
0103: if (getProof() != null) {
0104: return getServices().getExceptionHandler();
0105: } else {
0106: return defaultExceptionHandler;
0107: }
0108: }
0109:
0110: /** returns the variable namespace
0111: * @return the variable namespace
0112: */
0113: public Namespace var_ns() {
0114: return getProof().getNamespaces().variables();
0115: }
0116:
0117: /** returns the program variable namespace
0118: * @return the program variable namespace
0119: */
0120: public Namespace progVar_ns() {
0121: return getProof().getNamespaces().programVariables();
0122: }
0123:
0124: /** returns the function namespace
0125: * @return the function namespace
0126: */
0127: public Namespace func_ns() {
0128: return getProof().getNamespaces().functions();
0129: }
0130:
0131: /** returns the sort namespace
0132: * @return the sort namespace
0133: */
0134: public Namespace sort_ns() {
0135: return getProof().getNamespaces().sorts();
0136: }
0137:
0138: /** returns the heuristics namespace
0139: * @return the heuristics namespace
0140: */
0141: public Namespace heur_ns() {
0142: return getProof().getNamespaces().ruleSets();
0143: }
0144:
0145: /** returns the choice namespace
0146: * @return the choice namespace
0147: */
0148: public Namespace choice_ns() {
0149: return getProof().getNamespaces().choices();
0150: }
0151:
0152: /** returns the prog var namespace
0153: * @return the prog var namespace
0154: */
0155: public Namespace pv_ns() {
0156: return getProof().getNamespaces().programVariables();
0157: }
0158:
0159: /** returns the namespace set
0160: * @return the namespace set
0161: */
0162: public NamespaceSet namespaces() {
0163: return getProof().getNamespaces();
0164: }
0165:
0166: /** returns the JavaInfo with the java type information */
0167: public JavaInfo getJavaInfo() {
0168: return getProof().getJavaInfo();
0169: }
0170:
0171: /** returns the Services with the java service classes */
0172: public Services getServices() {
0173: return getProof().getServices();
0174: }
0175:
0176: /** returns the user constraint (table model)
0177: * @return the user constraint
0178: */
0179: public ConstraintTableModel getUserConstraint() {
0180: if (getProof() == null)
0181: return null;
0182: else
0183: return getProof().getUserConstraint();
0184: }
0185:
0186: /** @return Deliverer of new metavariables (with unique names)*/
0187: public MetavariableDeliverer getMetavariableDeliverer() {
0188: if (getProof() == null)
0189: return null;
0190: else
0191: return getProof().getMetavariableDeliverer();
0192: }
0193:
0194: // /** returns the proof settings
0195: // * @return the proof settings
0196: // */
0197: // public ProofSettings proofSettings() {
0198: // return proofSettings;
0199: // }
0200:
0201: /** simplified user interface? */
0202: public boolean stupidMode() {
0203: return stupidMode;
0204: }
0205:
0206: public void setStupidMode(boolean b) {
0207: stupidMode = b;
0208: }
0209:
0210: public boolean ensureProofLoadedSilent() {
0211: if (proof == null) {
0212: return false;
0213: }
0214: return true;
0215: }
0216:
0217: public boolean ensureProofLoaded() {
0218: final boolean loaded = ensureProofLoadedSilent();
0219: if (!loaded) {
0220: popupWarning("No proof.", "Oops...");
0221: }
0222: return loaded;
0223: }
0224:
0225: /** Undo.
0226: * @author VK
0227: */
0228: public void setBack() {
0229: if (ensureProofLoaded()) {
0230: setBack(getSelectedGoal());
0231: }
0232: }
0233:
0234: public void setBack(Node node) {
0235: if (ensureProofLoaded()) {
0236: if (!proof.setBack(node)) {
0237: popupWarning(
0238: "Setting back at the chosen node is not possible.",
0239: "Oops...");
0240: }
0241: }
0242: }
0243:
0244: public void setBack(Goal goal) {
0245: if (ensureProofLoaded()) {
0246: if (proof == null || !proof.setBack(goal))
0247: popupWarning(
0248: "Setting back the current goal is not possible.",
0249: "Oops...");
0250: }
0251: }
0252:
0253: public ProofVisualization visualizeProof() {
0254: if (ensureProofLoaded()) {
0255: return new ProofVisualization(getSelectedNode(),
0256: getServices());
0257: }
0258: return null;
0259: }
0260:
0261: public void testCaseConfirmation(String path) {
0262: JOptionPane.showMessageDialog(null,
0263: "A unittest was generated and written to " + path,
0264: "Unittest generated", JOptionPane.INFORMATION_MESSAGE);
0265: }
0266:
0267: public void testCaseConfirmation(String path, int coverage) {
0268: JOptionPane
0269: .showMessageDialog(null,
0270: "A unittest was generated and written to "
0271: + path
0272: + "\nTop-Level Statement Coverage: "
0273: + coverage, "Unittest generated",
0274: JOptionPane.INFORMATION_MESSAGE);
0275: }
0276:
0277: public void generateTestCaseForSelectedNode() {
0278: if (ensureProofLoaded()) {
0279: UnitTestBuilder testBuilder = new UnitTestBuilder(
0280: getServices(), getProof());
0281: try {
0282: testCaseConfirmation(testBuilder
0283: .createTestForNode(getSelectedNode()));
0284: } catch (Exception e) {
0285: ExtList l = new ExtList();
0286: l.add(e);
0287: new ExceptionDialog(Main.getInstance(), l);
0288: }
0289: }
0290: }
0291:
0292: /**
0293: * initializes proof (this is Swing thread-safe)
0294: */
0295: public void setProof(Proof p) {
0296: final Proof pp = p;
0297: if (SwingUtilities.isEventDispatchThread()) {
0298: setProofHelper(pp);
0299: } else {
0300: Runnable swingProzac = new Runnable() {
0301: public void run() {
0302: setProofHelper(pp);
0303: }
0304: };
0305: invokeAndWait(swingProzac);
0306: }
0307: }
0308:
0309: private void setProofHelper(Proof p) {
0310: if (proof != null) {
0311: proof.removeProofTreeListener(proofTreeListener);
0312: }
0313: if (p != null)
0314: notationInfo.setAbbrevMap(p.abbreviations());
0315: proof = p;
0316: if (proof != null) {
0317: proof.addProofTreeListener(proofTreeListener);
0318: proof.mgt().setMediator(this );
0319: proof.setSimplifier(upd_simplifier);
0320: }
0321: keySelectionModel.setSelectedProof(proof);
0322: }
0323:
0324: /**
0325: * Get the interactive prover.
0326: */
0327: public InteractiveProver getInteractiveProver() {
0328: return interactiveProver;
0329: }
0330:
0331: public Proof getProof() {
0332: return proof;
0333: }
0334:
0335: /** sets the maximum number of rule applications allowed in
0336: * automatic mode
0337: * @param steps an int setting the limit
0338: */
0339: public void setMaxAutomaticSteps(int steps) {
0340: if (proof != null) {
0341: proof.getSettings().getStrategySettings()
0342: .setMaxSteps(steps);
0343: }
0344: ProofSettings.DEFAULT_SETTINGS.getStrategySettings()
0345: .setMaxSteps(steps);
0346: }
0347:
0348: /** returns the maximum number of rule applications allowed in
0349: * automatic mode
0350: * @return the maximum number of rule applications allowed in
0351: * automatic mode
0352: */
0353: public int getMaxAutomaticSteps() {
0354: if (proof != null) {
0355: return proof.getSettings().getStrategySettings()
0356: .getMaxSteps();
0357: } else {
0358: return ProofSettings.DEFAULT_SETTINGS.getStrategySettings()
0359: .getMaxSteps();
0360: }
0361: }
0362:
0363: public SetOfTacletApp getTacletApplications(Goal g, String name,
0364: PosInOccurrence p) {
0365: return interactiveProver.getAppsForName(g, name, p);
0366: }
0367:
0368: public SetOfTacletApp getTacletApplications(Goal goal, String name,
0369: PosInOccurrence pos, TacletFilter filter) {
0370: return interactiveProver
0371: .getAppsForName(goal, name, pos, filter);
0372: }
0373:
0374: /**
0375: * collects all applications of a rule given by its name at a give position in the sequent
0376: * @param name
0377: * the name of the BuiltInRule for which applications are collected.
0378: * @param pos
0379: * the position in the sequent where the BuiltInRule should be applied
0380: * @return
0381: * a SetOfRuleApp with all possible applications of the rule
0382: */
0383: public SetOfRuleApp getBuiltInRuleApplications(String name,
0384: PosInOccurrence pos) {
0385: return interactiveProver.getBuiltInRuleAppsForName(name, pos);
0386: }
0387:
0388: public ProverTaskListener getProverTaskListener() {
0389: return mainFrame.getProverTaskListener();
0390: }
0391:
0392: /**
0393: * selected rule to apply; opens a dialog
0394: * @param tacletApp the TacletApp which has been selected
0395: * @param pos the PosInSequent describes the position where to apply the
0396: * rule
0397: */
0398: public void selectedTaclet(TacletApp tacletApp, PosInSequent pos) {
0399: Goal goal = keySelectionModel.getSelectedGoal();
0400: Debug.assertTrue(goal != null);
0401: selectedTaclet(tacletApp.taclet(), goal, pos
0402: .getPosInOccurrence());
0403: }
0404:
0405: public boolean selectedTaclet(Taclet taclet, Goal goal,
0406: PosInOccurrence pos) {
0407: SetOfTacletApp applics = getTacletApplications(goal, taclet
0408: .name().toString(), pos);
0409: if (applics.size() == 0) {
0410: JOptionPane
0411: .showMessageDialog(mainFrame,
0412: "Taclet application failed." + "\n"
0413: + taclet.name(), "Bummer!",
0414: JOptionPane.ERROR_MESSAGE);
0415: return false;
0416: }
0417: IteratorOfTacletApp it = applics.iterator();
0418: if (applics.size() == 1) {
0419: TacletApp firstApp = it.next();
0420: if (!getProof().mgt().ruleApplicable(firstApp, goal)) {
0421: barfRuleNotApplicable(firstApp);
0422: return false;
0423: }
0424:
0425: boolean ifSeqInteraction = firstApp.taclet().ifSequent() != Sequent.EMPTY_SEQUENT;
0426: if (stupidMode && !firstApp.complete()) {
0427: ListOfTacletApp ifSeqCandidates = firstApp
0428: .findIfFormulaInstantiations(goal.sequent(),
0429: getServices(), getUserConstraint()
0430: .getConstraint());
0431:
0432: if (ifSeqCandidates.size() == 1) {
0433: ifSeqInteraction = false;
0434: firstApp = ifSeqCandidates.head();
0435: }
0436: TacletApp tmpApp = firstApp.tryToInstantiate(goal,
0437: getServices());
0438: if (tmpApp != null)
0439: firstApp = tmpApp;
0440:
0441: }
0442: if (ifSeqInteraction || !firstApp.complete()) {
0443: TacletMatchCompletionDialog.completeAndApplyApp(
0444: firstApp, goal, this );
0445: } else {
0446: applyInteractive(firstApp, goal);
0447: }
0448: } else if (applics.size() > 1) {
0449: java.util.List appList = new java.util.LinkedList();
0450: TacletApp rapp = null;
0451:
0452: for (int i = 0; i < applics.size(); i++) {
0453: rapp = it.next();
0454: if (getProof().mgt().ruleApplicable(rapp, goal)) {
0455: appList.add(rapp);
0456: }
0457: }
0458:
0459: if (appList.size() == 0) {
0460: barfRuleNotApplicable(rapp);
0461: return false;
0462: }
0463:
0464: TacletMatchCompletionDialog.completeAndApplyApp(appList,
0465: goal, this );
0466:
0467: }
0468: return true;
0469: }
0470:
0471: private void barfRuleNotApplicable(RuleApp rapp) {
0472: JOptionPane.showMessageDialog(mainFrame, "Rule not applicable."
0473: + "\n" + rapp.rule().name() + "\n"
0474: + getProof().mgt().getLastAnalysisInfo(),
0475: "Correctness Management", JOptionPane.ERROR_MESSAGE);
0476: }
0477:
0478: /** selected rule to apply
0479: * @param rule the selected built-in rule
0480: * @param pos the PosInSequent describes the position where to apply the
0481: * rule
0482: */
0483: public void selectedBuiltInRule(BuiltInRule rule,
0484: PosInOccurrence pos) {
0485: Goal goal = keySelectionModel.getSelectedGoal();
0486: assert goal != null;
0487:
0488: SetOfRuleApp set = interactiveProver.getBuiltInRuleApp(rule,
0489: pos, getUserConstraint().getConstraint());
0490: if (set.size() > 1) {
0491: System.err
0492: .println("keymediator:: Expected a single app. If "
0493: + "it is OK that there are more than one "
0494: + "built-in rule apps. You have to add a "
0495: + "selection dialog here");
0496: System.err.println("keymediator:: Ambigous applications, "
0497: + "taking the first in list.");
0498: }
0499:
0500: RuleApp app = set.iterator().next();
0501: if (app != null && app.rule() == rule) {
0502: goal.apply(app);
0503: return;
0504: }
0505: }
0506:
0507: /** selected rule to apply
0508: * @param rule the selected built-in rule
0509: * @param pos the PosInSequent describes the position where to apply the
0510: * rule
0511: */
0512: public boolean selectedUseMethodContractRule(
0513: MethodContractRuleApp app) {
0514: Goal goal = keySelectionModel.getSelectedGoal();
0515: Debug.assertTrue(goal != null);
0516: if (!getProof().mgt().ruleApplicable(app, goal)) {
0517: barfRuleNotApplicable(app);
0518: return false;
0519: }
0520: applyInteractive(app, goal);
0521: return true;
0522: }
0523:
0524: /**
0525: * Apply a RuleApp and continue with update simplification or strategy
0526: * application according to current settings.
0527: * @param app
0528: * @param goal
0529: */
0530: public void applyInteractive(RuleApp app, Goal goal) {
0531: interactiveProver.applyInteractive(app, goal);
0532: }
0533:
0534: // ****************** Re-Use Stuff *********************************
0535:
0536: private ReuseListener hook = new ReuseListenerDummy();
0537: private boolean continuousReuse = true;
0538: private boolean reuseStarted = false;
0539:
0540: public void showReuseState() {
0541: hook.startShowingState();
0542: }
0543:
0544: public void showPreImage() {
0545: hook.showPreImage();
0546: }
0547:
0548: public void mark(Node n) {
0549: if (hook instanceof ReuseListenerDummy) {
0550: hook = new ReuseListenerImpl(this );
0551: addKeYSelectionListener(hook);
0552: }
0553: if (n.isReuseCandidate()) {
0554: n.unmarkReuseCandidate();
0555: hook.recomputeReuseTotal();
0556: } else {
0557: n.markReuseCandidate();
0558: }
0559: }
0560:
0561: public ReuseListener getReuseListener() {
0562: return hook;
0563: }
0564:
0565: public void markPersistent(Node n) {
0566: mark(n);
0567: n.markPersistentCandidate();
0568: }
0569:
0570: public void setContinuousReuse(boolean b) {
0571: continuousReuse = b;
0572: }
0573:
0574: public boolean reuseInProgress() {
0575: return continuousReuse && reuseStarted;
0576: }
0577:
0578: private ActionListener reuseAction;
0579:
0580: public void indicateNoReuse() {
0581: final JButton b = mainFrame.reuseButton;
0582: b.setEnabled(false);
0583: b.removeActionListener(reuseAction);
0584: reuseStarted = false;
0585: }
0586:
0587: public void indicateReuse(ReusePoint p) {
0588: final ReusePoint rp = p;
0589: final JButton b = mainFrame.reuseButton;
0590: b.removeActionListener(reuseAction);
0591: b.setToolTipText(rp.toString());
0592: b.setEnabled(true);
0593: reuseAction = new ActionListener() {
0594: ReusePoint reusePoint = rp;
0595:
0596: public void actionPerformed(ActionEvent e) {
0597: b.setEnabled(false);
0598: b.removeActionListener(this );
0599: b.setToolTipText(null);
0600: reuseStarted = true;
0601: getInteractiveProver().fireAutoModeStarted(
0602: new ProofEvent(getProof()));
0603: try {
0604: do {
0605: Goal currGoal = reusePoint.target(); // check proof!!!
0606: assert currGoal != null : "Cannot apply this here. Forgot to unregister listener?";
0607: hook
0608: .removeRPConsumedMarker(reusePoint
0609: .source());
0610: RuleApp app = reusePoint.getReuseApp();
0611: // if (app.complete()) {
0612: // if (currGoal.node().serialNr()!=12) {
0613: // if (true) {
0614: if (reusePoint.source() != changeWish) {
0615: currGoal.node().setReuseSource(reusePoint);
0616: hook.removeRPConsumedGoal(currGoal);
0617: ListOfGoal goalList = currGoal.apply(app);
0618: hook.addRPOldMarkersNewGoals(goalList);
0619: hook.addRPNewMarkersAllGoals(reusePoint
0620: .source());
0621: reuseStarted = hook.reusePossible();
0622: } else {
0623: // InteractiveProver will do the other 2 bookkeeping
0624: reuseStarted = false;
0625: // TacletMatchCompletionDialog.completeAndApplyApp(
0626: // (TacletApp)app, currGoal, KeYMediator.this);
0627: changeWish = null;
0628: hook.addRPNewMarkersAllGoals(reusePoint
0629: .source());
0630: }
0631: hook.showState();
0632: if (reuseStarted) {
0633: reusePoint = hook.getBestReusePoint();
0634: if (!continuousReuse) {
0635: b.setEnabled(true);
0636: b.addActionListener(this );
0637: b.setToolTipText(reusePoint.toString());
0638: }
0639: } else
0640: indicateNoReuse();
0641: } while (reuseInProgress());
0642: } catch (RuntimeException re) {
0643: getInteractiveProver().fireAutoModeStopped(
0644: new ProofEvent(getProof()));
0645: throw re;
0646: }
0647: getInteractiveProver().fireAutoModeStopped(
0648: new ProofEvent(getProof()));
0649: }
0650: };
0651: b.addActionListener(reuseAction);
0652: }
0653:
0654: private Node changeWish;
0655:
0656: public void changeNode(Node n) {
0657: Proof old = n.proof();
0658: Proof p = new Proof(old);
0659: mark(old.root());
0660:
0661: p.setProofEnv(old.env());
0662: mainFrame.addProblem(new SingleProof(p, "XXX"));
0663: changeWish = n;
0664: }
0665:
0666: // **********************************************************************
0667:
0668: /** collects all applicable FindTaclets of the current goal
0669: * (called by the SequentViewer)
0670: * @return a list of Taclets with all applicable FindTaclets
0671: */
0672:
0673: public ListOfTacletApp getFindTaclet(PosInSequent pos) {
0674: return interactiveProver.getFindTaclet(pos);
0675: }
0676:
0677: /** collects all applicable RewriteTaclets of the current goal
0678: * (called by the SequentViewer)
0679: * @return a list of Taclets with all applicable RewriteTaclets
0680: */
0681: public ListOfTacletApp getRewriteTaclet(PosInSequent pos) {
0682: return interactiveProver.getRewriteTaclet(pos);
0683: }
0684:
0685: /** collects all applicable NoFindTaclets of the current goal
0686: * (called by the SequentViewer)
0687: * @return a list of Taclets with all applicable NoFindTaclets
0688: */
0689: public ListOfTacletApp getNoFindTaclet() {
0690: return interactiveProver.getNoFindTaclet();
0691: }
0692:
0693: /** collects all built-in rules
0694: * @return a list of all applicable built-in rules
0695: */
0696: public ListOfBuiltInRule getBuiltInRule(PosInOccurrence pos) {
0697: return interactiveProver.getBuiltInRule(pos,
0698: getUserConstraint().getConstraint());
0699: }
0700:
0701: /** adds a listener to the KeYSelectionModel, so that the listener
0702: * will be informed if the proof or node the user has selected
0703: * changed
0704: * @param listener the KeYSelectionListener to add
0705: */
0706: public synchronized void addKeYSelectionListener(
0707: KeYSelectionListener listener) {
0708: keySelectionModel.addKeYSelectionListener(listener);
0709: }
0710:
0711: /** removes a listener from the KeYSelectionModel
0712: * @param listener the KeYSelectionListener to be removed
0713: */
0714: public synchronized void removeKeYSelectionListener(
0715: KeYSelectionListener listener) {
0716: keySelectionModel.removeKeYSelectionListener(listener);
0717: }
0718:
0719: /** adds a listener to GUI events
0720: * @param listener the GUIListener to be added
0721: */
0722: public void addGUIListener(GUIListener listener) {
0723: listenerList.add(GUIListener.class, listener);
0724: }
0725:
0726: /** adds a listener to GUI events
0727: * @param listener the GUIListener to be added
0728: */
0729: public void removeGUIListener(GUIListener listener) {
0730: listenerList.remove(GUIListener.class, listener);
0731: }
0732:
0733: public void addRuleAppListener(RuleAppListener listener) {
0734: Goal.addRuleAppListener(listener);
0735: }
0736:
0737: public void removeRuleAppListener(RuleAppListener listener) {
0738: Goal.removeRuleAppListener(listener);
0739: }
0740:
0741: public void addAutoModeListener(AutoModeListener listener) {
0742: interactiveProver.addAutoModeListener(listener);
0743: }
0744:
0745: public void removeAutoModeListener(AutoModeListener listener) {
0746: interactiveProver.addAutoModeListener(listener);
0747: }
0748:
0749: /** sets the current goal
0750: * @param goal the Goal being displayed in the view of the sequent
0751: */
0752: public void goalChosen(Goal goal) {
0753: keySelectionModel.setSelectedGoal(goal);
0754: }
0755:
0756: /** returns the main frame
0757: * @return the main frame
0758: */
0759: public JFrame mainFrame() {
0760: return mainFrame;
0761: }
0762:
0763: /** notifies that a node that is not a goal has been chosen
0764: * @param node the node being displayed in the view of the sequent
0765: */
0766: public void nonGoalNodeChosen(Node node) {
0767: keySelectionModel.setSelectedNode(node);
0768: }
0769:
0770: /** called to ask for modal access
0771: * @param src Object that is the asking component
0772: */
0773: public synchronized void requestModalAccess(Object src) {
0774: fireModalDialogOpened(new GUIEvent(src));
0775: }
0776:
0777: /** called if no more modal access is needed
0778: * @param src Object that is the asking component
0779: */
0780: public synchronized void freeModalAccess(Object src) {
0781: fireModalDialogClosed(new GUIEvent(src));
0782: }
0783:
0784: /** fires the request of a GUI component for modal access
0785: * this can be used to disable all views even if the GUI component
0786: * has no built in modal support
0787: */
0788: public synchronized void fireModalDialogOpened(GUIEvent e) {
0789: Object[] listeners = listenerList.getListenerList();
0790: for (int i = listeners.length - 2; i >= 0; i -= 2) {
0791: if (listeners[i] == GUIListener.class) {
0792: ((GUIListener) listeners[i + 1]).modalDialogOpened(e);
0793: }
0794: }
0795: }
0796:
0797: /** fires that a GUI component that has asked for modal access
0798: * has been closed, so views can be enabled again
0799: */
0800: public synchronized void fireModalDialogClosed(GUIEvent e) {
0801: Object[] listeners = listenerList.getListenerList();
0802: for (int i = listeners.length - 2; i >= 0; i -= 2) {
0803: if (listeners[i] == GUIListener.class) {
0804: ((GUIListener) listeners[i + 1]).modalDialogClosed(e);
0805: }
0806: }
0807: }
0808:
0809: /** Fires the shut down event.
0810: */
0811: public synchronized void fireShutDown(GUIEvent e) {
0812: Object[] listeners = listenerList.getListenerList();
0813: for (int i = listeners.length - 2; i >= 0; i -= 2) {
0814: if (listeners[i] == GUIListener.class) {
0815: ((GUIListener) listeners[i + 1]).shutDown(e);
0816: }
0817: }
0818: }
0819:
0820: /** sets the simultaneous update simplifier */
0821: public void setSimplifier(UpdateSimplifier s) {
0822: upd_simplifier = s;
0823: if (proof != null)
0824: proof.setSimplifier(s);
0825: }
0826:
0827: /** returns the current selected proof
0828: * @return the current selected proof
0829: */
0830: public Proof getSelectedProof() {
0831: return keySelectionModel.getSelectedProof();
0832: }
0833:
0834: /** returns the current selected goal
0835: * @return the current selected goal
0836: */
0837: public Goal getSelectedGoal() {
0838: return keySelectionModel.getSelectedGoal();
0839: }
0840:
0841: /** returns the current selected goal
0842: * @return the current selected goal
0843: */
0844: public KeYSelectionModel getSelectionModel() {
0845: return keySelectionModel;
0846: }
0847:
0848: /** returns the current selected node
0849: * @return the current selected node
0850: */
0851: public Node getSelectedNode() {
0852: return keySelectionModel.getSelectedNode();
0853: }
0854:
0855: /**
0856: * Start automatic application of rules on open goals.
0857: */
0858: public void startAutoMode() {
0859: if (ensureProofLoaded()) {
0860: startAutoMode(proof.openGoals());
0861: }
0862: }
0863:
0864: /**
0865: * Start automatic application of rules on specified goals.
0866: * @param goals
0867: */
0868: public void startAutoMode(ListOfGoal goals) {
0869: interactiveProver.startAutoMode(goals);
0870: }
0871:
0872: /**
0873: * Stop automatic application of rules.
0874: */
0875: public void stopAutoMode() {
0876: interactiveProver.stopAutoMode();
0877: }
0878:
0879: public void setResumeAutoMode(boolean b) {
0880: interactiveProver.setResumeAutoMode(b);
0881: }
0882:
0883: /**
0884: * Switches interactive mode on or off.
0885: * @param b true iff interactive mode is to be turned on
0886: */
0887: public void setInteractive(boolean b) {
0888: interactiveProver.setInteractive(b);
0889: if (proof != null) {
0890: if (b) {
0891: proof.setRuleAppIndexToInteractiveMode();
0892: } else {
0893: proof.setRuleAppIndexToAutoMode();
0894: }
0895: }
0896: }
0897:
0898: public void popupInformationMessage(Object message, String title) {
0899: JOptionPane.showMessageDialog(mainFrame, message, title,
0900: JOptionPane.INFORMATION_MESSAGE);
0901: }
0902:
0903: public void popupWarning(Object message, String title) {
0904: JOptionPane.showMessageDialog(mainFrame, message, title,
0905: JOptionPane.WARNING_MESSAGE);
0906: }
0907:
0908: /**
0909: * Brings up a dialog displaying a message.
0910: * @param modal whether or not the message should be displayed in a modal dialog.
0911: */
0912: public void popupInformationMessage(Object message, String title,
0913: boolean modal) {
0914: if (modal) {
0915: popupInformationMessage(message, title);
0916: } else {
0917: if (!(message instanceof Component))
0918: throw new InternalError("only messages of type "
0919: + Component.class + " supported, yet");
0920: // JFrame dlg = new JDialog(mainFrame(),title, modal);
0921: JFrame dlg = new JFrame(title);
0922: dlg.setDefaultCloseOperation(JDialog.DISPOSE_ON_CLOSE);
0923: dlg.getContentPane().add((Component) message);
0924: dlg.pack();
0925: setCenter(dlg, mainFrame());
0926: dlg.setVisible(true);
0927: }
0928: }
0929:
0930: /**
0931: * Center a component within a parental component.
0932: * @param comp the component to be centered.
0933: * @param parent center relative to what. <code>null</code> to center relative to screen.
0934: * @see #setCenter(Component)
0935: */
0936: public static void setCenter(Component comp, Component parent) {
0937: if (parent == null) {
0938: setCenter(comp);
0939: return;
0940: }
0941: Dimension dlgSize = comp.getPreferredSize();
0942: Dimension frmSize = parent.getSize();
0943: Point loc = parent.getLocation();
0944: if (dlgSize.width < frmSize.width
0945: && dlgSize.height < frmSize.height)
0946: comp.setLocation((frmSize.width - dlgSize.width) / 2
0947: + loc.x, (frmSize.height - dlgSize.height) / 2
0948: + loc.y);
0949: else
0950: setCenter(comp);
0951: }
0952:
0953: /**
0954: * Center a component on the screen.
0955: * @param comp the component to be centered relative to the screen.
0956: * It must already have its final size set.
0957: * @preconditions comp.getSize() as on screen.
0958: */
0959: public static void setCenter(Component comp) {
0960: Dimension screenSize = comp.getToolkit().getScreenSize();
0961: Dimension frameSize = comp.getSize();
0962: if (frameSize.height > screenSize.height)
0963: frameSize.height = screenSize.height;
0964: if (frameSize.width > screenSize.width)
0965: frameSize.width = screenSize.width;
0966: comp.setLocation((screenSize.width - frameSize.width) / 2,
0967: (screenSize.height - frameSize.height) / 2);
0968: }
0969:
0970: private int goalsClosedByAutoMode = 0;
0971:
0972: private Profile profile;
0973:
0974: public void closedAGoal() {
0975: goalsClosedByAutoMode++;
0976: }
0977:
0978: public int getNrGoalsClosedByAutoMode() {
0979: return goalsClosedByAutoMode;
0980: }
0981:
0982: public void resetNrGoalsClosedByHeuristics() {
0983: goalsClosedByAutoMode = 0;
0984: }
0985:
0986: public void stopInterface(boolean fullStop) {
0987: final boolean b = fullStop;
0988: Runnable interfaceSignaller = new Runnable() {
0989: public void run() {
0990: mainFrame.setCursor(new java.awt.Cursor(
0991: java.awt.Cursor.WAIT_CURSOR));
0992: if (b) {
0993: interactiveProver
0994: .fireAutoModeStarted(new ProofEvent(
0995: getProof()));
0996: }
0997: }
0998: };
0999: invokeAndWait(interfaceSignaller);
1000: }
1001:
1002: public void startInterface(boolean fullStop) {
1003: final boolean b = fullStop;
1004: Runnable interfaceSignaller = new Runnable() {
1005: public void run() {
1006: if (b)
1007: interactiveProver
1008: .fireAutoModeStopped(new ProofEvent(
1009: getProof()));
1010: mainFrame.setCursor(new java.awt.Cursor(
1011: java.awt.Cursor.DEFAULT_CURSOR));
1012: if (getProof() != null)
1013: keySelectionModel.fireSelectedProofChanged();
1014: }
1015: };
1016: invokeAndWait(interfaceSignaller);
1017: }
1018:
1019: public static void invokeAndWait(Runnable runner) {
1020: if (SwingUtilities.isEventDispatchThread())
1021: runner.run();
1022: else {
1023: try {
1024: SwingUtilities.invokeAndWait(runner);
1025: } catch (InterruptedException e) {
1026: System.err.println(e);
1027: e.printStackTrace();
1028: } catch (java.lang.reflect.InvocationTargetException ite) {
1029: Throwable targetExc = ite.getTargetException();
1030: System.err.println(targetExc);
1031: targetExc.printStackTrace();
1032: ite.printStackTrace();
1033: }
1034: }
1035: }
1036:
1037: public boolean autoMode() {
1038: return autoMode;
1039: }
1040:
1041: class KeYMediatorProofTreeListener extends ProofTreeAdapter {
1042: public void proofClosed(ProofTreeEvent e) {
1043: closedAGoal();
1044: KeYMediator.this .notify(new ProofClosedNotificationEvent(e
1045: .getSource()));
1046: }
1047:
1048: public void proofPruned(ProofTreeEvent e) {
1049: final ProofTreeRemovedNodeEvent ev = (ProofTreeRemovedNodeEvent) e;
1050: if (ev.getRemovedNode() == getSelectedNode()) {
1051: SwingUtilities.invokeLater(new Runnable() {
1052: public void run() {
1053: keySelectionModel.setSelectedNode(ev.getNode());
1054: }
1055: });
1056: }
1057: }
1058:
1059: public void proofGoalsAdded(ProofTreeEvent e) {
1060: ListOfGoal newGoals = e.getGoals();
1061: // Check for a closed goal ...
1062: if (newGoals.size() == 0) {
1063: // No new goals have been generated ...
1064: closedAGoal();
1065: }
1066: }
1067:
1068: public void proofStructureChanged(ProofTreeEvent e) {
1069: Proof p = e.getSource();
1070: if (p == getSelectedProof()) {
1071: Node sel_node = getSelectedNode();
1072: if (!(p.find(sel_node))) {
1073: keySelectionModel.defaultSelection();
1074: } else {
1075: // %%% hack does need to be done proper
1076: // needed top update that the selected node nay have
1077: // changed its status
1078: keySelectionModel.setSelectedNode(sel_node);
1079: }
1080: }
1081: }
1082: }
1083:
1084: //INNER CLASS
1085: class KeYMediatorProofListener implements RuleAppListener,
1086: AutoModeListener {
1087:
1088: private Node selectedBeforeAutoMode;
1089:
1090: /** invoked when a rule has been applied */
1091: public void ruleApplied(ProofEvent e) {
1092: keySelectionModel.defaultSelection();
1093: }
1094:
1095: /** invoked if automatic execution has started
1096: */
1097: public void autoModeStarted(ProofEvent e) {
1098: autoMode = true;
1099: selectedBeforeAutoMode = getSelectedNode();
1100: // if (proof == null) return; // there is no selection or anything
1101: }
1102:
1103: /** invoked if automatic execution has stopped
1104: */
1105: public void autoModeStopped(ProofEvent e) {
1106: autoMode = false;
1107: if (proof == null)
1108: return; // there is no selection or anything
1109: if (selectedBeforeAutoMode != null) {
1110: //XXX%%%%% This is way too slow for big proofs!
1111: // XXX Could you please check if it is still to slow?
1112: keySelectionModel
1113: .nearestOpenGoalSelection(selectedBeforeAutoMode);
1114: } else {
1115: keySelectionModel.defaultSelection();
1116: }
1117: }
1118: }
1119:
1120: class KeYMediatorSelectionListener implements KeYSelectionListener {
1121: /** focused node has changed */
1122: public void selectedNodeChanged(KeYSelectionEvent e) {
1123: // empty
1124: }
1125:
1126: /** the selected proof has changed (e.g. a new proof has been
1127: * loaded)
1128: */
1129: public void selectedProofChanged(KeYSelectionEvent e) {
1130: setProof(e.getSource().getSelectedProof());
1131: //should be obsolete...
1132: //ProofSettings.DEFAULT_SETTINGS.setLDTSettings(proof.getLDTSettings());
1133: }
1134:
1135: }
1136:
1137: /**
1138: * takes a notification event and informs the notification
1139: * manager
1140: * @param event the NotificationEvent
1141: */
1142: public void notify(NotificationEvent event) {
1143: if (mainFrame != null) {
1144: mainFrame.notify(event);
1145: }
1146: }
1147:
1148: /** return the chosen profile */
1149: public Profile getProfile() {
1150: if (profile == null) {
1151: profile = ProofSettings.DEFAULT_SETTINGS.getProfile();
1152: if (profile == null) {
1153: profile = new JavaProfile((Main) this .mainFrame());
1154: }
1155: }
1156: return profile;
1157: }
1158:
1159: /**
1160: * besides the number of rule applications it is possible to define a timeout after which rule application
1161: * shall be terminated
1162: * @return the time in ms after which automatic rule application stops
1163: */
1164: public long getAutomaticApplicationTimeout() {
1165: if (proof != null) {
1166: return getProof().getSettings().getStrategySettings()
1167: .getTimeout();
1168: } else {
1169: return ProofSettings.DEFAULT_SETTINGS.getStrategySettings()
1170: .getTimeout();
1171: }
1172: }
1173:
1174: /**
1175: * sets the time out after which automatic rule application stops
1176: * @param timeout a long specifying the timeout time in ms
1177: */
1178: public void setAutomaticApplicationTimeout(long timeout) {
1179: if (proof != null) {
1180: proof.getSettings().getStrategySettings().setTimeout(
1181: timeout);
1182: }
1183: ProofSettings.DEFAULT_SETTINGS.getStrategySettings()
1184: .setTimeout(timeout);
1185: }
1186: }
|