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: //
010:
011: package de.uka.ilkd.key.gui;
012:
013: import java.awt.*;
014: import java.awt.event.ActionEvent;
015: import java.awt.event.ActionListener;
016: import java.io.IOException;
017: import java.io.StringReader;
018:
019: import javax.swing.*;
020: import javax.swing.border.BevelBorder;
021: import javax.swing.border.CompoundBorder;
022: import javax.swing.border.EmptyBorder;
023: import javax.swing.border.TitledBorder;
024: import javax.swing.event.ListSelectionEvent;
025: import javax.swing.event.ListSelectionListener;
026: import javax.swing.event.TableModelEvent;
027: import javax.swing.event.TableModelListener;
028: import javax.swing.table.DefaultTableCellRenderer;
029:
030: import org.apache.log4j.Logger;
031:
032: import de.uka.ilkd.key.logic.Constraint;
033: import de.uka.ilkd.key.logic.Term;
034: import de.uka.ilkd.key.parser.ParserException;
035: import de.uka.ilkd.key.parser.SimpleTermParser;
036: import de.uka.ilkd.key.parser.TermParserFactory;
037: import de.uka.ilkd.key.pp.LogicPrinter;
038: import de.uka.ilkd.key.pp.ProgramPrinter;
039: import de.uka.ilkd.key.proof.ConstraintTableModel;
040: import de.uka.ilkd.key.proof.Proof;
041: import de.uka.ilkd.key.util.Debug;
042:
043: public class UserConstraintView extends JPanel {
044:
045: /** Text fields for new equalities */
046: private JTextField newEqLeftText, newEqRightText;
047: private JButton newEqAddButton, newEqReplaceButton, delEqButton;
048:
049: /**
050: * true iff the controls of the pane are activated (a proof is loaded, no
051: * modal dialog in visible)
052: */
053: private boolean controlsActive;
054:
055: /** Status messages */
056: private JLabel statusLabel;
057: private JLabel constraintSatLabel;
058:
059: /** Constraint to be edited */
060: private ConstraintTableModel constraintTableModel = null;
061: private ConstraintTableListener constraintTableListener = new ConstraintTableListener();
062: private JTable constraintTable;
063:
064: private KeYMediator mediator = null;
065:
066: /** Listener for proof changes */
067: private SelectionListener selectionListener = new SelectionListener();
068:
069: /** Listener for GUI changes */
070: private ConstraintViewGUIListener guiListener = new ConstraintViewGUIListener();
071:
072: public UserConstraintView() {
073:
074: layoutPane();
075: setVisible(true);
076:
077: setControlsActive(true);
078: printSatisfiability();
079: }
080:
081: public void setMediator(KeYMediator p_mediator) {
082: if (mediator != null)
083: unregisterAtMediator();
084:
085: mediator = p_mediator;
086: registerAtMediator();
087:
088: setConstraintTableModel(mediator.getUserConstraint());
089: }
090:
091: private void setConstraintTableModel(ConstraintTableModel p_model) {
092: if (constraintTableModel != null)
093: unregisterAtModel();
094:
095: constraintTableModel = p_model;
096:
097: if (constraintTableModel != null) {
098: constraintTable.setModel(constraintTableModel);
099: registerAtModel();
100: }
101:
102: setControlsActive(constraintTableModel != null);
103: updateTextFields();
104: printSatisfiability();
105: }
106:
107: private void registerAtMediator() {
108: mediator.addKeYSelectionListener(selectionListener);
109: mediator.addGUIListener(guiListener);
110: }
111:
112: private void unregisterAtMediator() {
113: mediator.removeGUIListener(guiListener);
114: mediator.removeKeYSelectionListener(selectionListener);
115: }
116:
117: private void registerAtModel() {
118: constraintTableModel
119: .addTableModelListener(constraintTableListener);
120: }
121:
122: private void unregisterAtModel() {
123: constraintTableModel
124: .removeTableModelListener(constraintTableListener);
125: }
126:
127: private void setControlsActive(boolean p) {
128: controlsActive = p;
129:
130: constraintTable.setEnabled(controlsAreActive());
131: newEqLeftText.setEnabled(controlsAreActive());
132: newEqRightText.setEnabled(controlsAreActive());
133:
134: updateButtons();
135: }
136:
137: /**
138: * @return true iff controls of the pane should be painted enabled in
139: * principal
140: */
141: private boolean controlsAreActive() {
142: return controlsActive && constraintTableModel != null;
143: }
144:
145: /** Build everything */
146: private void layoutPane() {
147: setLayout(new GridBagLayout());
148: GridBagConstraints c = new GridBagConstraints();
149:
150: c.fill = GridBagConstraints.BOTH;
151: c.gridx = 0;
152: c.gridy = 0;
153: c.gridwidth = 1;
154: c.gridheight = 1;
155: c.weightx = 1;
156: c.weighty = 1;
157: add(createConstraintPanel(), c);
158:
159: c.fill = GridBagConstraints.BOTH;
160: c.gridx = 0;
161: c.gridy = 1;
162: c.gridwidth = 1;
163: c.gridheight = 1;
164: c.weightx = 1;
165: c.weighty = 0;
166: c.insets = new Insets(2, 0, 0, 0);
167: add(createStatusPanel(), c);
168: }
169:
170: private JPanel createStatusPanel() {
171: statusLabel = new JLabel(" ");
172: JPanel statusLine = new JPanel(new BorderLayout());
173:
174: statusLine.add(statusLabel, BorderLayout.CENTER);
175: statusLabel.setBorder(new BevelBorder(BevelBorder.LOWERED));
176:
177: return statusLine;
178: }
179:
180: private void updateButtons() {
181: final ListSelectionModel lsm = constraintTable
182: .getSelectionModel();
183: delEqButton.setEnabled(controlsAreActive()
184: && !lsm.isSelectionEmpty());
185: newEqAddButton.setEnabled(controlsAreActive());
186: newEqReplaceButton.setEnabled(controlsAreActive()
187: && !lsm.isSelectionEmpty());
188: }
189:
190: /**
191: * Determine the first selected row of the table, and copy the values
192: * of this row to the text fields for entering new constraints
193: */
194: private void updateTextFields() {
195: final ListSelectionModel lsm = constraintTable
196: .getSelectionModel();
197: if (constraintTableModel == null || lsm.isSelectionEmpty()) {
198: newEqLeftText.setText("");
199: newEqRightText.setText("");
200: } else {
201: final int row = lsm.getMinSelectionIndex();
202: newEqLeftText
203: .setText(prettyPrint((Term) constraintTableModel
204: .getValueAt(row, 0)));
205: newEqRightText
206: .setText(prettyPrint((Term) constraintTableModel
207: .getValueAt(row, 1)));
208: }
209: }
210:
211: /**
212: * @return the position at which a row should be inserted in the table upon
213: * executing the replace action. This is the first not selected row
214: * after a selected one.
215: */
216: private int replaceRowInsertionPosition() {
217: final ListSelectionModel lsm = constraintTable
218: .getSelectionModel();
219: Debug.assertFalse(lsm.isSelectionEmpty());
220:
221: int row = lsm.getMinSelectionIndex();
222: do
223: ++row;
224: while (row <= lsm.getMaxSelectionIndex()
225: && lsm.isSelectedIndex(row));
226:
227: return row;
228: }
229:
230: /** Main area with table, text fields and buttons for adding/removing constraints */
231: private JPanel createConstraintPanel() {
232: JPanel constraintPanel = new JPanel(new GridBagLayout());
233: GridBagConstraints c = new GridBagConstraints();
234:
235: constraintTable = new JTable(constraintTableModel);
236: constraintTable.setDefaultRenderer(Term.class,
237: new CellRenderer());
238: constraintTable
239: .setPreferredScrollableViewportSize(new Dimension(300,
240: 300));
241: JScrollPane pane = new JScrollPane(constraintTable);
242:
243: constraintTable.getSelectionModel().addListSelectionListener(
244: new ListSelectionListener() {
245: public void valueChanged(ListSelectionEvent p_e) {
246: updateTextFields();
247: updateButtons();
248: }
249: });
250: constraintTable
251: .setSelectionMode(ListSelectionModel.SINGLE_INTERVAL_SELECTION);
252:
253: newEqLeftText = new JTextField();
254: newEqRightText = new JTextField();
255:
256: newEqAddButton = new JButton("Add");
257: newEqReplaceButton = new JButton("Replace");
258: delEqButton = new JButton("Del");
259:
260: newEqAddButton.addActionListener(new ActionListener() {
261: public void actionPerformed(ActionEvent p_e) {
262: addRow(newEqLeftText.getText(), newEqRightText
263: .getText(), "Added", constraintTableModel
264: .getRowCount());
265: }
266: });
267:
268: newEqReplaceButton.addActionListener(new ActionListener() {
269: public void actionPerformed(ActionEvent p_e) {
270: final int index = constraintTable.getSelectionModel()
271: .getMinSelectionIndex();
272: if (addRow(newEqLeftText.getText(), newEqRightText
273: .getText(), "Replaced",
274: replaceRowInsertionPosition())) {
275: removeSelectedRows();
276: constraintTable.changeSelection(index, index,
277: false, false);
278: }
279: }
280: });
281:
282: delEqButton.setEnabled(false);
283: delEqButton.addActionListener(new ActionListener() {
284: public void actionPerformed(ActionEvent p_e) {
285: removeSelectedRows();
286: }
287: });
288:
289: JLabel addLabel = new JLabel("Add new Equality:");
290:
291: constraintSatLabel = new JLabel("", SwingConstants.RIGHT);
292:
293: c.fill = GridBagConstraints.BOTH;
294: c.gridx = 0;
295: c.gridy = 0;
296: c.gridwidth = 2;
297: c.gridheight = 1;
298: c.weightx = 1;
299: c.weighty = 1;
300: c.insets = new Insets(0, 0, 3, 0);
301: constraintPanel.add(pane, c);
302:
303: c.fill = GridBagConstraints.HORIZONTAL;
304: c.gridx = 0;
305: c.gridy = 1;
306: c.gridwidth = 2;
307: c.gridheight = 1;
308: c.weightx = 1;
309: c.weighty = 0;
310: c.insets = new Insets(0, 0, 0, 0);
311: constraintPanel.add(constraintSatLabel, c);
312:
313: c.fill = GridBagConstraints.NONE;
314: c.anchor = GridBagConstraints.WEST;
315: c.gridx = 0;
316: c.gridy = 2;
317: c.gridwidth = 2;
318: c.gridheight = 1;
319: c.weightx = 1;
320: c.weighty = 0;
321: c.insets = new Insets(2, 0, 0, 0);
322: constraintPanel.add(addLabel, c);
323:
324: c.anchor = GridBagConstraints.CENTER;
325:
326: final JPanel textPanel = new JPanel(new GridLayout(1, 2, 8, 8));
327:
328: textPanel.add(newEqLeftText);
329: textPanel.add(newEqRightText);
330:
331: c.fill = GridBagConstraints.HORIZONTAL;
332: c.gridx = 0;
333: c.gridy = 3;
334: c.gridwidth = 2;
335: c.gridheight = 1;
336: c.weightx = 1;
337: c.weighty = 0;
338: c.insets = new Insets(4, 0, 0, 0);
339: constraintPanel.add(textPanel, c);
340:
341: final JPanel buttonPanel = new JPanel(
342: new GridLayout(1, 3, 8, 8));
343:
344: buttonPanel.add(newEqAddButton);
345: buttonPanel.add(newEqReplaceButton);
346: buttonPanel.add(delEqButton);
347:
348: c.fill = GridBagConstraints.HORIZONTAL;
349: c.gridx = 0;
350: c.gridy = 4;
351: c.gridwidth = 2;
352: c.gridheight = 1;
353: c.weightx = 1;
354: c.weighty = 0;
355: c.insets = new Insets(8, 0, 0, 0);
356: constraintPanel.add(buttonPanel, c);
357:
358: constraintPanel.setBorder(new CompoundBorder(new TitledBorder(
359: "Constraint Equalities"), new EmptyBorder(2, 2, 2, 2)));
360:
361: return constraintPanel;
362: }
363:
364: /**
365: * Will be called when this dialog will be closed
366: */
367: protected void closeDlg() {
368: // mediator.freeModalAccess(this);
369: }
370:
371: /**
372: * Redraw the table, which is necessary after notational modifications.
373: * %%% TODO: Somehow call this method when abbreviation settings change.
374: */
375: void updateTableDisplay() {
376: if (constraintTableModel != null)
377: constraintTableModel.fireTableDataChanged();
378: }
379:
380: private void printStatus(String p_status) {
381: statusLabel.setText(p_status);
382: }
383:
384: private synchronized void printSatisfiability() {
385: if (constraintTableModel != null) {
386: if (constraintTableModel.getConstraint().isSatisfiable()) {
387: constraintSatLabel.setText("Constraint is satisfiable");
388: constraintSatLabel.setForeground(UIManager
389: .getColor("Label.foreground"));
390: } else {
391: constraintSatLabel
392: .setText("Constraint is not satisfiable");
393: constraintSatLabel.setForeground(Color.red);
394: }
395: } else
396: constraintSatLabel.setText("");
397: }
398:
399: /**
400: * creates a new Termparser that parses the given string using
401: * namespaces and services from the mediator
402: * @param s the String to parse
403: */
404: public Term parseTerm(String s) throws ParserException {
405: final SimpleTermParser parser = TermParserFactory
406: .createInstance();
407: return parser.parse(new StringReader(s), null, mediator
408: .getServices(), mediator.namespaces(), mediator
409: .getNotationInfo().getAbbrevMap());
410: }
411:
412: /**
413: * Add a new equality as a pair of strings to the model
414: *
415: * @param p_performedAction
416: * a string that is used to render the status message
417: * @param p_index
418: * row number at which the new equation is supposed to turn up
419: * @return true iff the strings have been parsed successfully
420: */
421: public boolean addRow(String p_left, String p_right,
422: String p_performedAction, int p_index) {
423: Term left, right;
424: try {
425: left = parseTerm(p_left);
426: } catch (ParserException e) {
427: setErrorStatus(e, "left");
428: Logger.getLogger(UserConstraintView.class.getName())
429: .info(e);
430: displayError(e, newEqLeftText);
431: return false;
432: }
433:
434: try {
435: right = parseTerm(p_right);
436: } catch (ParserException e) {
437: setErrorStatus(e, "right");
438: Logger.getLogger(UserConstraintView.class.getName())
439: .info(e);
440: displayError(e, newEqRightText);
441: return false;
442: }
443:
444: // This is only valid for sort hierarchies that are trees
445: if (!(left.sort().extendsTrans(right.sort()) || right.sort()
446: .extendsTrans(left.sort()))) {
447: printStatus("Sorts are incompatible");
448: return false;
449: }
450:
451: if (!Constraint.BOTTOM.unify(left, right, null).isSatisfiable()) {
452: printStatus("Terms are not unifiable");
453: return false;
454: }
455:
456: constraintTableModel.addEquality(left, right, p_index);
457:
458: printStatus(p_performedAction + " Constraint");
459:
460: return true;
461: }
462:
463: private void setErrorStatus(ParserException p_e, String p_leftRight) {
464: printStatus("<html>Syntax error in " + p_leftRight
465: + " term:<pre>" + p_e.getMessage() + "</pre></html>");
466: }
467:
468: /**
469: * Make one of the text fields react to a syntax error that occurred when
470: * parsing the displayed string
471: */
472: private static void displayError(ParserException p_ex,
473: JTextField p_textarea) {
474: p_textarea.requestFocus();
475: if (p_ex.getLocation() != null)
476: p_textarea.setCaretPosition(Math.min(p_ex.getLocation()
477: .getColumn(), p_textarea.getColumns()));
478: }
479:
480: private String prettyPrint(Term value) {
481: Debug.assertFalse(mediator == null);
482:
483: LogicPrinter sp = new LogicPrinter(new ProgramPrinter(null),
484: mediator.getNotationInfo(), mediator.getServices(),
485: true);
486: try {
487: sp.printTerm(value);
488: return sp.toString();
489: } catch (IOException e) {
490: throw new RuntimeException(
491: "IO Exception in pretty printer:\n" + e);
492: }
493: }
494:
495: private void removeSelectedRows() {
496: int i;
497: while ((i = constraintTable.getSelectedRow()) != -1)
498: constraintTableModel.deleteRow(i);
499: }
500:
501: private class SelectionListener implements KeYSelectionListener {
502:
503: /** focused node has changed */
504: public void selectedNodeChanged(KeYSelectionEvent e) {
505: }
506:
507: /** the selected proof has changed (e.g. a new proof has been
508: * loaded) */
509: public void selectedProofChanged(KeYSelectionEvent e) {
510: final Proof selectedProof = e.getSource()
511: .getSelectedProof();
512: Runnable action = new Runnable() {
513: public void run() {
514: if (selectedProof != null) {
515: setConstraintTableModel(selectedProof
516: .getUserConstraint());
517: } else {
518: setConstraintTableModel(null);
519: }
520: }
521: };
522:
523: if (SwingUtilities.isEventDispatchThread())
524: action.run();
525: else
526: SwingUtilities.invokeLater(action);
527: }
528:
529: }
530:
531: private class ConstraintTableListener implements TableModelListener {
532:
533: public void tableChanged(TableModelEvent p_e) {
534: Runnable action = new Runnable() {
535: public void run() {
536: printSatisfiability();
537: }
538: };
539: if (SwingUtilities.isEventDispatchThread())
540: action.run();
541: else
542: SwingUtilities.invokeLater(action);
543: }
544:
545: }
546:
547: private class ConstraintViewGUIListener implements GUIListener {
548: /** invoked if a frame that wants modal access is opened */
549: public void modalDialogOpened(GUIEvent e) {
550: setControlsActive(false);
551: }
552:
553: /** invoked if a frame that wants modal access is closed */
554: public void modalDialogClosed(GUIEvent e) {
555: setControlsActive(true);
556: }
557:
558: public void shutDown(GUIEvent e) {
559:
560: }
561: }
562:
563: private class CellRenderer extends DefaultTableCellRenderer {
564:
565: public Component getTableCellRendererComponent(JTable table,
566: Object value, boolean isSelected, boolean hasFocus,
567: int row, int col) {
568: Debug.assertTrue(value instanceof Term);
569: return super .getTableCellRendererComponent(table,
570: prettyPrint((Term) value), isSelected, hasFocus,
571: row, col);
572: }
573: }
574: }
|