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: // This file is part of KeY - Integrated Deductive Software Design
0009: // Copyright (C) 2001-2005 Universitaet Karlsruhe, Germany
0010: // Universitaet Koblenz-Landau, Germany
0011: // Chalmers University of Technology, Sweden
0012: //
0013: // The KeY system is protected by the GNU General Public License.
0014: // See LICENSE.TXT for details.
0015: //
0016: //
0017:
0018: package de.uka.ilkd.key.gui;
0019:
0020: import java.awt.*;
0021: import java.awt.Dimension;
0022: import java.awt.event.*;
0023: import java.io.*;
0024: import java.net.URL;
0025: import java.util.*;
0026:
0027: import javax.swing.*;
0028: import javax.swing.border.TitledBorder;
0029: import javax.swing.event.*;
0030: import javax.swing.text.JTextComponent;
0031:
0032: import org.apache.log4j.Logger;
0033:
0034: import de.uka.ilkd.key.gui.assistant.*;
0035: import de.uka.ilkd.key.gui.configuration.*;
0036: import de.uka.ilkd.key.gui.nodeviews.NonGoalInfoView;
0037: import de.uka.ilkd.key.gui.nodeviews.SequentView;
0038: import de.uka.ilkd.key.gui.notification.NotificationManager;
0039: import de.uka.ilkd.key.gui.notification.events.*;
0040: import de.uka.ilkd.key.gui.prooftree.ProofTreeView;
0041: import de.uka.ilkd.key.java.*;
0042: import de.uka.ilkd.key.logic.Sequent;
0043: import de.uka.ilkd.key.logic.Term;
0044: import de.uka.ilkd.key.pp.*;
0045: import de.uka.ilkd.key.proof.*;
0046: import de.uka.ilkd.key.proof.decproc.DecProcRunner;
0047: import de.uka.ilkd.key.proof.decproc.DecisionProcedureSmtAuflia;
0048: import de.uka.ilkd.key.proof.init.*;
0049: import de.uka.ilkd.key.proof.mgt.*;
0050: import de.uka.ilkd.key.unittest.ModelGenerator;
0051: import de.uka.ilkd.key.unittest.UnitTestBuilder;
0052: import de.uka.ilkd.key.util.*;
0053: import de.uka.ilkd.key.util.ProgressMonitor;
0054:
0055: public class Main extends JFrame {
0056:
0057: public static final String INTERNAL_VERSION = KeYResourceManager
0058: .getManager().getSHA1();
0059:
0060: private static final String VERSION = KeYResourceManager
0061: .getManager().getVersion()
0062: + "(internal: " + INTERNAL_VERSION + ")";
0063: private static final String COPYRIGHT = "(C) Copyright 2001-2007 "
0064: + "Universit\u00e4t Karlsruhe, Universit\u00e4t Koblenz-Landau, "
0065: + "and Chalmers University of Technology";
0066:
0067: /**
0068: * The maximum number of recent files displayed.
0069: */
0070: private static final int MAX_RECENT_FILES = 8;
0071:
0072: /** Name of the config file controlling logging with log4j */
0073: private static final String LOGGER_CONFIGURATION = PathConfig.KEY_CONFIG_DIR
0074: + File.separator + "logger.props";
0075:
0076: static {
0077: // @xxx preliminary: better store along with other settings.
0078: PresentationFeatures.ENABLED = true;
0079: }
0080:
0081: /** the tab bar at the left */
0082: private JTabbedPane tabbedPane;
0083:
0084: /** the toolbar */
0085: private JToolBar toolBar;
0086:
0087: /** the current goal view */
0088: private JScrollPane goalView;
0089:
0090: /** the current proof tree*/
0091: private JPanel proofView;
0092:
0093: /** the list of current open goals*/
0094: private JScrollPane openGoalsView;
0095:
0096: /** the view of a sequent */
0097: private SequentView sequentView;
0098:
0099: /** the KeY test generator GUI*/
0100: private UnitTestGeneratorGui unitKeY;
0101:
0102: /** the user constraint view */
0103: private UserConstraintView userConstraintView = null;
0104:
0105: /** the rule view */
0106: private RuleView ruleView = null;
0107:
0108: /** the strategy selection view */
0109: private StrategySelectionView strategySelectionView = null;
0110:
0111: /** the current user constraint */
0112: private ConstraintTableModel userConstraint = null;
0113:
0114: /** contains a list of all proofs */
0115: private JScrollPane proofListView;
0116:
0117: private TaskTree proofList;
0118:
0119: /** list of open goals of the current proof */
0120: private GoalList goalList;
0121:
0122: /** the mediator is stored here */
0123: protected KeYMediator mediator;
0124:
0125: /** the status line */
0126: MainStatusLine statusLine;
0127:
0128: /** the main progress monitor */
0129: protected ProgressMonitor progressMonitor = new MainProgressMonitor();
0130:
0131: /** listener to global proof events */
0132: private MainProofListener proofListener;
0133:
0134: /** listener to gui events */
0135: private MainGUIListener guiListener;
0136: private RecentFileMenu recentFiles;
0137:
0138: private boolean frozen = false;
0139:
0140: /** listener to changes of the user constraint */
0141: private MainConstraintTableListener constraintListener;
0142:
0143: private static KeYFileChooser fileChooser = null;
0144:
0145: private static final String PARA =
0146:
0147: "<p style=\"font-family: lucida;font-size: 12pt;font-weight: bold\">";
0148:
0149: /** button for starting and stopping automatic mode */
0150: public static AutoModeAction autoModeAction;
0151:
0152: /** action for opening a KeY file */
0153: public static OpenFile openFileAction;
0154:
0155: /** action for saving a proof (attempt) */
0156: public static SaveFile saveFileAction;
0157:
0158: public static final String AUTO_MODE_TEXT = "Start/stop automated proof search";
0159:
0160: /** if true then automaticaly start startAutoMode after the key-file is loaded*/
0161:
0162: public static boolean batchMode = false;
0163:
0164: /** A push-button test generation view of KeY*/
0165: public static boolean testStandalone = false;
0166:
0167: /** Determines if the KeY prover is started in visible mode*/
0168: public static boolean visible = true;
0169:
0170: public static String statisticsFile = null;
0171:
0172: /** if true then the prover starts in
0173: * a unit test generation optimized mode.
0174: * ATTENTION: to be deleted (Puse profiles to customize
0175: * JML translation, TODO)
0176: * */
0177:
0178: public static boolean testMode = false;
0179:
0180: /** if false then JML specifications are not parsed (useful for .key input) */
0181: public static boolean jmlSpecs = true;
0182:
0183: public JButton reuseButton = new JButton("Reuse", IconFactory
0184: .reuseLogo());
0185:
0186: private JButton decisionProcedureButton;
0187:
0188: private JButton testButton;
0189:
0190: private JPopupMenu reusePopup = new JPopupMenu();
0191:
0192: protected static String fileNameOnStartUp = null;
0193:
0194: /** are we in stand-alone mode? (or with TCC?) */
0195: public static boolean standalone = System
0196: .getProperty("key.together") == null;
0197:
0198: /** for locking of threads waiting for the prover to exit */
0199: public Object monitor = new Object();
0200:
0201: private static final String TACLET_OPTIONS_MENU_STRING = "ToolTip options ";
0202:
0203: private Action createUnitTestAction = null;
0204:
0205: protected static Main instance = null;
0206:
0207: /** menu for configuration of decision procedure */
0208: JMenu decisionProcedureOption = new JMenu("Decision Procedures");
0209:
0210: JRadioButtonMenuItem simplifyButton = new JRadioButtonMenuItem(
0211: "Simplify", true);
0212:
0213: JRadioButtonMenuItem icsButton = new JRadioButtonMenuItem("ICS",
0214: false);
0215:
0216: JRadioButtonMenuItem cvcLiteButton = new JRadioButtonMenuItem(
0217: "CVCLite", false);
0218:
0219: JRadioButtonMenuItem cvc3Button = new JRadioButtonMenuItem("CVC3",
0220: false);
0221:
0222: JRadioButtonMenuItem svcButton = new JRadioButtonMenuItem("SVC",
0223: false);
0224:
0225: JRadioButtonMenuItem yicesButton = new JRadioButtonMenuItem(
0226: "Yices", false);
0227:
0228: JRadioButtonMenuItem smtButton = new JRadioButtonMenuItem(
0229: "SMT Translation", false);
0230:
0231: JMenuItem smtUseQuantifiersOption;
0232:
0233: JMenuItem smtBenchmarkArchivingOption;
0234:
0235: JMenuItem smtZipProblemDirOption;
0236:
0237: /** size of the tool bar icons */
0238: private int toolbarIconSize = 15;
0239:
0240: private ProverTaskListener taskListener;
0241:
0242: private NotificationManager notificationManager;
0243:
0244: /**
0245: * creates prover -- private, use getInstance()
0246: *
0247: * @param title
0248: * the String containing the frame's title
0249: */
0250: protected Main(String title) {
0251: super (title);
0252: setIconImage(IconFactory.keyLogo());
0253: setDefaultCloseOperation(WindowConstants.DO_NOTHING_ON_CLOSE);
0254: configureLogger();
0255: proofListener = new MainProofListener();
0256: guiListener = new MainGUIListener();
0257: constraintListener = new MainConstraintTableListener();
0258: taskListener = new MainTaskListener();
0259:
0260: setMediator(new KeYMediator(this ));
0261:
0262: initNotification();
0263: initProofList();
0264: layoutMain();
0265: initGoalList();
0266: initGUIProofTree();
0267:
0268: SwingUtilities.updateComponentTreeUI(this );
0269: ToolTipManager.sharedInstance().setDismissDelay(30000);
0270: setSize(1000, 750);
0271: addWindowListener(new MainListener());
0272:
0273: }
0274:
0275: private void initNotification() {
0276: if (!batchMode) {
0277: notificationManager = new NotificationManager(mediator);
0278: }
0279: }
0280:
0281: public static Main getInstance() {
0282: return getInstance(true);
0283: }
0284:
0285: public static Main getInstance(boolean visible) {
0286: if (instance == null) {
0287: instance = new Main("KeY -- Prover");
0288: }
0289: if (!instance.isVisible())
0290: instance.setVisible(visible); // XXX: enough?
0291: return instance;
0292: }
0293:
0294: public static void setStandalone(boolean b) {
0295: standalone = b;
0296: }
0297:
0298: public static void configureLogger() {
0299: if ((new File(LOGGER_CONFIGURATION)).exists())
0300: org.apache.log4j.PropertyConfigurator.configureAndWatch(
0301: LOGGER_CONFIGURATION, 1500);
0302: else {
0303: org.apache.log4j.BasicConfigurator.configure();
0304: Logger.getRootLogger().setLevel(
0305: org.apache.log4j.Level.ERROR);
0306: DecisionProcedureSmtAuflia
0307: .configureLogger(org.apache.log4j.Level.DEBUG); //Debugging of SMT Translation
0308: }
0309: }
0310:
0311: public String getPrcsVersion() {
0312: return INTERNAL_VERSION;
0313: }
0314:
0315: public void updateUI() {
0316: if (goalView != null)
0317: goalView.updateUI();
0318: if (proofView != null)
0319: proofView.updateUI();
0320: if (openGoalsView != null)
0321: openGoalsView.updateUI();
0322: if (userConstraintView != null)
0323: userConstraintView.updateUI();
0324: if (ruleView != null)
0325: ruleView.updateUI();
0326: if (proofListView != null)
0327: proofListView.updateUI();
0328: }
0329:
0330: /**
0331: * sets the mediator to corresspond with other gui elements
0332: *
0333: * @param m
0334: * the KeYMediator
0335: */
0336: private void setMediator(KeYMediator m) {
0337: if (mediator != null)
0338: unregister();
0339: mediator = m;
0340: mediator.setSimplifier(ProofSettings.DEFAULT_SETTINGS
0341: .getSimultaneousUpdateSimplifierSettings()
0342: .getSimplifier());
0343:
0344: // The following needs to be called before the SequentView
0345: // is created.
0346: Config.DEFAULT.setDefaultFonts();
0347: sequentView = new SequentView(mediator);
0348: register();
0349: }
0350:
0351: /** register several listeners */
0352: private void register() {
0353: mediator.addKeYSelectionListener(proofListener);
0354: mediator.addAutoModeListener(proofListener);
0355: mediator.addGUIListener(guiListener);
0356: }
0357:
0358: /** unregister several listeners */
0359: private void unregister() {
0360: mediator.removeKeYSelectionListener(proofListener);
0361: mediator.removeAutoModeListener(proofListener);
0362: mediator.removeGUIListener(guiListener);
0363: }
0364:
0365: /**
0366: * return the mediator
0367: *
0368: * @return the mediator
0369: */
0370: public KeYMediator mediator() {
0371: return instance.mediator;
0372: }
0373:
0374: public void setVisible(boolean v) {
0375: super .setVisible(v && visible);
0376: }
0377:
0378: /** paints empty view */
0379: private void paintEmptyViewComponent(JComponent pane, String name) {
0380: pane.setBorder(new TitledBorder(name));
0381: pane.setBackground(Color.white);
0382: if (pane instanceof JScrollPane) {
0383: ((JScrollPane) pane).getViewport().setBackground(
0384: Color.white);
0385: }
0386: pane.setMinimumSize(new java.awt.Dimension(150, 0));
0387: }
0388:
0389: /** adds a new tab */
0390: public void addTab(String tabname, JComponent view,
0391: String description) {
0392: tabbedPane.addTab(tabname, null, view, description);
0393: }
0394:
0395: /** sets the tool bar */
0396: private void setToolBar(JToolBar bar) {
0397: toolBar = bar;
0398: toolBar.setFloatable(true);
0399: toolBar.setRollover(true);
0400: }
0401:
0402: /** lays out the main frame */
0403: protected void layoutMain() {
0404: // set overall layout manager
0405: getContentPane().setLayout(new BorderLayout());
0406:
0407: // create empty components first
0408: setJMenuBar(new JMenuBar());
0409: setToolBar(new JToolBar("Proof Control"));
0410:
0411: autoModeAction = new AutoModeAction();
0412: openFileAction = new OpenFile();
0413: saveFileAction = new SaveFile();
0414: createUnitTestAction = new CreateUnitTestAction();
0415:
0416: // ============================================================
0417: // ================== create empty views =====================
0418: // ============================================================
0419:
0420: goalView = new JScrollPane();
0421: paintEmptyViewComponent(goalView, "Current Goal");
0422:
0423: proofView = new JPanel();
0424: proofView.setLayout(new BorderLayout(0, 0));
0425:
0426: paintEmptyViewComponent(proofView, "Proof");
0427:
0428: openGoalsView = new JScrollPane();
0429: paintEmptyViewComponent(openGoalsView, "Open Goals");
0430:
0431: userConstraintView = new UserConstraintView();
0432: if (mediator != null) {
0433: userConstraintView.setMediator(mediator);
0434: }
0435:
0436: strategySelectionView = new StrategySelectionView();
0437: if (mediator != null) {
0438: strategySelectionView.setMediator(mediator);
0439: }
0440:
0441: ruleView = new RuleView();
0442: if (mediator != null) {
0443: ruleView.setMediator(mediator);
0444: }
0445:
0446: // MENU BAR
0447: // ============================================================
0448: // ================== create menu bar entries ================
0449: // ============================================================
0450: createMenuBarEntries();
0451:
0452: // TOOL BAR SECTION
0453: // ============================================================
0454: // ==================== create tool bar entries ===============
0455: // ============================================================
0456:
0457: toolBar.add(createAutoModeButton());
0458: toolBar.addSeparator();
0459: toolBar.addSeparator();
0460: toolBar.addSeparator();
0461: toolBar.add(createDecisionProcedureButton());
0462: toolBar.addSeparator();
0463:
0464: JButton goalBackButton = new JButton("Goal Back");
0465: goalBackButton.setIcon(IconFactory
0466: .goalBackLogo(toolbarIconSize));
0467: goalBackButton.addActionListener(new ActionListener() {
0468: public void actionPerformed(ActionEvent e) {
0469: setBack();
0470: }
0471: });
0472:
0473: toolBar.add(goalBackButton);
0474: toolBar.addSeparator();
0475: toolBar.add(reuseButton);
0476:
0477: toolBar.addSeparator();
0478:
0479: if (mediator.getProfile() instanceof JavaTestGenerationProfile) {
0480: toolBar.add(createUnitTestButton());
0481: }
0482:
0483: reuseButton.setEnabled(false);
0484: reuseButton
0485: .setToolTipText("Start proof reuse (when template available)");
0486: JMenuItem singleStepReuse = new JCheckBoxMenuItem("Single step");
0487: singleStepReuse.setSelected(false);
0488: singleStepReuse.addActionListener(new ActionListener() {
0489: public void actionPerformed(ActionEvent e) {
0490: mediator.setContinuousReuse(!((JCheckBoxMenuItem) e
0491: .getSource()).isSelected());
0492: }
0493: });
0494: reusePopup.add(singleStepReuse);
0495: reuseButton.addMouseListener(new MouseAdapter() {
0496: public void mousePressed(MouseEvent e) {
0497: if (e.isPopupTrigger()) {
0498: reusePopup.show(e.getComponent(), e.getX(), e
0499: .getY());
0500: }
0501: }
0502: });
0503: toolBar.addSeparator();
0504:
0505: JToolBar fileOperations = new JToolBar("File Operations");
0506: fileOperations.add(createOpenFile());
0507: fileOperations.add(createOpenMostRecentFile());
0508: fileOperations.add(createSaveFile());
0509:
0510: goalView.getInputMap(JComponent.WHEN_IN_FOCUSED_WINDOW).put(
0511: KeyStroke.getKeyStroke(KeyEvent.VK_R,
0512: ActionEvent.CTRL_MASK), "show_reuse_state");
0513: goalView.getActionMap().put("show_reuse_state",
0514: new AbstractAction() {
0515: public void actionPerformed(ActionEvent e) {
0516: mediator().showReuseState();
0517: }
0518: });
0519:
0520: goalView.getInputMap(JComponent.WHEN_IN_FOCUSED_WINDOW).put(
0521: KeyStroke.getKeyStroke(KeyEvent.VK_SPACE,
0522: ActionEvent.ALT_MASK), "show_reuse_cntd");
0523: goalView.getActionMap().put("show_reuse_cntd",
0524: new AbstractAction() {
0525: public void actionPerformed(ActionEvent e) {
0526: mediator().showPreImage();
0527: }
0528: });
0529:
0530: goalView.getInputMap(JComponent.WHEN_IN_FOCUSED_WINDOW).put(
0531: KeyStroke.getKeyStroke(KeyEvent.VK_C,
0532: ActionEvent.CTRL_MASK), "copy");
0533: goalView.getActionMap().put("copy", new AbstractAction() {
0534: public void actionPerformed(ActionEvent e) {
0535: copyHighlightToClipboard(sequentView);
0536: }
0537: });
0538:
0539: JPanel toolBarPanel = new JPanel();
0540: toolBarPanel.setLayout(new FlowLayout(FlowLayout.LEADING));
0541: toolBarPanel.add(toolBar);
0542: toolBarPanel.add(fileOperations);
0543:
0544: getContentPane()
0545: .add(clipBoardTextArea, BorderLayout.PAGE_START);
0546: getContentPane().add(toolBarPanel, BorderLayout.PAGE_START);
0547:
0548: // ============================================================
0549: // ==================== create tabbed pane ====================
0550: // ============================================================
0551:
0552: tabbedPane = new JTabbedPane();
0553:
0554: addTab("Proof", proofView, "The current state of the "
0555: + "proof as tree");
0556:
0557: addTab("Goals", openGoalsView, "The currently open goals");
0558:
0559: tabbedPane.addTab("User Constraint", null, userConstraintView,
0560: "Currently chosen metavariable instantiations");
0561:
0562: tabbedPane.addTab("Proof Search Strategy", null,
0563: strategySelectionView,
0564: "Select strategy for automated proof search");
0565:
0566: tabbedPane.addTab("Rules", null, new JScrollPane(ruleView),
0567: "All available rules");
0568: tabbedPane.setSelectedIndex(0);
0569: tabbedPane.setPreferredSize(new java.awt.Dimension(250, 440));
0570: tabbedPane.getInputMap(
0571: JComponent.WHEN_ANCESTOR_OF_FOCUSED_COMPONENT)
0572: .getParent().remove(
0573: KeyStroke.getKeyStroke(KeyEvent.VK_UP,
0574: ActionEvent.CTRL_MASK));
0575: tabbedPane.getInputMap(JComponent.WHEN_FOCUSED).getParent()
0576: .remove(
0577: KeyStroke.getKeyStroke(KeyEvent.VK_DOWN,
0578: ActionEvent.CTRL_MASK));
0579:
0580: proofListView
0581: .setPreferredSize(new java.awt.Dimension(250, 100));
0582: paintEmptyViewComponent(proofListView, "Tasks");
0583:
0584: JSplitPane leftPane = new JSplitPane(JSplitPane.VERTICAL_SPLIT,
0585: proofListView, tabbedPane) {
0586: public void setUI(javax.swing.plaf.SplitPaneUI ui) {
0587: try {
0588: super .setUI(ui);
0589: } catch (NullPointerException e) {
0590: Debug
0591: .out("Exception thrown by class Main at setUI");
0592: }
0593: }
0594: }; // work around bug in
0595: // com.togethersoft.util.ui.plaf.metal.OIMetalSplitPaneUI
0596:
0597: leftPane.setOneTouchExpandable(true);
0598:
0599: JSplitPane splitPane = new JSplitPane(
0600: JSplitPane.HORIZONTAL_SPLIT, leftPane, goalView) {
0601: public void setUI(javax.swing.plaf.SplitPaneUI ui) {
0602: try {
0603: super .setUI(ui);
0604: } catch (NullPointerException e) {
0605: Debug
0606: .out("Exception thrown by class Main at setUI");
0607: }
0608: }
0609: }; // work around bug in
0610: // com.togethersoft.util.ui.plaf.metal.OIMetalSplitPaneUI
0611: splitPane.setResizeWeight(0); // the right pane is more important
0612: splitPane.setOneTouchExpandable(true);
0613: getContentPane().add(splitPane, BorderLayout.CENTER);
0614:
0615: statusLine = new MainStatusLine(
0616: "<html>"
0617: + PARA
0618: + COPYRIGHT
0619: + PARA
0620: + "KeY is free software and comes with ABSOLUTELY NO WARRANTY."
0621: + " See Help | License.", getFont());
0622: getContentPane().add(statusLine, BorderLayout.SOUTH);
0623: setupInternalInspection();
0624: }
0625:
0626: /**
0627: * *********************** UGLY INSPECTION CODE **********************
0628: */
0629: private void setupInternalInspection() {
0630: goalView.getInputMap(JComponent.WHEN_IN_FOCUSED_WINDOW).put(
0631: KeyStroke.getKeyStroke(KeyEvent.VK_Z,
0632: ActionEvent.CTRL_MASK), "show_tree");
0633: goalView.getActionMap().put("show_tree", new AbstractAction() {
0634:
0635: public void actionPerformed(ActionEvent e) {
0636: System.err.println(sequentView.getMousePosInSequent()
0637: .getPosInOccurrence().posInTerm());
0638:
0639: Term t = sequentView.getMousePosInSequent()
0640: .getPosInOccurrence().subTerm();
0641: System.err.println("****************** "
0642: + t.op().getClass());
0643: System.err.println(t.hashCode());
0644: t.tree();
0645:
0646: // if (t instanceof ProgramTerm) {
0647: de.uka.ilkd.key.java.visitor.JavaASTWalker w = new de.uka.ilkd.key.java.visitor.JavaASTWalker(
0648: t.javaBlock().program()) {
0649: protected void walk(ProgramElement node) {
0650: if (node != root())
0651: doAction(node);
0652: if (node instanceof NonTerminalProgramElement) {
0653: NonTerminalProgramElement nonTerminalNode = (NonTerminalProgramElement) node;
0654: for (int i = 0; i < nonTerminalNode
0655: .getChildCount(); i++) {
0656: walk(nonTerminalNode.getChildAt(i));
0657: }
0658: }
0659: }
0660:
0661: protected void doAction(ProgramElement node) {
0662: if (node instanceof Statement
0663: && !(node instanceof StatementBlock))
0664: System.err.println(node.getClass() + ":- "
0665: + node);
0666: if (node instanceof de.uka.ilkd.key.java.statement.MethodFrame)
0667: System.err
0668: .println(((de.uka.ilkd.key.java.statement.MethodFrame) node)
0669: .getExecutionContext());
0670: }
0671: };
0672: w.start();
0673: }
0674: });
0675: }
0676:
0677: private JButton createAutoModeButton() {
0678: return new JButton(autoModeAction);
0679: }
0680:
0681: private JComponent createOpenMostRecentFile() {
0682: final JButton button = new JButton();
0683: button.setAction(new OpenMostRecentFile());
0684: return button;
0685: }
0686:
0687: private JComponent createOpenFile() {
0688: final JButton button = new JButton();
0689: button.setAction(openFileAction);
0690: button.setText(null);
0691: return button;
0692: }
0693:
0694: private JComponent createSaveFile() {
0695: final JButton button = new JButton();
0696: button.setAction(saveFileAction);
0697: button.setText(null);
0698: return button;
0699: }
0700:
0701: private JButton createUnitTestButton() {
0702: testButton = new JButton();
0703: testButton.setAction(new CreateUnitTestAction());
0704:
0705: return testButton;
0706: }
0707:
0708: /** creates the toolbar button invoking decision procedures like ICS, Simplify */
0709: private JButton createDecisionProcedureButton() {
0710: String toolTipText = "Run "
0711: + ProofSettings.DEFAULT_SETTINGS
0712: .getDecisionProcedureSettings()
0713: .getDecisionProcedure();
0714: if (ProofSettings.DEFAULT_SETTINGS
0715: .getDecisionProcedureSettings().useSMT_Translation()) {
0716: toolTipText = "Run SMT Translation";
0717: }
0718:
0719: decisionProcedureButton = new JButton();
0720: decisionProcedureButton.setToolTipText(toolTipText);
0721: decisionProcedureButton.setText(toolTipText);
0722:
0723: // select icon
0724: if (ProofSettings.DEFAULT_SETTINGS
0725: .getDecisionProcedureSettings().useSimplify()) {
0726: decisionProcedureButton.setIcon(IconFactory
0727: .simplifyLogo(toolbarIconSize));
0728: } else if (ProofSettings.DEFAULT_SETTINGS
0729: .getDecisionProcedureSettings().useICS()) {
0730: decisionProcedureButton.setIcon(IconFactory
0731: .icsLogo(toolbarIconSize));
0732: } else if (ProofSettings.DEFAULT_SETTINGS
0733: .getDecisionProcedureSettings().useCVCLite()
0734: || ProofSettings.DEFAULT_SETTINGS
0735: .getDecisionProcedureSettings().useCVC3()
0736: || ProofSettings.DEFAULT_SETTINGS
0737: .getDecisionProcedureSettings().useSVC()
0738: || ProofSettings.DEFAULT_SETTINGS
0739: .getDecisionProcedureSettings().useYices()
0740: || ProofSettings.DEFAULT_SETTINGS
0741: .getDecisionProcedureSettings()
0742: .useSMT_Translation()) {
0743: // TODO: use different logos?!
0744: decisionProcedureButton.setIcon(IconFactory
0745: .icsLogo(toolbarIconSize));
0746: }
0747:
0748: decisionProcedureButton.addActionListener(new ActionListener() {
0749: public void actionPerformed(ActionEvent e) {
0750: if (!mediator.ensureProofLoaded())
0751: return;
0752: new DecProcRunner(Main.this ).run();
0753: }
0754: });
0755:
0756: return decisionProcedureButton;
0757: }
0758:
0759: public ProverTaskListener getProverTaskListener() {
0760: return taskListener;
0761: }
0762:
0763: /**
0764: * @return the status line object
0765: */
0766: public MainStatusLine getStatusLine() {
0767: return statusLine;
0768: }
0769:
0770: private void setStandardStatusLineImmediately() {
0771: statusLine.reset();
0772: }
0773:
0774: /**
0775: * Make the status line display a standard message, make progress bar and abort button invisible
0776: */
0777: public void setStandardStatusLine() {
0778: if (SwingUtilities.isEventDispatchThread())
0779: setStandardStatusLineImmediately();
0780: else {
0781: Runnable lineUpdater = new Runnable() {
0782: public void run() {
0783: setStandardStatusLineImmediately();
0784: }
0785: };
0786: SwingUtilities.invokeLater(lineUpdater);
0787: }
0788: }
0789:
0790: private void setStatusLineImmediately(String s) {
0791: statusLine.reset();
0792: statusLine.setStatusText(s);
0793: statusLine.setProgressPanelVisible(false);
0794: }
0795:
0796: private void setStatusLineImmediately(String s, int totalChars) {
0797: statusLine.reset();
0798: statusLine.setStatusText(s);
0799: getProgressMonitor().setMaximum(totalChars);
0800: statusLine.setProgressPanelVisible(true);
0801: // statusLine.setAbortButtonEnabled(false);
0802: }
0803:
0804: /**
0805: * Display the given message in the status line, make progress bar and abort button visible, set
0806: * the progress bar range to the given value, set the current progress to zero
0807: */
0808: public void setStatusLine(String s, int totalChars) {
0809: if (SwingUtilities.isEventDispatchThread())
0810: setStatusLineImmediately(s, totalChars);
0811: else {
0812: final String str = s;
0813: final int max = totalChars;
0814: Runnable lineUpdater = new Runnable() {
0815: public void run() {
0816: setStatusLineImmediately(str, max);
0817: }
0818: };
0819: SwingUtilities.invokeLater(lineUpdater);
0820: }
0821: }
0822:
0823: /**
0824: * Display the given message in the status line, make progress bar and abort button invisible
0825: */
0826: public void setStatusLine(String s) {
0827: if (SwingUtilities.isEventDispatchThread())
0828: setStatusLineImmediately(s);
0829: else {
0830: final String str = s;
0831: Runnable lineUpdater = new Runnable() {
0832: public void run() {
0833: setStatusLineImmediately(str);
0834: }
0835: };
0836: SwingUtilities.invokeLater(lineUpdater);
0837: }
0838: }
0839:
0840: /**
0841: * Get the progress monitor that will update a progress bar in a corner of the main window.
0842: */
0843: public ProgressMonitor getProgressMonitor() {
0844: return progressMonitor;
0845: }
0846:
0847: /**
0848: * Freeze the main window by blocking all input events, except those for the status line (i.e.
0849: * the abort button within the status line)
0850: */
0851: public void freezeExceptAutoModeButton() {
0852: if (!frozen) {
0853: frozen = true;
0854:
0855: Component glassPane = new BlockingGlassPane(
0856: getContentPane());
0857: setGlassPane(glassPane);
0858: glassPane.setVisible(true);
0859: }
0860: }
0861:
0862: public void unfreezeExceptAutoModeButton() {
0863: if (frozen) {
0864: getGlassPane().setVisible(false);
0865: frozen = false;
0866: }
0867: }
0868:
0869: /** exit */
0870: protected void exitMain() {
0871: boolean quit = false;
0872: final int option = JOptionPane.showConfirmDialog(Main.this ,
0873: "Really Quit?", "Exit", JOptionPane.YES_NO_OPTION);
0874: if (option == JOptionPane.YES_OPTION) {
0875: quit = true;
0876: }
0877:
0878: recentFiles.store(PathConfig.RECENT_FILES_STORAGE);
0879:
0880: if (quit) {
0881: mediator.fireShutDown(new GUIEvent(this ));
0882:
0883: if (standalone) {
0884: // wait some seconds; give notification sound a bit time
0885: try {
0886: Thread.sleep(1000);
0887: } catch (InterruptedException ie) {
0888: Debug.out("Thread has been interrupted.");
0889: }
0890: System.out.println("Have a nice day.");
0891: System.exit(-1);
0892: }
0893: }
0894: // Release threads waiting for the prover to exit
0895: synchronized (this .monitor) {
0896: this .monitor.notifyAll();
0897: }
0898: }
0899:
0900: /** opens selection dialog for the maximum tooltip line number */
0901: protected void selectMaxTooltipLines() {
0902: ViewSelector vselector = new ViewSelector(this );
0903: vselector.setVisible(true);
0904: }
0905:
0906: /** opens selection dialog for choices */
0907: protected void selectChoices() {
0908: new ChoiceSelector(ProofSettings.DEFAULT_SETTINGS
0909: .getChoiceSettings());
0910: }
0911:
0912: protected void showActivatedChoices() {
0913: Proof currentProof = mediator.getProof();
0914: if (currentProof == null) {
0915: mediator
0916: .notify(new GeneralInformationEvent(
0917: "No Options available.",
0918: "If you wish to see Taclet Options "
0919: + "for a proof you have to load one first"));
0920: } else {
0921: Iterator it = currentProof.getSettings()
0922: .getChoiceSettings().getDefaultChoices().values()
0923: .iterator();
0924: String message = "Active Taclet Options:\n";
0925: while (it.hasNext()) {
0926: message += it.next().toString() + "\n";
0927: }
0928: final JTextComponent activeOptions = new JTextArea(message);
0929: activeOptions.setEditable(false);
0930: JOptionPane.showMessageDialog(Main.this , activeOptions,
0931: "Active Taclet Options",
0932: JOptionPane.INFORMATION_MESSAGE);
0933: }
0934: }
0935:
0936: public void showSpecBrowser() {
0937: if (mediator.getProof() == null) {
0938: mediator.notify(new GeneralFailureEvent(
0939: "Please load a proof first"));
0940: } else {
0941: JMLSpecBrowser.getJMLSpecBrowser(mediator);
0942: }
0943: }
0944:
0945: public void showDLSpecBrowser() {
0946: if (mediator.getProof() == null) {
0947: mediator.notify(new GeneralFailureEvent(
0948: "Please load a proof first"));
0949: } else {
0950: JDialog fr = UsedMethodContractsList
0951: .getInstance(mediator());
0952: fr.setVisible(true);
0953: }
0954: }
0955:
0956: /**
0957: * for debugging - opens a window with the settings from current Proof and the default settings
0958: */
0959: protected void showSettings() {
0960: String message;
0961:
0962: message = "Default Settings: \n"
0963: + ProofSettings.DEFAULT_SETTINGS.settingsToString()
0964: + "\n----------\n";
0965: message += "Settings[CurrentProof]:\n"
0966: + ((mediator.getProof() == null) ? "No proof loaded."
0967: : mediator.getProof().getSettings()
0968: .settingsToString());
0969:
0970: final JTextArea settings = new JTextArea(message, 30, 80);
0971: settings.setEditable(false);
0972: settings.setLineWrap(true);
0973:
0974: JScrollPane settingsPane = new JScrollPane(settings);
0975:
0976: JOptionPane.showMessageDialog(Main.this , settingsPane,
0977: "Settings", JOptionPane.INFORMATION_MESSAGE);
0978: }
0979:
0980: /** opens configuration dialog for the simultaneous update simplifier */
0981: protected void configSimultaneousUpdateSimplifier() {
0982: SimultaneousUpdateSimplifierConfiguration config = new SimultaneousUpdateSimplifierConfiguration(
0983: mediator(), ProofSettings.DEFAULT_SETTINGS
0984: .getSimultaneousUpdateSimplifierSettings());
0985: config.setVisible(true);
0986: }
0987:
0988: /**
0989: * opens a configuration dialog for the loaded libraries
0990: */
0991: protected void configLibraries() {
0992: LibrariesConfiguration config = new LibrariesConfiguration(
0993: mediator(), ProofSettings.DEFAULT_SETTINGS
0994: .getLibrariesSettings());
0995: config.setVisible(true);
0996: }
0997:
0998: protected void setBack() {
0999: mediator.setBack();
1000: }
1001:
1002: protected void makePrettyView() {
1003: if (mediator().ensureProofLoadedSilent()) {
1004: if (!PresentationFeatures.ENABLED) {
1005: mediator().getNotationInfo().setBackToDefault();
1006: } else {
1007: PresentationFeatures.modifyNotationInfo(mediator
1008: .getNotationInfo(), mediator.func_ns());
1009: }
1010: mediator().getSelectedProof().updateProof();
1011: userConstraintView.updateTableDisplay(); // %%% HACK
1012: }
1013:
1014: }
1015:
1016: public JMLPOAndSpecProvider getJMLPOAndSpecProvider() {
1017: return new JMLEclipseAdapter(mediator);
1018: }
1019:
1020: public void showLicense() {
1021:
1022: URL lic = KeYResourceManager.getManager().getResourceFile(
1023: Main.class, "LICENSE.TXT");
1024: StringBuffer sb = new StringBuffer();
1025: try {
1026: FileInputStream inp = new FileInputStream(lic.getFile());
1027: while (inp.available() > 0)
1028: sb.append((char) inp.read());
1029: } catch (IOException ioe) {
1030: System.out
1031: .println("License file cannot be loaded or is missing: \n"
1032: + COPYRIGHT
1033: + "\nKeY is protected by the "
1034: + "GNU General Public License");
1035: sb = new StringBuffer(COPYRIGHT
1036: + "\nKeY is protected by the "
1037: + "GNU General Public License");
1038: }
1039: String s = sb.toString();
1040: JScrollPane scroll = new JScrollPane();
1041: JTextArea text = new JTextArea(s, 20, 40);
1042: text.setEditable(false);
1043: text.setCaretPosition(0);
1044: scroll.setViewportView(text);
1045: JFrame fr = new JFrame("KeY License");
1046: fr.getContentPane().setLayout(new BorderLayout());
1047: fr.getContentPane().add(scroll, BorderLayout.CENTER);
1048: JButton ok = new JButton("OK");
1049: ok.addActionListener(new ActionListener() {
1050: public void actionPerformed(ActionEvent e) {
1051: ((JFrame) ((JButton) e.getSource())
1052: .getTopLevelAncestor()).dispose();
1053: }
1054: });
1055: fr.getContentPane().add(ok, BorderLayout.SOUTH);
1056: fr.setSize(600, 900);
1057: fr.getContentPane().add(scroll);
1058: fr.setVisible(true);
1059: }
1060:
1061: public void showAbout() {
1062: String aspects = compiledAspects();
1063: JOptionPane pane = new JOptionPane(COPYRIGHT
1064: + "\n\nWWW: http://key-project.org\n\nVersion "
1065: + VERSION
1066: + ((aspects.length() == 0) ? ""
1067: : "\nCompiled with Aspects:\n" + aspects),
1068: JOptionPane.INFORMATION_MESSAGE,
1069: JOptionPane.DEFAULT_OPTION, IconFactory
1070: .keyLogo(105, 60));
1071: JDialog dialog = pane.createDialog(this , "The KeY Project");
1072: dialog.setVisible(true);
1073: }
1074:
1075: /**
1076: * Return a list of aspects compiled into the system, one by line. The idea is that the aspects
1077: * will advise this method to add themselves to the list.
1078: */
1079: public String compiledAspects() {
1080: return "";
1081: }
1082:
1083: /**
1084: * registers a new menuitem at the given menu
1085: *
1086: * @param menu
1087: * the JMenu where to register the new item
1088: * @param item
1089: * the JMenuItem to register
1090: */
1091: public void registerAtMenu(JMenu menu, JMenuItem item) {
1092: menu.add(item);
1093: }
1094:
1095: /**
1096: * adds a separator to the given menu
1097: */
1098: public void addSeparator(JMenu menu) {
1099: menu.addSeparator();
1100: }
1101:
1102: /** the number of goals the goal list currently contains */
1103: public int displayedOpenGoalNumber() {
1104: return goalList.getModel().getSize();
1105: }
1106:
1107: /** starts the goal choice frame */
1108: protected void initGoalList() {
1109: goalList = new GoalList(mediator);
1110: goalList.setSize(goalList.getPreferredSize());
1111: openGoalsView.setViewportView(goalList);
1112: }
1113:
1114: protected void initProofList() {
1115: proofList = new TaskTree(mediator);
1116: proofListView = new JScrollPane();
1117: }
1118:
1119: protected void addToProofList(
1120: de.uka.ilkd.key.proof.ProofAggregate plist) {
1121: proofList.addProof(plist);
1122: // GUI
1123: proofList.setSize(proofList.getPreferredSize());
1124: proofListView.setViewportView(proofList);
1125: }
1126:
1127: /** starts the gui proof tree frame */
1128: protected void initGUIProofTree() {
1129: ProofTreeView guiProofTree = new ProofTreeView(mediator);
1130: guiProofTree.setSize(guiProofTree.getPreferredSize());
1131: guiProofTree.setVisible(true);
1132: proofView.removeAll();
1133: proofView.add(guiProofTree);
1134: }
1135:
1136: static java.awt.TextArea clipBoardTextArea = new java.awt.TextArea(
1137: "", 10, 10, java.awt.TextArea.SCROLLBARS_NONE) {
1138: public java.awt.Dimension getMaximumSize() {
1139: return new java.awt.Dimension(0, 0);
1140: }
1141: };
1142:
1143: public static void copyHighlightToClipboard(SequentView view) {
1144: String s = view.getHighlightedText();
1145: // now CLIPBOARD
1146: java.awt.datatransfer.StringSelection ss = new java.awt.datatransfer.StringSelection(
1147: s);
1148: clipBoardTextArea.getToolkit().getSystemClipboard()
1149: .setContents(ss, ss);
1150: // now PRIMARY
1151: clipBoardTextArea.setText(s);
1152: clipBoardTextArea.selectAll();
1153: }
1154:
1155: protected JMenu createFileMenu() {
1156: JMenu fileMenu = new JMenu("File");
1157: fileMenu.setMnemonic(KeyEvent.VK_F);
1158:
1159: JMenuItem load = new JMenuItem();
1160: load.setAction(openFileAction);
1161:
1162: JMenuItem save = new JMenuItem();
1163: save.setAction(saveFileAction);
1164:
1165: registerAtMenu(fileMenu, load);
1166: registerAtMenu(fileMenu, save);
1167:
1168: JMenuItem tacletPOItem = new JMenuItem(
1169: "Load Non-Axiom Lemma ...");
1170: tacletPOItem.addActionListener(new ActionListener() {
1171: public void actionPerformed(ActionEvent e) {
1172: if (mediator().ensureProofLoaded()) {
1173: generateTacletPO();
1174: }
1175: }
1176: });
1177: registerAtMenu(fileMenu, tacletPOItem);
1178:
1179: JMenuItem exit = new JMenuItem("Exit");
1180: exit.setAccelerator(KeyStroke.getKeyStroke(KeyEvent.VK_Q,
1181: ActionEvent.CTRL_MASK));
1182: exit.addActionListener(new ActionListener() {
1183: public void actionPerformed(ActionEvent e) {
1184: exitMain();
1185: }
1186: });
1187:
1188: addSeparator(fileMenu);
1189:
1190: recentFiles = new RecentFileMenu(new ActionListener() {
1191: public void actionPerformed(ActionEvent e) {
1192: loadProblem(new File(recentFiles
1193: .getAbsolutePath((JMenuItem) e.getSource())));
1194: }
1195: }, MAX_RECENT_FILES, null);
1196:
1197: recentFiles.load(PathConfig.RECENT_FILES_STORAGE);
1198:
1199: registerAtMenu(fileMenu, recentFiles.getMenu());
1200:
1201: addSeparator(fileMenu);
1202: registerAtMenu(fileMenu, exit);
1203: return fileMenu;
1204: }
1205:
1206: protected JMenu createFontSizeMenuEntry() {
1207: final JMenu fontSize = new JMenu("Font Size");
1208:
1209: final JMenuItem smaller = new JMenuItem("Smaller");
1210: smaller.addActionListener(new ActionListener() {
1211: public void actionPerformed(ActionEvent e) {
1212: Config.DEFAULT.smaller();
1213: }
1214: });
1215: smaller.setAccelerator(KeyStroke.getKeyStroke(KeyEvent.VK_DOWN,
1216: InputEvent.CTRL_DOWN_MASK));
1217:
1218: final JMenuItem larger = new JMenuItem("Larger");
1219: larger.addActionListener(new ActionListener() {
1220: public void actionPerformed(ActionEvent e) {
1221: Config.DEFAULT.larger();
1222: }
1223: });
1224: larger.setAccelerator(KeyStroke.getKeyStroke(KeyEvent.VK_UP,
1225: InputEvent.CTRL_DOWN_MASK));
1226:
1227: Config.DEFAULT
1228: .addConfigChangeListener(new ConfigChangeListener() {
1229: public void configChanged(ConfigChangeEvent e) {
1230: smaller.setEnabled(!Config.DEFAULT
1231: .isMinimumSize());
1232: larger.setEnabled(!Config.DEFAULT
1233: .isMaximumSize());
1234: }
1235: });
1236:
1237: fontSize.add(smaller);
1238: fontSize.add(larger);
1239: return fontSize;
1240: }
1241:
1242: protected JMenu createViewMenu() {
1243: JMenu view = new JMenu("View");
1244: view.setMnemonic(KeyEvent.VK_V);
1245:
1246: JMenuItem pretty = new JCheckBoxMenuItem("Use pretty syntax");
1247: pretty.setToolTipText("If ticked, infix notations are used.");
1248: pretty.setSelected(PresentationFeatures.ENABLED);
1249: pretty.addActionListener(new ActionListener() {
1250: public void actionPerformed(ActionEvent e) {
1251: PresentationFeatures.ENABLED = ((JCheckBoxMenuItem) e
1252: .getSource()).isSelected();
1253: makePrettyView();
1254: }
1255: });
1256:
1257: registerAtMenu(view, pretty);
1258: addSeparator(view);
1259:
1260: registerAtMenu(view, createFontSizeMenuEntry());
1261:
1262: final JMenuItem tacletOptionsView = new JMenuItem(
1263: TACLET_OPTIONS_MENU_STRING);
1264:
1265: tacletOptionsView.setAccelerator(KeyStroke.getKeyStroke(
1266: KeyEvent.VK_M, ActionEvent.CTRL_MASK));
1267: tacletOptionsView.addActionListener(new ActionListener() {
1268: public void actionPerformed(ActionEvent e) {
1269: selectMaxTooltipLines();
1270: tacletOptionsView.setText(TACLET_OPTIONS_MENU_STRING);
1271: //+ "(" +
1272: // ProofSettings.DEFAULT_SETTINGS.getViewSettings().getMaxTooltipLines()
1273: // + ")");
1274: }
1275: });
1276: registerAtMenu(view, tacletOptionsView);
1277:
1278: return view;
1279: }
1280:
1281: protected JMenu createProofMenu() {
1282: JMenu proof = new JMenu("Proof");
1283: proof.setMnemonic(KeyEvent.VK_P);
1284: JMenuItem close = new JMenuItem("Abandon Task");
1285: close.setAccelerator(KeyStroke.getKeyStroke(KeyEvent.VK_W,
1286: ActionEvent.CTRL_MASK));
1287: close.addActionListener(new ActionListener() {
1288: public void actionPerformed(ActionEvent e) {
1289: closeTask();
1290: }
1291: });
1292: registerAtMenu(proof, close);
1293:
1294: JMenuItem choiceItem = new JMenuItem(
1295: "Show Active Taclet Options");
1296: choiceItem.addActionListener(new ActionListener() {
1297: public void actionPerformed(ActionEvent e) {
1298: showActivatedChoices();
1299: }
1300: });
1301: registerAtMenu(proof, choiceItem);
1302:
1303: JMenuItem methodContractsItem = new JMenuItem(
1304: "Show Used Specifications...");
1305: methodContractsItem.addActionListener(new ActionListener() {
1306: public void actionPerformed(ActionEvent e) {
1307: JDialog fr = new UsedMethodContractsList(mediator
1308: .getSelectedProof().getBasicTask(), mediator);
1309: fr.setVisible(true);
1310: }
1311: });
1312: registerAtMenu(proof, methodContractsItem);
1313:
1314: final JMenuItem statisticsInfo = new JMenuItem(
1315: "Show Proof Statistics");
1316:
1317: statisticsInfo.addActionListener(new ActionListener() {
1318: public void actionPerformed(ActionEvent e) {
1319: final Proof proof = mediator.getSelectedProof();
1320: if (mediator() != null && proof != null) {
1321:
1322: String stats = proof.statistics();
1323:
1324: int interactiveSteps = computeInteractiveSteps(proof
1325: .root());
1326:
1327: stats += "Interactive Steps: " + interactiveSteps;
1328:
1329: JOptionPane.showMessageDialog(Main.this , stats,
1330: "Proof Statistics",
1331: JOptionPane.INFORMATION_MESSAGE);
1332: }
1333: }
1334:
1335: private int computeInteractiveSteps(Node node) {
1336: int steps = 0;
1337: final IteratorOfNode it = node.childrenIterator();
1338: while (it.hasNext()) {
1339: steps += computeInteractiveSteps(it.next());
1340: }
1341:
1342: if (node.getNodeInfo().getInteractiveRuleApplication()) {
1343: steps++;
1344: }
1345: return steps;
1346: }
1347: });
1348: registerAtMenu(proof, statisticsInfo);
1349:
1350: return proof;
1351: }
1352:
1353: protected JMenu createOptionsMenu() {
1354: JMenu options = new JMenu("Options");
1355: options.setMnemonic(KeyEvent.VK_O);
1356: JMenuItem choiceItem = new JMenuItem(
1357: "Default Taclet Options...");
1358: choiceItem.setAccelerator(KeyStroke.getKeyStroke(KeyEvent.VK_T,
1359: ActionEvent.CTRL_MASK));
1360:
1361: choiceItem.addActionListener(new ActionListener() {
1362: public void actionPerformed(ActionEvent e) {
1363: selectChoices();
1364: }
1365: });
1366: registerAtMenu(options, choiceItem);
1367:
1368: JMenuItem updateSimplifierItem = new JMenuItem(
1369: "Update Simplifier...");
1370: updateSimplifierItem.setAccelerator(KeyStroke.getKeyStroke(
1371: KeyEvent.VK_U, ActionEvent.CTRL_MASK));
1372:
1373: updateSimplifierItem.addActionListener(new ActionListener() {
1374: public void actionPerformed(ActionEvent e) {
1375: configSimultaneousUpdateSimplifier();
1376: }
1377: });
1378: registerAtMenu(options, updateSimplifierItem);
1379:
1380: ButtonGroup decisionProcGroup = new ButtonGroup();
1381:
1382: JMenuItem librariesItem = new JMenuItem("Taclet Libraries...");
1383: librariesItem.addActionListener(new ActionListener() {
1384: public void actionPerformed(ActionEvent e) {
1385: configLibraries();
1386: }
1387: });
1388: registerAtMenu(options, librariesItem);
1389:
1390: setupDecisionProcedureGroup(decisionProcGroup);
1391:
1392: registerAtMenu(options, decisionProcedureOption);
1393:
1394: JMenuItem computeSpecificationOptions = ComputeSpecificationView
1395: .createOptionMenuItems();
1396: registerAtMenu(options, computeSpecificationOptions);
1397:
1398: // GENERAL SETTINGS
1399: // minimize interaction
1400: final boolean stupidMode = ProofSettings.DEFAULT_SETTINGS
1401: .getGeneralSettings().stupidMode();
1402: final JMenuItem stupidModeOption = new JCheckBoxMenuItem(
1403: "Minimize Interaction", stupidMode);
1404: mediator.setStupidMode(stupidMode);
1405:
1406: stupidModeOption.addActionListener(new ActionListener() {
1407: public void actionPerformed(ActionEvent e) {
1408: boolean b = ((JCheckBoxMenuItem) e.getSource())
1409: .isSelected();
1410: mediator().setStupidMode(b);
1411: ProofSettings.DEFAULT_SETTINGS.getGeneralSettings()
1412: .setStupidMode(b);
1413: }
1414: });
1415:
1416: registerAtMenu(options, stupidModeOption);
1417:
1418: // suggestive var names
1419: // currently removed to avoid confusion
1420: /*
1421: final boolean suggestiveVarNames =
1422: ProofSettings.DEFAULT_SETTINGS.getGeneralSettings().suggestiveVarNames();
1423: final JMenuItem suggVarNamesOption =
1424: new JCheckBoxMenuItem("Suggestive names for aux vars",
1425: suggestiveVarNames);
1426: VariableNamer.setSuggestiveEnabled(suggestiveVarNames);
1427:
1428: suggVarNamesOption.addActionListener(new ActionListener() {
1429: public void actionPerformed(ActionEvent e) {
1430: boolean b = ((JCheckBoxMenuItem)e.getSource()).isSelected();
1431: VariableNamer.setSuggestiveEnabled(b);
1432: ProofSettings.DEFAULT_SETTINGS.
1433: getGeneralSettings().setSuggestiveVarNames(b);
1434: }});
1435:
1436: registerAtMenu(options, suggVarNamesOption);
1437: */
1438:
1439: addSeparator(options);
1440:
1441: final boolean dndDirectionSensitivity = ProofSettings.DEFAULT_SETTINGS
1442: .getGeneralSettings().isDndDirectionSensitive();
1443: final JMenuItem dndDirectionSensitivityOption = new JCheckBoxMenuItem(
1444: "DnD Direction Sensitive", dndDirectionSensitivity);
1445: dndDirectionSensitivityOption
1446: .addActionListener(new ActionListener() {
1447: public void actionPerformed(ActionEvent e) {
1448: boolean b = ((JCheckBoxMenuItem) e.getSource())
1449: .isSelected();
1450: ProofSettings.DEFAULT_SETTINGS
1451: .getGeneralSettings()
1452: .setDnDDirectionSensitivity(b);
1453: }
1454: });
1455:
1456: registerAtMenu(options, dndDirectionSensitivityOption);
1457:
1458: // sound settings
1459: final boolean soundNotification = ProofSettings.DEFAULT_SETTINGS
1460: .getGeneralSettings().soundNotification();
1461: final JMenuItem soundNotificationOption = new JCheckBoxMenuItem(
1462: "Sound", soundNotification);
1463: if (notificationManager != null) {
1464: notificationManager
1465: .setDefaultNotification(soundNotification);
1466: }
1467: soundNotificationOption.addActionListener(new ActionListener() {
1468: public void actionPerformed(ActionEvent e) {
1469: boolean b = ((JCheckBoxMenuItem) e.getSource())
1470: .isSelected();
1471: if (notificationManager != null) {
1472: notificationManager.setDefaultNotification(b);
1473: }
1474: ProofSettings.DEFAULT_SETTINGS.getGeneralSettings()
1475: .setSoundNotification(b);
1476: }
1477: });
1478:
1479: registerAtMenu(options, soundNotificationOption);
1480:
1481: // proof assistant
1482: final JMenuItem assistantOption = new JCheckBoxMenuItem(
1483: "Proof Assistant", ProofSettings.DEFAULT_SETTINGS
1484: .getGeneralSettings().proofAssistantMode());
1485:
1486: final ProofAssistantController assistant = new ProofAssistantController(
1487: mediator, ProofSettings.DEFAULT_SETTINGS
1488: .getGeneralSettings(), new ProofAssistantAI(),
1489: new ProofAssistant());
1490:
1491: // listen to the state of the assistant in order to hold the
1492: // item and state consistent
1493: assistant.addChangeListener(new ChangeListener() {
1494: public void stateChanged(ChangeEvent e) {
1495: final boolean assistentEnabled = ((ProofAssistantController) e
1496: .getSource()).getState();
1497: assistantOption.setSelected(assistentEnabled);
1498: // setSelected does not trigger an action event so we have
1499: // to make the change explicitly permanent
1500: ProofSettings.DEFAULT_SETTINGS.getGeneralSettings()
1501: .setProofAssistantMode(assistentEnabled);
1502: }
1503: });
1504:
1505: assistantOption.addActionListener(new ActionListener() {
1506: public void actionPerformed(ActionEvent e) {
1507: ProofSettings.DEFAULT_SETTINGS.getGeneralSettings()
1508: .setProofAssistantMode(
1509: ((JCheckBoxMenuItem) e.getSource())
1510: .isSelected());
1511: }
1512: });
1513:
1514: registerAtMenu(options, assistantOption);
1515:
1516: return options;
1517: }
1518:
1519: /**
1520: * @param decisionProcGroup
1521: */
1522: private void setupDecisionProcedureGroup(
1523: ButtonGroup decisionProcGroup) {
1524: simplifyButton.setSelected(ProofSettings.DEFAULT_SETTINGS
1525: .getDecisionProcedureSettings().useSimplify());
1526: simplifyButton.setIcon(IconFactory.simplifyLogo(15));
1527: decisionProcGroup.add(simplifyButton);
1528: decisionProcedureOption.add(simplifyButton);
1529:
1530: DecisionProcButtonListener decisionProcButtonListener = new DecisionProcButtonListener();
1531: simplifyButton.addActionListener(decisionProcButtonListener);
1532:
1533: icsButton.setIcon(IconFactory.icsLogo(15));
1534: icsButton.setSelected(ProofSettings.DEFAULT_SETTINGS
1535: .getDecisionProcedureSettings().useICS());
1536: decisionProcGroup.add(icsButton);
1537: decisionProcedureOption.add(icsButton);
1538: icsButton.addActionListener(decisionProcButtonListener);
1539:
1540: cvc3Button.setIcon(IconFactory.icsLogo(15));
1541: cvc3Button.setSelected(ProofSettings.DEFAULT_SETTINGS
1542: .getDecisionProcedureSettings().useCVC3());
1543: decisionProcGroup.add(cvc3Button);
1544: decisionProcedureOption.add(cvc3Button);
1545: cvc3Button.addActionListener(decisionProcButtonListener);
1546:
1547: cvcLiteButton.setIcon(IconFactory.icsLogo(15));
1548: cvcLiteButton.setSelected(ProofSettings.DEFAULT_SETTINGS
1549: .getDecisionProcedureSettings().useCVCLite());
1550: decisionProcGroup.add(cvcLiteButton);
1551: decisionProcedureOption.add(cvcLiteButton);
1552: cvcLiteButton.addActionListener(decisionProcButtonListener);
1553:
1554: svcButton.setIcon(IconFactory.icsLogo(15));
1555: svcButton.setSelected(ProofSettings.DEFAULT_SETTINGS
1556: .getDecisionProcedureSettings().useSVC());
1557: decisionProcGroup.add(svcButton);
1558: decisionProcedureOption.add(svcButton);
1559: svcButton.addActionListener(decisionProcButtonListener);
1560:
1561: yicesButton.setIcon(IconFactory.icsLogo(15));
1562: yicesButton.setSelected(ProofSettings.DEFAULT_SETTINGS
1563: .getDecisionProcedureSettings().useYices());
1564: decisionProcGroup.add(yicesButton);
1565: decisionProcedureOption.add(yicesButton);
1566: yicesButton.addActionListener(decisionProcButtonListener);
1567:
1568: smtButton.setIcon(IconFactory.icsLogo(15));
1569: smtButton.setSelected(ProofSettings.DEFAULT_SETTINGS
1570: .getDecisionProcedureSettings().useSMT_Translation());
1571: decisionProcGroup.add(smtButton);
1572: decisionProcedureOption.add(smtButton);
1573: smtButton.addActionListener(decisionProcButtonListener);
1574:
1575: // Add option for quantifier translation
1576: final boolean useQuantifiers = ProofSettings.DEFAULT_SETTINGS
1577: .getDecisionProcedureSettings().useQuantifiers();
1578: smtUseQuantifiersOption = new JCheckBoxMenuItem(
1579: "Translate quantifiers (SMT)", useQuantifiers);
1580: decisionProcedureOption.add(smtUseQuantifiersOption);
1581: smtUseQuantifiersOption
1582: .addActionListener(decisionProcButtonListener);
1583:
1584: // Add the options for SMT benchmark archiving
1585: decisionProcedureOption.addSeparator();
1586: final boolean benchmarkArchiving = ProofSettings.DEFAULT_SETTINGS
1587: .getDecisionProcedureSettings().doBenchmarkArchiving();
1588: smtBenchmarkArchivingOption = new JCheckBoxMenuItem(
1589: "Archive SMT benchmarks", benchmarkArchiving);
1590: decisionProcedureOption.add(smtBenchmarkArchivingOption);
1591: smtBenchmarkArchivingOption
1592: .addActionListener(decisionProcButtonListener);
1593:
1594: final boolean zipProblemDir = ProofSettings.DEFAULT_SETTINGS
1595: .getDecisionProcedureSettings().doZipProblemDir();
1596: smtZipProblemDirOption = new JCheckBoxMenuItem(
1597: "Zip problem dir into archive", zipProblemDir);
1598: decisionProcedureOption.add(smtZipProblemDirOption);
1599: smtZipProblemDirOption
1600: .addActionListener(decisionProcButtonListener);
1601: }
1602:
1603: public JMenu createHelpMenu() {
1604: JMenu help = new JMenu("About");
1605: help.setMnemonic(KeyEvent.VK_A);
1606: JMenuItem about = new JMenuItem("About KeY");
1607: about.addActionListener(new ActionListener() {
1608: public void actionPerformed(ActionEvent e) {
1609: showAbout();
1610: }
1611: });
1612: help.add(about);
1613:
1614: JMenuItem license = new JMenuItem("License");
1615: license.addActionListener(new ActionListener() {
1616: public void actionPerformed(ActionEvent e) {
1617: showLicense();
1618: }
1619: });
1620: help.add(license);
1621: return help;
1622: }
1623:
1624: protected JMenu createToolsMenu() {
1625: JMenu tools = new JMenu("Tools");
1626: tools.setMnemonic(KeyEvent.VK_T);
1627: getJMenuBar().add(tools);
1628:
1629: JMenuItem extractSpecification = new JMenuItem(
1630: "Extract Specification");
1631: extractSpecification.setAccelerator(KeyStroke.getKeyStroke(
1632: KeyEvent.VK_E, ActionEvent.CTRL_MASK));
1633:
1634: extractSpecification.addActionListener(new ActionListener() {
1635: public void actionPerformed(ActionEvent e) {
1636: if (mediator().ensureProofLoaded()) {
1637: //@internal we don't want to block UI just
1638: //because we are about to calculate a lot of
1639: //things, now. Also the interactive prover
1640: //might want to run during the execution of
1641: //ComputeSpecification
1642: new Thread(new Runnable() {
1643: public void run() {
1644: ComputeSpecificationView.show(mediator());
1645: }
1646: }).start();
1647: }
1648: }
1649: });
1650: tools.add(extractSpecification);
1651:
1652: JMenuItem specificationBrowser = new JMenuItem(
1653: "JML Specification Browser...");
1654: specificationBrowser.setAccelerator(KeyStroke.getKeyStroke(
1655: KeyEvent.VK_J, ActionEvent.CTRL_MASK));
1656: specificationBrowser.addActionListener(new ActionListener() {
1657: public void actionPerformed(ActionEvent e) {
1658: showSpecBrowser();
1659: }
1660: });
1661: registerAtMenu(tools, specificationBrowser);
1662:
1663: JMenuItem dlSpecificationBrowser = new JMenuItem(
1664: "DL Specification Browser...");
1665: dlSpecificationBrowser.setAccelerator(KeyStroke.getKeyStroke(
1666: KeyEvent.VK_L, ActionEvent.CTRL_MASK));
1667: dlSpecificationBrowser.addActionListener(new ActionListener() {
1668: public void actionPerformed(ActionEvent e) {
1669: showDLSpecBrowser();
1670: }
1671: });
1672: registerAtMenu(tools, dlSpecificationBrowser);
1673:
1674: JMenuItem nonInterference = new JMenuItem(
1675: "Check Non-Interference");
1676: nonInterference.addActionListener(new ActionListener() {
1677: public void actionPerformed(ActionEvent e) {
1678: BasicTask[] selProofs = proofList
1679: .getAllSelectedBasicTasks();
1680: if (selProofs.length == 2) {
1681: new NonInterferenceCheck(selProofs).run();
1682: } else {
1683: mediator().popupWarning("Please select 2 proofs",
1684: "Non-Interference Check");
1685: }
1686: }
1687: });
1688:
1689: tools.add(nonInterference);
1690:
1691: JMenuItem testItem = new JMenuItem();
1692: testItem.setAction(createUnitTestAction);
1693:
1694: tools.add(testItem);
1695:
1696: return tools;
1697: }
1698:
1699: protected JMenu createDebugMenu() {
1700: JMenu debug = new JMenu("Debug");
1701: debug.setMnemonic(KeyEvent.VK_D);
1702: JMenuItem showSettings = new JMenuItem("Show settings");
1703: showSettings.addActionListener(new ActionListener() {
1704: public void actionPerformed(ActionEvent e) {
1705: showSettings();
1706: }
1707: });
1708: debug.add(showSettings);
1709: return debug;
1710: }
1711:
1712: /** creates menubar entries and adds them to menu bar */
1713: private void createMenuBarEntries() {
1714: JMenuBar menuBar = getJMenuBar();
1715: menuBar.add(createFileMenu());
1716: menuBar.add(createViewMenu());
1717: menuBar.add(createProofMenu());
1718: menuBar.add(createOptionsMenu());
1719: menuBar.add(createToolsMenu());
1720: menuBar.add(Box.createHorizontalGlue());
1721: menuBar.add(createHelpMenu());
1722: if (Debug.ENABLE_DEBUG)
1723: menuBar.add(createDebugMenu());
1724: }
1725:
1726: /**
1727: * returns the toolbar
1728: */
1729: public JToolBar getToolBar() {
1730: return toolBar;
1731: }
1732:
1733: /**
1734: * Sets the content of the current goal view. Do not use this method from outside, take method
1735: * {@link #updateGoalView(String, JComponent)} instead (thread safe)
1736: */
1737: private void paintGoalView(String borderTitle,
1738: JComponent goalViewPane) {
1739: goalView.setViewportView(goalViewPane);
1740: goalView.setBorder(new TitledBorder(borderTitle));
1741: goalView.validate();
1742: validate();
1743: }
1744:
1745: /**
1746: * updates the view of the sequent being displayed in the main frame
1747: */
1748: private synchronized void updateGoalView(final String borderTitle,
1749: final JComponent goalViewPane) {
1750: if (SwingUtilities.isEventDispatchThread()) {
1751: paintGoalView(borderTitle, goalViewPane);
1752: } else {
1753: Runnable sequentUpdater = new Runnable() {
1754: public void run() {
1755: paintGoalView(borderTitle, goalViewPane);
1756: }
1757: };
1758: SwingUtilities.invokeLater(sequentUpdater);
1759: }
1760: }
1761:
1762: /**
1763: * prints the content of the sequent view
1764: */
1765: public void printSequentView(Sequent sequent) {
1766: SequentPrintFilter filter = new ConstraintSequentPrintFilter(
1767: sequent, mediator().getUserConstraint().getConstraint());
1768: final LogicPrinter printer = new LogicPrinter(
1769: new ProgramPrinter(null), mediator().getNotationInfo(),
1770: mediator.getServices());
1771:
1772: sequentView.setPrinter(printer, filter, null);
1773: sequentView.printSequent();
1774:
1775: updateGoalView("Current Goal", sequentView);
1776: }
1777:
1778: public static KeYFileChooser getFileChooser(String title) {
1779: if (fileChooser == null) {
1780: fileChooser = new KeYFileChooser();
1781: }
1782: fileChooser.setDialogTitle(title);
1783: fileChooser.prepare();
1784: return fileChooser;
1785: }
1786:
1787: /** saves a proof */
1788: protected void saveProof() {
1789: KeYFileChooser jFC = getFileChooser("Choose filename to save proof");
1790: boolean saved = jFC.showSaveDialog(this );
1791: if (saved) {
1792: saveProof(jFC.getSelectedFile());
1793: }
1794: }
1795:
1796: protected void saveProof(String proofFile) {
1797: saveProof(new File(proofFile));
1798: }
1799:
1800: protected void saveProof(File proofFile) {
1801: String filename = proofFile.getAbsolutePath();
1802: ProofSaver saver;
1803: if (filename.endsWith(".tex"))
1804: saver = new ProofSaverLatex(this , filename);
1805: else
1806: saver = new ProofSaver(this , filename);
1807: String errorMsg = saver.save();
1808:
1809: if (errorMsg != null) {
1810: notify(new GeneralFailureEvent(
1811: "Saving Proof failed.\n Error: " + errorMsg));
1812: }
1813: }
1814:
1815: protected void loadProblem(File file) {
1816: recentFiles.addRecentFile(file.getAbsolutePath());
1817: if (unitKeY != null) {
1818: unitKeY.recent.addRecentFile(file.getAbsolutePath());
1819: }
1820: new ProblemLoader(file, this , mediator.getProfile()).run();
1821: }
1822:
1823: protected void closeTask() {
1824: final Proof proof = mediator.getProof();
1825: if (proof != null) {
1826: final TaskTreeNode rootTask = proof.getBasicTask()
1827: .getRootTask();
1828: proofList.removeTask(rootTask);
1829:
1830: ((ProofTreeView) proofView.getComponent(0))
1831: .removeProofs(rootTask.allProofs());
1832: }
1833: }
1834:
1835: public void closeTaskWithoutIntercation() {
1836: final Proof proof = mediator.getProof();
1837: if (proof != null) {
1838: final TaskTreeNode rootTask = proof.getBasicTask()
1839: .getRootTask();
1840: proofList.removeTaskWithoutInteraction(rootTask);
1841:
1842: ((ProofTreeView) proofView.getComponent(0))
1843: .removeProofs(rootTask.allProofs());
1844: }
1845: }
1846:
1847: protected void generateTacletPO() {
1848: final KeYFileChooser localFileChooser = getFileChooser("Choose file to "
1849: + "load taclets " + "from ...");
1850: boolean loaded = localFileChooser.showOpenDialog(Main.this );
1851: if (!loaded)
1852: return;
1853:
1854: final File file = localFileChooser.getSelectedFile();
1855:
1856: new TacletSoundnessPOLoader(file, this ).run();
1857: }
1858:
1859: /**
1860: * brings window in front and request focus
1861: */
1862: private void popup() {
1863: setState(Frame.NORMAL);
1864: setVisible(true);
1865: requestFocus();
1866: }
1867:
1868: public void addProblem(
1869: final de.uka.ilkd.key.proof.ProofAggregate plist) {
1870: Runnable guiUpdater = new Runnable() {
1871: public void run() {
1872: disableCurrentGoalView = true;
1873: addToProofList(plist);
1874: setUpNewProof(plist.getFirstProof());
1875: disableCurrentGoalView = false;
1876: setProofNodeDisplay();
1877: popup();
1878: }
1879: };
1880: if (SwingUtilities.isEventDispatchThread())
1881: guiUpdater.run();
1882: else
1883: KeYMediator.invokeAndWait(guiUpdater);
1884: }
1885:
1886: protected Proof setUpNewProof(Proof proof) {
1887: KeYMediator localMediator = mediator();
1888: localMediator.setProof(proof);
1889: return proof;
1890: }
1891:
1892: private java.util.Hashtable doNotEnable;
1893:
1894: private void setToolBarDisabled() {
1895: doNotEnable = new java.util.Hashtable(10);
1896: Component[] cs = toolBar.getComponents();
1897: int i = cs.length;
1898: while (i-- != 0) {
1899: if (!cs[i].isEnabled())
1900: doNotEnable.put(cs[i], cs[i]);
1901: cs[i].setEnabled(false);
1902: }
1903: }
1904:
1905: private void setToolBarEnabled() {
1906: Component[] cs = toolBar.getComponents();
1907: int i = cs.length;
1908: while (i-- != 0) {
1909: if (!doNotEnable.containsKey(cs[i]))
1910: cs[i].setEnabled(true);
1911: }
1912: }
1913:
1914: /**
1915: * Loads the last opened file
1916: */
1917: private final class OpenMostRecentFile extends AbstractAction {
1918:
1919: public OpenMostRecentFile() {
1920: putValue(SMALL_ICON, IconFactory
1921: .openMostRecent(toolbarIconSize));
1922: putValue(SHORT_DESCRIPTION, "Load last opened file.");
1923: }
1924:
1925: public void actionPerformed(ActionEvent e) {
1926: if (recentFiles != null
1927: && recentFiles.getMostRecent() != null) {
1928: final String recentFile = recentFiles.getMostRecent()
1929: .getAbsolutePath();
1930: if (recentFile != null) {
1931: loadProblem(new File(recentFile));
1932: }
1933: }
1934: }
1935: }
1936:
1937: /**
1938: * Opens a file dialog allowing to select the file to be loaded
1939: */
1940: private final class OpenFile extends AbstractAction {
1941: public OpenFile() {
1942: putValue(NAME, "Load ...");
1943: putValue(SMALL_ICON, IconFactory
1944: .openKeYFile(toolbarIconSize));
1945: putValue(SHORT_DESCRIPTION,
1946: "Browse and load problem or proof files.");
1947: putValue(ACCELERATOR_KEY, KeyStroke.getKeyStroke(
1948: KeyEvent.VK_O, ActionEvent.CTRL_MASK));
1949:
1950: }
1951:
1952: public void actionPerformed(ActionEvent e) {
1953: KeYFileChooser keYFileChooser = getFileChooser("Select file "
1954: + "to load proof " + "or problem");
1955: boolean loaded = keYFileChooser.showOpenDialog(Main.this );
1956: if (loaded) {
1957: File file = keYFileChooser.getSelectedFile();
1958: loadProblem(file);
1959: }
1960:
1961: }
1962: }
1963:
1964: /**
1965: * Saves the current selected proof.
1966: */
1967: private final class SaveFile extends AbstractAction {
1968:
1969: public SaveFile() {
1970: putValue(NAME, "Save ...");
1971: putValue(SMALL_ICON, IconFactory.saveFile(toolbarIconSize));
1972: putValue(SHORT_DESCRIPTION, "Save current proof.");
1973: putValue(ACCELERATOR_KEY, KeyStroke.getKeyStroke(
1974: KeyEvent.VK_S, ActionEvent.CTRL_MASK));
1975:
1976: setEnabled(mediator.getProof() != null);
1977:
1978: mediator
1979: .addKeYSelectionListener(new KeYSelectionListener() {
1980: /** focused node has changed */
1981: public void selectedNodeChanged(
1982: KeYSelectionEvent e) {
1983: }
1984:
1985: /**
1986: * the selected proof has changed. Enable or disable action depending whether a proof is
1987: * available or not
1988: */
1989: public void selectedProofChanged(
1990: KeYSelectionEvent e) {
1991: setEnabled(e.getSource().getSelectedProof() != null);
1992: }
1993: });
1994: }
1995:
1996: public void actionPerformed(ActionEvent e) {
1997: if (mediator().ensureProofLoaded()) {
1998: saveProof();
1999: }
2000: }
2001: }
2002:
2003: /**
2004: * The progress monitor that displays a progress bar in a corner of the main window.
2005: */
2006: class MainProgressMonitor implements ProgressMonitor {
2007: public void setProgress(int progress) {
2008: if (SwingUtilities.isEventDispatchThread())
2009: statusLine.setProgress(progress);
2010: else {
2011: final int v = progress;
2012: Runnable lineUpdater = new Runnable() {
2013: public void run() {
2014: statusLine.setProgress(v);
2015: }
2016: };
2017: SwingUtilities.invokeLater(lineUpdater);
2018: }
2019: }
2020:
2021: public void setMaximum(int maximum) {
2022: statusLine.setProgressBarMaximum(maximum);
2023: }
2024: }
2025:
2026: class MainListener extends WindowAdapter {
2027: public void windowClosing(WindowEvent e) {
2028: if (testStandalone) {
2029: visible = false;
2030: setVisible(false);
2031: } else {
2032: exitMain();
2033: }
2034: }
2035: }
2036:
2037: class MainGUIListener implements GUIListener {
2038: /** invoked if a frame that wants modal access is opened */
2039:
2040: private void enableMenuBar(JMenuBar m, boolean b) {
2041: for (int i = 0; i < m.getMenuCount(); i++) {
2042: if (m.getMenu(i) != null) { // otherwise it is a spacer
2043: m.getMenu(i).setEnabled(b);
2044: }
2045: }
2046: }
2047:
2048: public void modalDialogOpened(GUIEvent e) {
2049:
2050: if (e.getSource() instanceof ApplyTacletDialog) {
2051: // disable all elements except the sequent window (drag'n'drop !) ...
2052: enableMenuBar(Main.this .getJMenuBar(), false);
2053: Main.this .goalView.setEnabled(false);
2054: Main.this .proofView.setEnabled(false);
2055: Main.this .openGoalsView.setEnabled(false);
2056: Main.this .userConstraintView.setEnabled(false);
2057: Main.this .strategySelectionView.setEnabled(false);
2058: Main.this .ruleView.setEnabled(false);
2059: setToolBarDisabled();
2060: } else {
2061: // disable the whole main window ...
2062: Main.this .setEnabled(false);
2063: }
2064: }
2065:
2066: /** invoked if a frame that wants modal access is closed */
2067: public void modalDialogClosed(GUIEvent e) {
2068: if (e.getSource() instanceof ApplyTacletDialog) {
2069: // enable all previously diabled elements ...
2070: enableMenuBar(Main.this .getJMenuBar(), true);
2071: Main.this .goalView.setEnabled(true);
2072: Main.this .proofView.setEnabled(true);
2073: Main.this .openGoalsView.setEnabled(true);
2074: Main.this .userConstraintView.setEnabled(true);
2075: Main.this .strategySelectionView.setEnabled(true);
2076: Main.this .ruleView.setEnabled(true);
2077: setToolBarEnabled();
2078: } else {
2079: // enable the whole main window ...
2080: Main.this .setEnabled(true);
2081: }
2082: }
2083:
2084: public void shutDown(GUIEvent e) {
2085: Main.this .notify(new ExitKeYEvent());
2086: Main.this .setVisible(false);
2087: }
2088:
2089: }
2090:
2091: /**
2092: * set to true if the view of the current goal should not be updated
2093: */
2094: private boolean disableCurrentGoalView = false;
2095:
2096: private synchronized void setProofNodeDisplay() {
2097: if (!disableCurrentGoalView) {
2098: Goal goal;
2099: try {
2100: goal = mediator().getSelectedGoal();
2101: } catch (IllegalStateException e) { // there is no proof (yet)
2102: return;
2103: }
2104: if (goal != null
2105: && !mediator.getUserConstraint().displayClosed(
2106: goal.node())) {
2107: printSequentView(goal.sequent());
2108: } else {
2109: NonGoalInfoView innerNodeView = new NonGoalInfoView(
2110: mediator().getSelectedNode(), mediator());
2111: updateGoalView("Inner Node", innerNodeView);
2112: }
2113: }
2114: }
2115:
2116: class MainProofListener implements AutoModeListener,
2117: KeYSelectionListener, SettingsListener {
2118:
2119: Logger logger = Logger.getLogger("key.threading");
2120:
2121: Proof proof = null;
2122:
2123: /** focused node has changed */
2124: public synchronized void selectedNodeChanged(KeYSelectionEvent e) {
2125: if (mediator().autoMode())
2126: return;
2127: setProofNodeDisplay();
2128: }
2129:
2130: /**
2131: * the selected proof has changed (e.g. a new proof has been loaded)
2132: */
2133: public synchronized void selectedProofChanged(
2134: KeYSelectionEvent e) {
2135: Debug.out("Main: initialize with new proof");
2136:
2137: if (proof != null) {
2138: proof.getSettings().getStrategySettings()
2139: .removeSettingsListener(this );
2140: }
2141: proof = e.getSource().getSelectedProof();
2142: if (proof != null) {
2143: proof.getSettings().getStrategySettings()
2144: .addSettingsListener(this );
2145: }
2146:
2147: disableCurrentGoalView = false;
2148: goalView.setViewportView(null);
2149:
2150: if (userConstraint != null)
2151: userConstraint
2152: .removeConstraintTableListener(constraintListener);
2153:
2154: userConstraint = (proof != null) ? proof
2155: .getUserConstraint() : null;
2156:
2157: if (userConstraint != null)
2158: userConstraint
2159: .addConstraintTableListener(constraintListener);
2160: setProofNodeDisplay();
2161: makePrettyView();
2162: // update label of autoModeButton and update decproc options list
2163: updateDecisionProcedureButton();
2164: DecisionProcedureSettings currentSetting = ProofSettings.DEFAULT_SETTINGS
2165: .getDecisionProcedureSettings();
2166: if (proof != null) {
2167: currentSetting = proof.getSettings()
2168: .getDecisionProcedureSettings();
2169: }
2170: simplifyButton.setSelected(currentSetting.useSimplify());
2171: icsButton.setSelected(currentSetting.useICS());
2172: cvcLiteButton.setSelected(currentSetting.useCVCLite());
2173: cvc3Button.setSelected(currentSetting.useCVC3());
2174: svcButton.setSelected(currentSetting.useSVC());
2175: yicesButton.setSelected(currentSetting.useYices());
2176: smtButton.setSelected(currentSetting.useSMT_Translation());
2177: smtUseQuantifiersOption.setSelected(currentSetting
2178: .useQuantifiers());
2179: smtBenchmarkArchivingOption.setSelected(currentSetting
2180: .doBenchmarkArchiving());
2181: smtZipProblemDirOption.setSelected(currentSetting
2182: .doZipProblemDir());
2183:
2184: // Inform the decproc classes that the selected proof has changed!
2185: DecisionProcedureSmtAuflia.fireSelectedProofChanged(proof);
2186: }
2187:
2188: /**
2189: * invoked if automatic execution has started
2190: */
2191: public synchronized void autoModeStarted(ProofEvent e) {
2192: logger.warn("Automode started");
2193: disableCurrentGoalView = true;
2194: mediator().removeKeYSelectionListener(proofListener);
2195: freezeExceptAutoModeButton();
2196: }
2197:
2198: /**
2199: * invoked if automatic execution has stopped
2200: */
2201: public synchronized void autoModeStopped(ProofEvent e) {
2202: logger.warn("Automode stopped");
2203: if (logger.isDebugEnabled()) {
2204: logger.debug("From " + Debug.stackTrace());
2205: }
2206: unfreezeExceptAutoModeButton();
2207: disableCurrentGoalView = false;
2208: setProofNodeDisplay();
2209: mediator().addKeYSelectionListener(proofListener);
2210: }
2211:
2212: /** invoked when the strategy of a proof has been changed */
2213: public synchronized void settingsChanged(GUIEvent e) {
2214: if (proof.getSettings().getStrategySettings() == (StrategySettings) e
2215: .getSource()) {
2216: // updateAutoModeConfigButton();
2217: }
2218: }
2219:
2220: }
2221:
2222: class DecisionProcButtonListener implements ActionListener {
2223: public void actionPerformed(ActionEvent e) {
2224: Proof currentProof = mediator.getProof();
2225: ProofSettings currentSettings = ProofSettings.DEFAULT_SETTINGS;
2226: if (currentProof != null)
2227: currentSettings = currentProof.getSettings();
2228:
2229: if (e.getSource() == simplifyButton) {
2230: currentSettings.getDecisionProcedureSettings()
2231: .setDecisionProcedure(
2232: DecisionProcedureSettings.SIMPLIFY);
2233: } else if (e.getSource() == icsButton) {
2234: currentSettings.getDecisionProcedureSettings()
2235: .setDecisionProcedure(
2236: DecisionProcedureSettings.ICS);
2237: } else if (e.getSource() == cvcLiteButton) {
2238: currentSettings.getDecisionProcedureSettings()
2239: .setDecisionProcedure(
2240: DecisionProcedureSettings.CVCLite);
2241: } else if (e.getSource() == cvc3Button) {
2242: currentSettings.getDecisionProcedureSettings()
2243: .setDecisionProcedure(
2244: DecisionProcedureSettings.CVC3);
2245: } else if (e.getSource() == svcButton) {
2246: currentSettings.getDecisionProcedureSettings()
2247: .setDecisionProcedure(
2248: DecisionProcedureSettings.SVC);
2249: } else if (e.getSource() == yicesButton) {
2250: currentSettings.getDecisionProcedureSettings()
2251: .setDecisionProcedure(
2252: DecisionProcedureSettings.YICES);
2253: } else if (e.getSource() == smtButton) {
2254: currentSettings.getDecisionProcedureSettings()
2255: .setDecisionProcedure(
2256: DecisionProcedureSettings.SMT);
2257: } else if (e.getSource() == smtUseQuantifiersOption) {
2258: boolean b = ((JCheckBoxMenuItem) e.getSource())
2259: .isSelected();
2260: currentSettings.getDecisionProcedureSettings()
2261: .setUseQuantifier(b);
2262: ProofSettings.DEFAULT_SETTINGS
2263: .getDecisionProcedureSettings()
2264: .setUseQuantifier(b);
2265: } else if (e.getSource() == smtBenchmarkArchivingOption) {
2266: boolean b = ((JCheckBoxMenuItem) e.getSource())
2267: .isSelected();
2268: currentSettings.getDecisionProcedureSettings()
2269: .setDoBenchmarkArchiving(b);
2270: ProofSettings.DEFAULT_SETTINGS
2271: .getDecisionProcedureSettings()
2272: .setDoBenchmarkArchiving(b);
2273: } else if (e.getSource() == smtZipProblemDirOption) {
2274: boolean b = ((JCheckBoxMenuItem) e.getSource())
2275: .isSelected();
2276: currentSettings.getDecisionProcedureSettings()
2277: .setDoZipProblemDir(b);
2278: ProofSettings.DEFAULT_SETTINGS
2279: .getDecisionProcedureSettings()
2280: .setDoZipProblemDir(b);
2281: }
2282: updateDecisionProcedureButton();
2283: if (currentProof != null) {
2284: ProofSettings.DEFAULT_SETTINGS
2285: .getDecisionProcedureSettings()
2286: .setDecisionProcedure(
2287: currentSettings
2288: .getDecisionProcedureSettings()
2289: .getDecisionProcedure());
2290: }
2291: }
2292: }
2293:
2294: public void updateDecisionProcedureButton() {
2295: Proof currentProof = mediator.getProof();
2296: DecisionProcedureSettings decSettings = (currentProof == null) ? ProofSettings.DEFAULT_SETTINGS
2297: .getDecisionProcedureSettings()
2298: : currentProof.getSettings()
2299: .getDecisionProcedureSettings();
2300: if (decSettings.useSimplify()) {
2301: decisionProcedureButton.setIcon(IconFactory
2302: .simplifyLogo(toolbarIconSize));
2303: decisionProcedureButton.setToolTipText("Run Simplify");
2304: decisionProcedureButton.setText("Run Simplify");
2305: } else if (decSettings.useICS()) {
2306: decisionProcedureButton.setIcon(IconFactory
2307: .icsLogo(toolbarIconSize));
2308: decisionProcedureButton.setToolTipText("Run ICS");
2309: decisionProcedureButton.setText("Run ICS");
2310: } else if (decSettings.useCVCLite()) {
2311: decisionProcedureButton.setIcon(IconFactory
2312: .icsLogo(toolbarIconSize));
2313: decisionProcedureButton.setToolTipText("Run CVCLite");
2314: decisionProcedureButton.setText("Run CVCLite");
2315: } else if (decSettings.useCVC3()) {
2316: decisionProcedureButton.setIcon(IconFactory
2317: .icsLogo(toolbarIconSize));
2318: decisionProcedureButton.setToolTipText("Run CVC3");
2319: decisionProcedureButton.setText("Run CVC3");
2320: } else if (decSettings.useSVC()) {
2321: decisionProcedureButton.setIcon(IconFactory
2322: .icsLogo(toolbarIconSize));
2323: decisionProcedureButton.setToolTipText("Run SVC");
2324: decisionProcedureButton.setText("Run SVC");
2325: } else if (decSettings.useYices()) {
2326: decisionProcedureButton.setIcon(IconFactory
2327: .icsLogo(toolbarIconSize));
2328: decisionProcedureButton.setToolTipText("Run Yices");
2329: decisionProcedureButton.setText("Run Yices");
2330: } else if (decSettings.useSMT_Translation()) {
2331: decisionProcedureButton.setIcon(IconFactory
2332: .icsLogo(toolbarIconSize));
2333: decisionProcedureButton
2334: .setToolTipText("Run SMT Translation");
2335: decisionProcedureButton.setText("Run SMT Translation");
2336: }
2337: }
2338:
2339: class MainConstraintTableListener implements
2340: ConstraintTableListener {
2341: public void constraintChanged(ConstraintTableEvent e) {
2342: setProofNodeDisplay();
2343: }
2344: }
2345:
2346: class MainTaskListener implements ProverTaskListener { // XXX
2347: public void taskStarted(String message, int size) {
2348: final MainStatusLine sl = getStatusLine();
2349: sl.reset();
2350: if (size > 0) {
2351: sl.setProgressPanelVisible(true);
2352: getProgressMonitor().setMaximum(size);
2353: }
2354: sl.setStatusText(message);
2355: }
2356:
2357: public void taskProgress(int position) {
2358: getProgressMonitor().setProgress(position);
2359: }
2360:
2361: public void taskFinished() {
2362: final MainStatusLine sl = getStatusLine();
2363: sl.reset();
2364: }
2365: }
2366:
2367: public static void evaluateOptions(String[] opt) {
2368: int index = 0;
2369: while (opt.length > index) {
2370: if ((new File(opt[index])).exists()) {
2371: fileNameOnStartUp = opt[index];
2372: } else {
2373: opt[index] = opt[index].toUpperCase();
2374: if (opt[index].equals("NO_DEBUG")) {
2375: de.uka.ilkd.key.util.Debug.ENABLE_DEBUG = false;
2376: } else if (opt[index].equals("DEBUG")) {
2377: de.uka.ilkd.key.util.Debug.ENABLE_DEBUG = true;
2378: } else if (opt[index].equals("NO_ASSERTION")) {
2379: de.uka.ilkd.key.util.Debug.ENABLE_ASSERTION = false;
2380: } else if (opt[index].equals("ASSERTION")) {
2381: de.uka.ilkd.key.util.Debug.ENABLE_ASSERTION = true;
2382: } else if (opt[index].equals("NO_JMLSPECS")) {
2383: jmlSpecs = false;
2384: } else if (opt[index].equals("AUTO")) {
2385: batchMode = true;
2386: } else if (opt[index].equals("TESTING")
2387: || opt[index].equals("UNIT")) {
2388: if (opt[index].equals("TESTING")) {
2389: testStandalone = true;
2390: visible = false;
2391: }
2392: System.out.println("VBT optimizations enabled ...");
2393:
2394: final Profile p = new JavaTestGenerationProfile(
2395: null);
2396:
2397: if (index + 1 < opt.length
2398: && opt[index + 1].toUpperCase().equals(
2399: "LOOP")) {
2400: p
2401: .setSelectedGoalChooserBuilder(BalancedGoalChooserBuilder.NAME);
2402: System.out
2403: .println("Balanced loop unwinding ...");
2404: index++;
2405: }
2406: ProofSettings.DEFAULT_SETTINGS.setProfile(p);
2407: p.updateSettings(ProofSettings.DEFAULT_SETTINGS);
2408: testMode = true;
2409: } else if (opt[index].equals("DEBUGGER")) {
2410: System.out
2411: .println("Symbolic Execution Debugger Mode enabled ...");
2412: final Profile p = new DebuggerProfile(null);
2413: if (index + 1 < opt.length
2414: && opt[index + 1].equals("LOOP")) {
2415: p
2416: .setSelectedGoalChooserBuilder(BalancedGoalChooserBuilder.NAME);
2417: //System.out.println("Balanced loop unwinding ...");
2418: index++;
2419: }
2420: ProofSettings.DEFAULT_SETTINGS.setProfile(p);
2421: p.updateSettings(ProofSettings.DEFAULT_SETTINGS);
2422: testMode = true;
2423: }
2424:
2425: else if (opt[index].equals("FOL")) {
2426: ProofSettings.DEFAULT_SETTINGS
2427: .setProfile(new PureFOLProfile());
2428: } else if (opt[index].equals("TIMEOUT")) {
2429: long timeout = -1;
2430: try {
2431: timeout = Long.parseLong(opt[index + 1]);
2432: } catch (NumberFormatException nfe) {
2433: System.out
2434: .println("Illegal timeout (must be a number >=-1).");
2435: System.exit(-1);
2436: }
2437: if (timeout < -1) {
2438: System.out
2439: .println("Illegal timeout (must be a number >=-1).");
2440: System.exit(-1);
2441: }
2442: index++;
2443: ProofSettings.DEFAULT_SETTINGS
2444: .getStrategySettings().setTimeout(timeout);
2445: } else if (opt[index].equals("PRINT_STATISTICS")) {
2446: if (!(opt.length > index + 1))
2447: printUsageAndExit();
2448: statisticsFile = opt[index + 1];
2449: ++index;
2450: } else {
2451: printUsageAndExit();
2452: }
2453: }
2454: index++;
2455: }
2456: if (Debug.ENABLE_DEBUG) {
2457: System.out.println("Running in debug mode ...");
2458: } else {
2459: System.out.println("Running in normal mode ...");
2460: }
2461: if (Debug.ENABLE_ASSERTION) {
2462: System.out.println("Using assertions ...");
2463: } else {
2464: System.out.println("Not using assertions ...");
2465: }
2466: }
2467:
2468: private static void printUsageAndExit() {
2469: System.out.println("File not found or unrecognized option.\n");
2470: System.out.println("Possible parameters are (* = default): ");
2471: System.out
2472: .println(" no_debug : disables debug mode (*)");
2473: System.out.println(" debug : enables debug mode");
2474: System.out.println(" no_assertion : disables assertions");
2475: System.out
2476: .println(" assertion : enables assertions (*)");
2477: System.out
2478: .println(" no_jmlspecs : disables parsing JML specifications");
2479: System.out
2480: .println(" unit [loop] : unit test generation mode (optional argument loop to "
2481: + "enable balanced loop unwinding)");
2482: System.out
2483: .println(" auto : start prove procedure after initialisation");
2484: System.out
2485: .println(" testing : starts the prover with a simple test generation oriented user interface");
2486: System.out.println(" print_statistics <filename>");
2487: System.out
2488: .println(" : in auto mode, output nr. of rule applications and time spent");
2489: System.out
2490: .println(" fol : use FOL profile (no program or update rules)");
2491: System.out.println(" timeout <time in ms>");
2492: System.out
2493: .println(" : set maximal time for rule "
2494: + "application in ms (-1 disables timeout)");
2495: System.out.println(" <filename> : loads a .key file");
2496: System.exit(-1);
2497: }
2498:
2499: /** Glass pane that only delivers events for the status line (i.e. the abort button)
2500: *
2501: * This has been partly taken from the GlassPaneDemo of the Java Tutorial
2502: */
2503: class BlockingGlassPane extends JComponent {
2504: GlassPaneListener listener;
2505:
2506: public BlockingGlassPane(Container contentPane) {
2507: setCursor(new Cursor(Cursor.WAIT_CURSOR));
2508:
2509: listener = new GlassPaneListener(this , contentPane);
2510: addMouseListener(listener);
2511: addMouseMotionListener(listener);
2512: }
2513: }
2514:
2515: /**
2516: * Mouse listener for the glass pane that only delivers events for the status line (i.e. the
2517: * abort button)
2518: *
2519: * This has been partly taken from the GlassPaneDemo of the Java Tutorial
2520: */
2521: class GlassPaneListener extends MouseInputAdapter {
2522: Component currentComponent = null;
2523: Component glassPane;
2524: Container contentPane;
2525:
2526: public GlassPaneListener(Component glassPane,
2527: Container contentPane) {
2528: this .glassPane = glassPane;
2529: this .contentPane = contentPane;
2530: }
2531:
2532: public void mouseMoved(MouseEvent e) {
2533: redispatchMouseEvent(e);
2534: }
2535:
2536: /*
2537: * We must forward at least the mouse drags that started with mouse presses over the check box.
2538: * Otherwise, when the user presses the check box then drags off, the check box isn't disarmed --
2539: * it keeps its dark gray background or whatever its L&F uses to indicate that the button is
2540: * currently being pressed.
2541: */
2542: public void mouseDragged(MouseEvent e) {
2543: redispatchMouseEvent(e);
2544: }
2545:
2546: public void mouseClicked(MouseEvent e) {
2547: redispatchMouseEvent(e);
2548: }
2549:
2550: public void mouseEntered(MouseEvent e) {
2551: redispatchMouseEvent(e);
2552: }
2553:
2554: public void mouseExited(MouseEvent e) {
2555: redispatchMouseEvent(e);
2556: }
2557:
2558: public void mousePressed(MouseEvent e) {
2559: redispatchMouseEvent(e);
2560: }
2561:
2562: public void mouseReleased(MouseEvent e) {
2563: redispatchMouseEvent(e);
2564: currentComponent = null;
2565: }
2566:
2567: private void redispatchMouseEvent(MouseEvent e) {
2568: if (currentComponent != null) {
2569: dispatchForCurrentComponent(e);
2570: } else {
2571: int eventID = e.getID();
2572: Point glassPanePoint = e.getPoint();
2573:
2574: Point containerPoint = SwingUtilities.convertPoint(
2575: glassPane, glassPanePoint, contentPane);
2576: Component component = SwingUtilities
2577: .getDeepestComponentAt(contentPane,
2578: containerPoint.x, containerPoint.y);
2579:
2580: if (eventID == MouseEvent.MOUSE_PRESSED
2581: && isLiveComponent(component)) {
2582: currentComponent = component;
2583: dispatchForCurrentComponent(e);
2584: }
2585: }
2586: }
2587:
2588: private boolean isLiveComponent(Component c) {
2589: // this is not the most elegant way to identify the right
2590: // components, but it scales well ;-)
2591: while (c != null) {
2592: if ((c instanceof JComponent)
2593: && AUTO_MODE_TEXT.equals(((JComponent) c)
2594: .getToolTipText()))
2595: return true;
2596: c = c.getParent();
2597: }
2598: return false;
2599: }
2600:
2601: private void dispatchForCurrentComponent(MouseEvent e) {
2602: Point glassPanePoint = e.getPoint();
2603: Point componentPoint = SwingUtilities.convertPoint(
2604: glassPane, glassPanePoint, currentComponent);
2605: currentComponent.dispatchEvent(new MouseEvent(
2606: currentComponent, e.getID(), e.getWhen(), e
2607: .getModifiers(), componentPoint.x,
2608: componentPoint.y, e.getClickCount(), e
2609: .isPopupTrigger()));
2610: }
2611: }
2612:
2613: private final class CreateUnitTestAction extends AbstractAction {
2614: final Icon icon = IconFactory.junitLogo(toolbarIconSize);
2615:
2616: public CreateUnitTestAction() {
2617: putValue(NAME, "Create Unittests");
2618: putValue(Action.SHORT_DESCRIPTION,
2619: "Create JUnit test cases from proof.");
2620: putValue(Action.SMALL_ICON, icon);
2621:
2622: setEnabled(mediator.getSelectedProof() != null);
2623:
2624: mediator
2625: .addKeYSelectionListener(new KeYSelectionListener() {
2626: /** focused node has changed */
2627: public void selectedNodeChanged(
2628: KeYSelectionEvent e) {
2629: }
2630:
2631: /**
2632: * the selected proof has changed. Enable or disable action depending whether a
2633: * proof is available or not
2634: */
2635: public void selectedProofChanged(
2636: KeYSelectionEvent e) {
2637: setEnabled(e.getSource().getSelectedProof() != null);
2638: }
2639: });
2640: }
2641:
2642: public void actionPerformed(ActionEvent e) {
2643: MethodSelectionDialog.getInstance(mediator);
2644: }
2645: }
2646:
2647: private final class AutoModeAction extends AbstractAction {
2648:
2649: final Icon startLogo = IconFactory
2650: .autoModeStartLogo(toolbarIconSize);
2651: final Icon stopLogo = IconFactory
2652: .autoModeStopLogo(toolbarIconSize);
2653:
2654: private Proof associatedProof;
2655:
2656: private final ProofTreeListener ptl = new ProofTreeAdapter() {
2657:
2658: public void proofStructureChanged(ProofTreeEvent e) {
2659: if (e.getSource() == associatedProof) {
2660: enable();
2661: }
2662:
2663: }
2664:
2665: public void proofClosed(ProofTreeEvent e) {
2666: if (e.getSource() == associatedProof) {
2667: enable();
2668: }
2669: }
2670:
2671: public void proofGoalsAdded(ProofTreeEvent e) {
2672: Proof p = e.getSource();
2673: ListOfGoal newGoals = e.getGoals();
2674: // Check for a closed goal ...
2675: if ((newGoals.size() == 0) && (!p.closed())) {
2676: // No new goals have been generated ...
2677: setStatusLine("1 goal closed, "
2678: + p.openGoals().size() + " remaining");
2679: }
2680: }
2681: };
2682:
2683: public void enable() {
2684: setEnabled(associatedProof != null
2685: && !associatedProof.closed());
2686: }
2687:
2688: public AutoModeAction() {
2689: putValue("hideActionText", Boolean.TRUE);
2690: putValue(Action.SHORT_DESCRIPTION, AUTO_MODE_TEXT);
2691: putValue(Action.SMALL_ICON, startLogo);
2692:
2693: associatedProof = mediator.getProof();
2694:
2695: enable();
2696:
2697: if (associatedProof != null
2698: && !associatedProof.containsProofTreeListener(ptl)) {
2699: associatedProof.addProofTreeListener(ptl);
2700: }
2701:
2702: mediator
2703: .addKeYSelectionListener(new KeYSelectionListener() {
2704: /** focused node has changed */
2705: public void selectedNodeChanged(
2706: KeYSelectionEvent e) {
2707: }
2708:
2709: /**
2710: * the selected proof has changed. Enable or disable action depending whether a proof is
2711: * available or not
2712: */
2713: public void selectedProofChanged(
2714: KeYSelectionEvent e) {
2715: if (associatedProof != null) {
2716: associatedProof
2717: .removeProofTreeListener(ptl);
2718: }
2719:
2720: associatedProof = e.getSource()
2721: .getSelectedProof();
2722: enable();
2723:
2724: if (associatedProof != null) {
2725: associatedProof
2726: .addProofTreeListener(ptl);
2727: }
2728: }
2729: });
2730:
2731: mediator.addAutoModeListener(new AutoModeListener() {
2732:
2733: /**
2734: * invoked if automatic execution has started
2735: */
2736: public void autoModeStarted(ProofEvent e) {
2737: if (associatedProof != null) {
2738: associatedProof.removeProofTreeListener(ptl);
2739: }
2740: putValue(Action.SMALL_ICON, stopLogo);
2741: }
2742:
2743: /**
2744: * invoked if automatic execution has stopped
2745: */
2746: public void autoModeStopped(ProofEvent e) {
2747: if (associatedProof != null
2748: && associatedProof == e.getSource()
2749: && !associatedProof
2750: .containsProofTreeListener(ptl)) {
2751: associatedProof.addProofTreeListener(ptl);
2752: }
2753: putValue(Action.SMALL_ICON, startLogo);
2754: }
2755:
2756: });
2757:
2758: }
2759:
2760: public void actionPerformed(ActionEvent e) {
2761: // Unfortunately, when clicking the button twice
2762: // (very fast), the glasspane won't be quick
2763: // enough to catch the second event. Therefore
2764: // we make a second check (which is a %%%HACK)
2765: if (!frozen)
2766: mediator().startAutoMode();
2767: else
2768: mediator().stopAutoMode();
2769: }
2770:
2771: }
2772:
2773: public void loadCommandLineFile() {
2774: if (fileNameOnStartUp != null) {
2775: loadProblem(new File(fileNameOnStartUp));
2776: }
2777: }
2778:
2779: public static void main(String[] args) {
2780: System.out.println("\nKeY Version " + VERSION);
2781: System.out.println(COPYRIGHT + "\nKeY is protected by the "
2782: + "GNU General Public License\n");
2783:
2784: // does no harm on non macs
2785: System.setProperty("apple.laf.useScreenMenuBar", "true");
2786:
2787: Main.evaluateOptions(args);
2788: Main key = getInstance(visible);
2789: key.loadCommandLineFile();
2790: if (testStandalone) {
2791: key.unitKeY = new UnitTestGeneratorGui(key);
2792: }
2793: }
2794:
2795: /**
2796: * informs the NotificationManager about an event
2797: *
2798: * @param event
2799: * the NotificationEvent
2800: */
2801: public void notify(NotificationEvent event) {
2802: if (notificationManager != null) {
2803: notificationManager.notify(event);
2804: }
2805: }
2806:
2807: private final static class UnitTestGeneratorGui extends JFrame {
2808:
2809: protected final Main main;
2810: final protected KeYMediator mediator;
2811: private int toolbarIconSize = 15;
2812: private static UnitTestGeneratorGui testGui;
2813: private boolean openDialog = false;
2814: private RecentFileMenu recent = null;
2815: private JButton run;
2816: private JFrame proofList;
2817: private HashMap test2model;
2818: private boolean autoMode = false;
2819:
2820: public static final String AUTO_MODE_TEXT = "Create Tests";
2821:
2822: public UnitTestGeneratorGui(Main main) {
2823: super ("KeY Unit Test Generator");
2824: this .main = main;
2825: mediator = main.mediator();
2826: test2model = new HashMap();
2827: setIconImage(IconFactory.keyLogo());
2828: createProofList();
2829: layoutGui();
2830: setLocation(70, 70);
2831: addWindowListener(new UnitTestGeneratorGuiListener());
2832: pack();
2833: Dimension d = getSize();
2834: d.setSize(400, (int) d.getHeight() + 3);
2835: setSize(d);
2836: setVisible(true);
2837: testGui = this ;
2838: }
2839:
2840: protected void createProofList() {
2841: proofList = new JFrame("Test Requirements");
2842: proofList.getContentPane().add(main.proofListView);
2843: proofList.setSize(400, 170);
2844: proofList.addWindowListener(new WindowAdapter() {
2845: public void windowClosing(WindowEvent e) {
2846: proofList.setVisible(false);
2847: }
2848: });
2849: proofList.setVisible(true);
2850: }
2851:
2852: protected void layoutGui() {
2853: setJMenuBar(new JMenuBar());
2854: getJMenuBar().add(createFileMenu());
2855: getJMenuBar().add(createToolsMenu());
2856: getJMenuBar().add(createOptionsMenu());
2857: getJMenuBar().add(Box.createHorizontalGlue());
2858: getJMenuBar().add(main.createHelpMenu());
2859: run = new JButton(new AutoModeAction());
2860: getContentPane().setLayout(
2861: new BoxLayout(getContentPane(), BoxLayout.Y_AXIS));
2862: JPanel buttonPanel = new JPanel();
2863: buttonPanel.add(run);
2864: JPanel sliderPanel = new JPanel();
2865: sliderPanel.setLayout(new BoxLayout(sliderPanel,
2866: BoxLayout.Y_AXIS));
2867: sliderPanel.add(new MaxRuleAppSlider(mediator));
2868: buttonPanel.add(sliderPanel);
2869: buttonPanel.setLayout(new BoxLayout(buttonPanel,
2870: BoxLayout.X_AXIS));
2871: getContentPane().add(buttonPanel);
2872: MainStatusLine msl = main.getStatusLine();
2873: getContentPane().add(msl);
2874: }
2875:
2876: class UnitTestGeneratorGuiListener extends WindowAdapter {
2877: public void windowClosing(WindowEvent e) {
2878: main.exitMain();
2879: }
2880: }
2881:
2882: private void runTest(String testPath, String modelDir)
2883: throws IOException {
2884: String testDir = testPath.substring(0, testPath
2885: .lastIndexOf(File.separator))
2886: + modelDir;
2887: String test = testPath.substring(testPath
2888: .lastIndexOf(File.separator) + 1);
2889: Runtime.getRuntime().exec("cp " + testPath + " " + testDir);
2890: File testDirFile = new File(testDir);
2891: Runtime rt = Runtime.getRuntime();
2892: Process compile = rt.exec("javac " + test, null,
2893: testDirFile);
2894: String compileError = read(compile.getErrorStream()).trim();
2895: if (!"".equals(compileError)) {
2896: throw new RuntimeException(compileError);
2897: }
2898:
2899: Process runJUnit = rt.exec("java junit.swingui.TestRunner "
2900: + test.substring(0, test.lastIndexOf(".")), null,
2901: testDirFile);
2902: String junitError = read(runJUnit.getErrorStream());
2903: if (!"".equals(junitError)) {
2904: throw new RuntimeException(junitError);
2905: }
2906: }
2907:
2908: private void createTestSelectionWindow() {
2909: JDialog tsw = new JDialog(this , "Select Test Case");
2910: tsw.getContentPane().setLayout(
2911: new BoxLayout(tsw.getContentPane(),
2912: BoxLayout.Y_AXIS));
2913: final JList testList = new JList();
2914: testList.setListData(bubbleSortTests(createTestArray()));
2915:
2916: JScrollPane testListScroll = new JScrollPane(
2917: JScrollPane.VERTICAL_SCROLLBAR_AS_NEEDED,
2918: JScrollPane.HORIZONTAL_SCROLLBAR_AS_NEEDED);
2919: testListScroll.getViewport().setView(testList);
2920: testListScroll.setBorder(new TitledBorder("Created Tests"));
2921: testListScroll.setMinimumSize(new java.awt.Dimension(150,
2922: 400));
2923: tsw.getContentPane().add(testListScroll);
2924:
2925: JButton test = new JButton("Run Test");
2926: test.addActionListener(new ActionListener() {
2927: public void actionPerformed(ActionEvent e) {
2928: if (testList.getSelectedValue() == null) {
2929: JOptionPane.showMessageDialog(null,
2930: "You must select a test first!",
2931: "No Test Selected",
2932: JOptionPane.ERROR_MESSAGE);
2933: } else {
2934: TestAndModel tam = (TestAndModel) testList
2935: .getSelectedValue();
2936: try {
2937: runTest(tam.test, tam.model);
2938: } catch (Exception exc) {
2939: ExtList l = new ExtList();
2940: l.add(exc);
2941: new ExceptionDialog(testGui, l);
2942: }
2943: }
2944: }
2945: });
2946: tsw.getContentPane().add(test);
2947: tsw.pack();
2948: tsw.setVisible(true);
2949: }
2950:
2951: private Object[] bubbleSortTests(Object[] tams) {
2952: boolean sorted = false;
2953: while (!sorted) {
2954: sorted = true;
2955: for (int i = 0; i < tams.length - 1; i++) {
2956: if (tams[i].toString().compareTo(
2957: tams[i + 1].toString()) > 0) {
2958: Object temp = tams[i];
2959: tams[i] = tams[i + 1];
2960: tams[i + 1] = temp;
2961: sorted = false;
2962: }
2963: }
2964: }
2965: return tams;
2966: }
2967:
2968: private Object[] createTestArray() {
2969: Iterator it = test2model.entrySet().iterator();
2970: Vector v = new Vector();
2971: while (it.hasNext()) {
2972: Map.Entry e = (Map.Entry) it.next();
2973: String test = ((StringBuffer) e.getKey()).toString();
2974: String model = (String) e.getValue();
2975: while (!"".equals(test.trim())) {
2976: v.add(new TestAndModel(test.substring(0, test
2977: .indexOf(" ")), model));
2978: test = test.substring(test.indexOf(" ") + 1);
2979: }
2980: }
2981: return v.toArray();
2982: }
2983:
2984: class TestAndModel {
2985: public String test;
2986: public String model;
2987:
2988: public TestAndModel(String test, String model) {
2989: this .test = test;
2990: this .model = model;
2991: }
2992:
2993: public String toString() {
2994: return test;
2995: }
2996: }
2997:
2998: /** Read the input until end of file and return contents in a
2999: * single string containing all line breaks. */
3000: protected String read(InputStream in) throws IOException {
3001: String lineSeparator = System.getProperty("line.separator");
3002: BufferedReader reader = new BufferedReader(
3003: new InputStreamReader(in));
3004: StringBuffer sb = new StringBuffer();
3005: String line;
3006: while ((line = reader.readLine()) != null) {
3007: sb.append(line).append(lineSeparator);
3008: }
3009: return sb.toString();
3010: }
3011:
3012: protected JMenu createFileMenu() {
3013: JMenu fileMenu = new JMenu("File");
3014: fileMenu.setMnemonic(KeyEvent.VK_F);
3015:
3016: JMenuItem load = new JMenuItem();
3017: load.setAction(openFileAction);
3018:
3019: fileMenu.add(load);
3020:
3021: JMenuItem exit = new JMenuItem("Exit");
3022: exit.setAccelerator(KeyStroke.getKeyStroke(KeyEvent.VK_Q,
3023: ActionEvent.CTRL_MASK));
3024: exit.addActionListener(new ActionListener() {
3025: public void actionPerformed(ActionEvent e) {
3026: main.exitMain();
3027: }
3028: });
3029:
3030: fileMenu.addSeparator();
3031:
3032: recent = new RecentFileMenu(new ActionListener() {
3033: public void actionPerformed(ActionEvent e) {
3034: main
3035: .loadProblem(new File(recent
3036: .getAbsolutePath((JMenuItem) e
3037: .getSource())));
3038: }
3039: }, MAX_RECENT_FILES, null);
3040:
3041: recent.load(PathConfig.RECENT_FILES_STORAGE);
3042:
3043: fileMenu.add(recent.getMenu());
3044:
3045: fileMenu.addSeparator();
3046: fileMenu.add(exit);
3047: return fileMenu;
3048: }
3049:
3050: protected JMenu createToolsMenu() {
3051: JMenu toolsMenu = new JMenu("Tools");
3052: JMenuItem specificationBrowser = new JMenuItem(
3053: "JML Specification Browser...");
3054: specificationBrowser.setAccelerator(KeyStroke.getKeyStroke(
3055: KeyEvent.VK_J, ActionEvent.CTRL_MASK));
3056: specificationBrowser
3057: .addActionListener(new ActionListener() {
3058: public void actionPerformed(ActionEvent e) {
3059: main.showSpecBrowser();
3060: }
3061: });
3062: toolsMenu.add(specificationBrowser);
3063:
3064: final JMenuItem showProver = new JMenuItem("Show Prover",
3065: IconFactory.keyLogo(toolbarIconSize,
3066: toolbarIconSize));
3067: showProver.setAccelerator(KeyStroke.getKeyStroke(
3068: KeyEvent.VK_P, ActionEvent.CTRL_MASK));
3069: showProver.addActionListener(new ActionListener() {
3070: public void actionPerformed(ActionEvent e) {
3071: Main.visible = !Main.visible;
3072: main.setVisible(Main.visible);
3073: showProver.setText(Main.visible ? "Hide Prover"
3074: : "Show Prover");
3075: }
3076: });
3077: toolsMenu.add(showProver);
3078:
3079: final JMenuItem runTest = new JMenuItem(
3080: "Run Created Tests", IconFactory
3081: .junitLogo(toolbarIconSize));
3082: runTest.addActionListener(new ActionListener() {
3083: public void actionPerformed(ActionEvent e) {
3084: createTestSelectionWindow();
3085: }
3086: });
3087: toolsMenu.add(runTest);
3088:
3089: final JMenuItem showRequirements = new JMenuItem(
3090: "Hide Test Requirements");
3091: showRequirements.addActionListener(new ActionListener() {
3092: public void actionPerformed(ActionEvent e) {
3093: proofList.setVisible(!proofList.isVisible());
3094: showRequirements
3095: .setText(proofList.isVisible() ? "Hide Test Requirements"
3096: : "Show Test Requirements");
3097: }
3098: });
3099: toolsMenu.add(showRequirements);
3100:
3101: toolsMenu.addMenuListener(new MenuListener() {
3102: public void menuCanceled(MenuEvent arg0) {
3103: }
3104:
3105: public void menuDeselected(MenuEvent arg0) {
3106: }
3107:
3108: public void menuSelected(MenuEvent arg0) {
3109: showProver.setText(Main.visible ? "Hide Prover"
3110: : "Show Prover");
3111: showRequirements
3112: .setText(proofList.isVisible() ? "Hide Test Requirements"
3113: : "Show Test Requirements");
3114: }
3115: });
3116: return toolsMenu;
3117: }
3118:
3119: protected JMenu createOptionsMenu() {
3120: JMenu options = new JMenu("Options");
3121: options.setMnemonic(KeyEvent.VK_O);
3122: JMenuItem choiceItem = new JMenuItem(
3123: "Taclet options defaults");
3124: choiceItem.setAccelerator(KeyStroke.getKeyStroke(
3125: KeyEvent.VK_T, ActionEvent.CTRL_MASK));
3126:
3127: choiceItem.addActionListener(new ActionListener() {
3128: public void actionPerformed(ActionEvent e) {
3129: main.selectChoices();
3130: }
3131: });
3132: options.add(choiceItem);
3133:
3134: ButtonGroup decisionProcGroup = new ButtonGroup();
3135:
3136: JMenu decisionProcedureOption = new JMenu(
3137: "Decision Procedure Config");
3138: setupDecisionProcedureGroup(decisionProcGroup,
3139: decisionProcedureOption);
3140: options.add(decisionProcedureOption);
3141:
3142: final JRadioButtonMenuItem completeEx = new JRadioButtonMenuItem(
3143: "Require Complete Execution", false);
3144: completeEx
3145: .setToolTipText("Use only completely executed traces for test"
3146: + " generation.");
3147: completeEx
3148: .setSelected(UnitTestBuilder.requireCompleteExecution);
3149: completeEx.addActionListener(new ActionListener() {
3150: public void actionPerformed(ActionEvent e) {
3151: UnitTestBuilder.requireCompleteExecution = completeEx
3152: .isSelected();
3153: }
3154: });
3155: options.add(completeEx);
3156:
3157: final JRadioButtonMenuItem methodSelectionButton = new JRadioButtonMenuItem(
3158: "Method Selection Dialog", false);
3159: methodSelectionButton
3160: .addActionListener(new ActionListener() {
3161: public void actionPerformed(ActionEvent e) {
3162: openDialog = methodSelectionButton
3163: .isSelected();
3164: }
3165: });
3166: methodSelectionButton.setToolTipText("<html><pre>"
3167: + "If checked, a dialog for selecting"
3168: + " method calls that the created test shall cover"
3169: + "\nopens after "
3170: + "termination of the symbolic execution.</pre>");
3171: options.add(methodSelectionButton);
3172:
3173: return options;
3174: }
3175:
3176: private void setupDecisionProcedureGroup(
3177: ButtonGroup decisionProcGroup,
3178: JMenu decisionProcedureOption) {
3179: final JRadioButtonMenuItem simplifyButton = new JRadioButtonMenuItem(
3180: "Simplify", ProofSettings.DEFAULT_SETTINGS
3181: .getDecisionProcedureSettings()
3182: .useSimplifyForTest());
3183: decisionProcGroup.add(simplifyButton);
3184: decisionProcedureOption.add(simplifyButton);
3185:
3186: simplifyButton.addActionListener(new ActionListener() {
3187: public void actionPerformed(ActionEvent e) {
3188: ModelGenerator.decProdForTestGen = ModelGenerator.SIMPLIFY;
3189: ProofSettings.DEFAULT_SETTINGS
3190: .getDecisionProcedureSettings()
3191: .setDecisionProcedureForTest(
3192: DecisionProcedureSettings.SIMPLIFY);
3193: }
3194: });
3195:
3196: final JRadioButtonMenuItem cogentButton = new JRadioButtonMenuItem(
3197: "Cogent", ProofSettings.DEFAULT_SETTINGS
3198: .getDecisionProcedureSettings()
3199: .useCogentForTest());
3200: decisionProcGroup.add(cogentButton);
3201: decisionProcedureOption.add(cogentButton);
3202:
3203: cogentButton.addActionListener(new ActionListener() {
3204: public void actionPerformed(ActionEvent e) {
3205: ModelGenerator.decProdForTestGen = ModelGenerator.COGENT;
3206: ProofSettings.DEFAULT_SETTINGS
3207: .getDecisionProcedureSettings()
3208: .setDecisionProcedureForTest(
3209: DecisionProcedureSettings.COGENT);
3210: }
3211: });
3212:
3213: // In case no decision procedure settings exist yet (for instance if
3214: // the .key directory was deleted):
3215: if (!ProofSettings.DEFAULT_SETTINGS
3216: .getDecisionProcedureSettings()
3217: .useSimplifyForTest()
3218: && !ProofSettings.DEFAULT_SETTINGS
3219: .getDecisionProcedureSettings()
3220: .useCogentForTest()) {
3221: simplifyButton
3222: .setSelected(ModelGenerator.decProdForTestGen == ModelGenerator.SIMPLIFY);
3223: cogentButton
3224: .setSelected(ModelGenerator.decProdForTestGen == ModelGenerator.COGENT);
3225: }
3226: // MethodSelectionDialog can change dec. proc. settings. Therefore
3227: // this is necessary:
3228: decisionProcedureOption.addMenuListener(new MenuListener() {
3229: public void menuCanceled(MenuEvent arg0) {
3230: }
3231:
3232: public void menuDeselected(MenuEvent arg0) {
3233: }
3234:
3235: public void menuSelected(MenuEvent arg0) {
3236: simplifyButton
3237: .setSelected(ModelGenerator.decProdForTestGen == ModelGenerator.SIMPLIFY);
3238: cogentButton
3239: .setSelected(ModelGenerator.decProdForTestGen == ModelGenerator.COGENT);
3240: }
3241: });
3242: }
3243:
3244: private final class AutoModeAction extends AbstractAction {
3245:
3246: private boolean buttonPressed = false;
3247: private boolean creatingTests = false;
3248:
3249: final Icon startLogo = IconFactory
3250: .autoModeStartLogo(toolbarIconSize);
3251: final Icon stopLogo = IconFactory
3252: .autoModeStopLogo(toolbarIconSize);
3253:
3254: private Proof associatedProof;
3255:
3256: private final ProofTreeListener ptl = new ProofTreeAdapter() {
3257:
3258: public void proofStructureChanged(ProofTreeEvent e) {
3259: if (e.getSource() == associatedProof) {
3260: enable();
3261: }
3262:
3263: }
3264:
3265: public void proofClosed(ProofTreeEvent e) {
3266: if (e.getSource() == associatedProof) {
3267: enable();
3268: }
3269: }
3270:
3271: public void proofGoalsAdded(ProofTreeEvent e) {
3272: }
3273: };
3274:
3275: public void enable() {
3276: setEnabled(associatedProof != null
3277: && !associatedProof.closed() && !creatingTests);
3278: }
3279:
3280: public AutoModeAction() {
3281: putValue("hideActionText", Boolean.TRUE);
3282: putValue(Action.SHORT_DESCRIPTION, AUTO_MODE_TEXT);
3283: putValue(Action.SMALL_ICON, startLogo);
3284:
3285: associatedProof = mediator.getProof();
3286:
3287: enable();
3288:
3289: if (associatedProof != null
3290: && !associatedProof
3291: .containsProofTreeListener(ptl)) {
3292: associatedProof.addProofTreeListener(ptl);
3293: }
3294:
3295: mediator
3296: .addKeYSelectionListener(new KeYSelectionListener() {
3297: /** focused node has changed */
3298: public void selectedNodeChanged(
3299: KeYSelectionEvent e) {
3300: }
3301:
3302: /**
3303: * the selected proof has changed. Enable or disable action depending whether a proof is
3304: * available or not
3305: */
3306: public void selectedProofChanged(
3307: KeYSelectionEvent e) {
3308: if (associatedProof != null) {
3309: associatedProof
3310: .removeProofTreeListener(ptl);
3311: }
3312:
3313: associatedProof = e.getSource()
3314: .getSelectedProof();
3315: enable();
3316:
3317: if (associatedProof != null) {
3318: associatedProof
3319: .addProofTreeListener(ptl);
3320: }
3321: }
3322: });
3323:
3324: mediator.addAutoModeListener(new AutoModeListener() {
3325:
3326: /**
3327: * invoked if automatic execution has started
3328: */
3329: public void autoModeStarted(ProofEvent e) {
3330: autoMode = true;
3331: if (associatedProof != null) {
3332: associatedProof
3333: .removeProofTreeListener(ptl);
3334: }
3335: putValue(Action.SMALL_ICON, stopLogo);
3336: }
3337:
3338: /**
3339: * invoked if automatic execution has stopped
3340: */
3341: public void autoModeStopped(ProofEvent e) {
3342: autoMode = false;
3343: if (associatedProof != null) {
3344: run
3345: .setToolTipText("<html><pre>Create Test for:\n"
3346: + associatedProof.name()
3347: + "</pre>");
3348: }
3349: if (associatedProof != null
3350: && associatedProof == e.getSource()
3351: && !associatedProof
3352: .containsProofTreeListener(ptl)) {
3353: associatedProof.addProofTreeListener(ptl);
3354: }
3355: if (associatedProof != null && buttonPressed
3356: && associatedProof == e.getSource()
3357: && associatedProof.countNodes() > 1) {
3358: creatingTests = true;
3359: new Thread(new Runnable() {
3360: public void run() {
3361: try {
3362: setEnabled(false);
3363: main
3364: .setStatusLine("Generating Tests");
3365: StringBuffer testPath = new StringBuffer();
3366: String modelDir = associatedProof
3367: .getJavaModel()
3368: .getModelDir();
3369: test2model.put(testPath,
3370: modelDir);
3371: buttonPressed = false;
3372: if (openDialog) {
3373: MethodSelectionDialog msd = MethodSelectionDialog
3374: .getInstance(mediator);
3375: msd
3376: .setLatestTests(testPath);
3377: } else {
3378: UnitTestBuilder testBuilder = new UnitTestBuilder(
3379: mediator
3380: .getServices(),
3381: mediator.getProof());
3382: testPath
3383: .append(testBuilder
3384: .createTestForProof(associatedProof)
3385: + " ");
3386:
3387: main
3388: .setStatusLine("Test Generation Completed");
3389: mediator
3390: .testCaseConfirmation(testPath
3391: .toString());
3392: }
3393: main
3394: .setStatusLine("Test Generation Completed");
3395: } catch (Exception exc) {
3396: ExtList l = new ExtList();
3397: l.add(exc);
3398: new ExceptionDialog(testGui, l);
3399: }
3400: creatingTests = false;
3401: enable();
3402: }
3403: }).start();
3404: }
3405: putValue(Action.SMALL_ICON, startLogo);
3406: }
3407:
3408: });
3409:
3410: }
3411:
3412: public void actionPerformed(ActionEvent e) {
3413: // Unfortunately, when clicking the button twice
3414: // (very fast), the glasspane won't be quick
3415: // enough to catch the second event. Therefore
3416: // we make a second check (which is a %%%HACK)
3417: if (!autoMode) {
3418: // setEnabled(false);
3419: buttonPressed = true;
3420: mediator.startAutoMode();
3421: } else {
3422: mediator.stopAutoMode();
3423: }
3424: }
3425:
3426: }
3427: }
3428:
3429: }
|