001: // This file is part of KeY - Integrated Deductive Software Design
002: // Copyright (C) 2001-2007 Universitaet Karlsruhe, Germany
003: // Universitaet Koblenz-Landau, Germany
004: // Chalmers University of Technology, Sweden
005: //
006: // The KeY system is protected by the GNU General Public License.
007: // See LICENSE.TXT for details.
008:
009: package de.uka.ilkd.key.gui;
010:
011: import java.awt.Dimension;
012: import java.awt.FlowLayout;
013: import java.awt.event.ActionEvent;
014: import java.awt.event.ActionListener;
015: import java.io.IOException;
016: import java.io.StringReader;
017:
018: import javax.swing.*;
019:
020: import de.uka.ilkd.key.logic.EverythingLocationDescriptor;
021: import de.uka.ilkd.key.logic.IteratorOfLocationDescriptor;
022: import de.uka.ilkd.key.logic.SetOfLocationDescriptor;
023: import de.uka.ilkd.key.logic.TermFactory;
024: import de.uka.ilkd.key.parser.KeYLexer;
025: import de.uka.ilkd.key.parser.KeYParser;
026: import de.uka.ilkd.key.parser.ParserMode;
027: import de.uka.ilkd.key.pp.LogicPrinter;
028: import de.uka.ilkd.key.pp.NotationInfo;
029: import de.uka.ilkd.key.proof.init.InitConfig;
030: import de.uka.ilkd.key.speclang.ClassInvariant;
031: import de.uka.ilkd.key.util.Debug;
032: import de.uka.ilkd.key.util.ExtList;
033:
034: /**
035: * A dialog for selecting / entering a depends clause.
036: */
037: public class DependsClauseDialog extends JDialog {
038: private static final int LINE_WIDTH = 70;
039:
040: private final InitConfig initConfig;
041: private final SetOfLocationDescriptor defaultClause;
042: private final JTextArea textArea;
043: private SetOfLocationDescriptor currentClause;
044: private boolean successful = false;
045:
046: public DependsClauseDialog(ClassInvariant inv, InitConfig ic,
047: SetOfLocationDescriptor defaultClause) {
048: super (new JFrame(), "Depends clause for \"" + inv + "\"", true);
049: this .initConfig = ic;
050: this .defaultClause = defaultClause;
051:
052: //create text area
053: textArea = new JTextArea(10, LINE_WIDTH);
054: setToDefault();
055: JScrollPane scrollPane = new JScrollPane(textArea);
056: getContentPane().add(scrollPane);
057:
058: //create button panel
059: JPanel buttonPanel = new JPanel();
060: buttonPanel.setLayout(new FlowLayout(FlowLayout.RIGHT, 5, 5));
061: getContentPane().add(buttonPanel);
062: Dimension buttonDim = new Dimension(80, 25);
063:
064: //create "ok" button
065: JButton okButton = new JButton("OK");
066: okButton.setPreferredSize(buttonDim);
067: okButton.setMinimumSize(buttonDim);
068: okButton.addActionListener(new ActionListener() {
069: public void actionPerformed(ActionEvent e) {
070: if (parseText()) {
071: successful = true;
072: setVisible(false);
073: }
074: }
075: });
076: buttonPanel.add(okButton);
077: getRootPane().setDefaultButton(okButton);
078:
079: //create "restore default" button
080: JButton restoreButton = new JButton("Restore default");
081: Dimension restoreButtonDim = new Dimension(120, 25);
082: restoreButton.setPreferredSize(restoreButtonDim);
083: restoreButton.setMinimumSize(restoreButtonDim);
084: restoreButton.addActionListener(new ActionListener() {
085: public void actionPerformed(ActionEvent e) {
086: setToDefault();
087: }
088: });
089: buttonPanel.add(restoreButton);
090:
091: getContentPane().setLayout(
092: new BoxLayout(getContentPane(), BoxLayout.Y_AXIS));
093: pack();
094: setLocation(70, 70);
095: setVisible(true);
096: }
097:
098: private void setToDefault() {
099: currentClause = defaultClause;
100:
101: //print default clause to text area
102: LogicPrinter printer = new LogicPrinter(null, NotationInfo
103: .createInstance(), initConfig.getServices());
104: printer.setLineWidth(LINE_WIDTH);
105: try {
106: printer.printLocationDescriptors(defaultClause);
107: textArea.setText(printer.toString());
108: } catch (IOException e) {
109: Debug.fail();
110: }
111: }
112:
113: private boolean parseText() {
114: KeYLexer lexer = new KeYLexer(new StringReader(textArea
115: .getText()), initConfig.getServices()
116: .getExceptionHandler());
117: KeYParser parser = new KeYParser(ParserMode.TERM, lexer, null,
118: TermFactory.DEFAULT, initConfig.getServices(),
119: initConfig.namespaces());
120: try {
121: SetOfLocationDescriptor locations = parser.location_list();
122:
123: //check for "*"-locations, which are not allowed here
124: IteratorOfLocationDescriptor it = locations.iterator();
125: while (it.hasNext()) {
126: if (it.next() instanceof EverythingLocationDescriptor) {
127: throw new Exception(
128: "Please use a non-trivial depends clause.");
129: }
130: }
131:
132: currentClause = locations;
133: } catch (Exception e) {
134: ExtList list = new ExtList();
135: list.add(e);
136: new ExceptionDialog(this , list);
137: return false;
138: }
139:
140: return true;
141: }
142:
143: /**
144: * Tells whether the user clicked "ok".
145: */
146: public boolean wasSuccessful() {
147: return successful;
148: }
149:
150: public SetOfLocationDescriptor getDependsClause() {
151: return currentClause;
152: }
153: }
|