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: // This file is part of KeY - Integrated Deductive Software Design
009: // Copyright (C) 2001-2005 Universitaet Karlsruhe, Germany
010: // Universitaet Koblenz-Landau, Germany
011: // Chalmers University of Technology, Sweden
012: //
013: // The KeY system is protected by the GNU General Public License.
014: // See LICENSE.TXT for details.
015: //
016: //
017:
018: package de.uka.ilkd.key.rule.encapsulation;
019:
020: import java.awt.Color;
021: import java.awt.Dimension;
022: import java.awt.event.ActionEvent;
023: import java.awt.event.ActionListener;
024: import java.util.Iterator;
025: import java.util.LinkedList;
026: import java.util.List;
027:
028: import javax.swing.*;
029:
030: import de.uka.ilkd.key.util.Debug;
031:
032: class UniverseDialog extends JDialog {
033:
034: private static final Color COLOR_TRUE = Color.GREEN;
035: private static final Color COLOR_FALSE = Color.RED;
036: private static final Color COLOR_UNDECIDED = Color.LIGHT_GRAY;
037:
038: private final ListOfTypeSchemeConstraint constraints;
039: private final List /*JLabel*/constraintLabels;
040:
041: public UniverseDialog(ListOfTypeSchemeConstraint constraints) {
042: super (new JFrame(), "Universes", true);
043:
044: //initialise members
045: this .constraints = constraints;
046: constraintLabels = new LinkedList();
047:
048: //initialise content pane
049: getContentPane().setLayout(
050: new BoxLayout(getContentPane(), BoxLayout.X_AXIS));
051:
052: //create variables panel
053: JPanel varsPanel = new JPanel();
054: varsPanel.setLayout(new BoxLayout(varsPanel, BoxLayout.Y_AXIS));
055: JScrollPane varsPane = new JScrollPane(varsPanel);
056: getContentPane().add(varsPane);
057:
058: //create variable labels and combo boxes
059: SetOfTypeSchemeVariable vars = (new TypeSchemeAndConstraint(
060: constraints)).getFreeVars();
061: IteratorOfTypeSchemeVariable it = vars.iterator();
062: while (it.hasNext()) {
063: TypeSchemeVariable var = it.next();
064:
065: //prepare values
066: SetOfTypeScheme valueRange = var.getValueRange();
067: Object[] values = new Object[valueRange.size() + 1];
068: values[0] = var.getDefaultValue();
069: IteratorOfTypeScheme it2 = valueRange.iterator();
070: int i = 1;
071: while (it2.hasNext()) {
072: values[i++] = it2.next();
073: }
074:
075: //create variable panel
076: JPanel varPanel = new JPanel();
077: varPanel
078: .setLayout(new BoxLayout(varPanel, BoxLayout.X_AXIS));
079: varsPanel.add(varPanel);
080:
081: //create variable label and combo box
082: JLabel varLabel = new JLabel(var.toString());
083: varLabel.setMinimumSize(new Dimension(200, 20));
084: varLabel.setPreferredSize(new Dimension(200, 20));
085: varPanel.add(varLabel);
086: JComboBox varCombo = new JComboBox(values);
087: varCombo.addActionListener(new VarComboListener(var));
088: varCombo.setMinimumSize(new Dimension(280, 20));
089: varCombo.setPreferredSize(new Dimension(280, 20));
090: varPanel.add(varCombo);
091: }
092:
093: //create constraints panel
094: JPanel constraintsPanel = new JPanel();
095: constraintsPanel.setLayout(new BoxLayout(constraintsPanel,
096: BoxLayout.Y_AXIS));
097: JScrollPane constraintsPane = new JScrollPane(constraintsPanel);
098: getContentPane().add(constraintsPane);
099:
100: //create constraints labels
101: IteratorOfTypeSchemeConstraint it2 = constraints.iterator();
102: while (it2.hasNext()) {
103: TypeSchemeConstraint constraint = it2.next();
104:
105: JLabel constraintLabel = new JLabel(constraint.toString());
106: constraintLabels.add(constraintLabel);
107: constraintLabel.setOpaque(true);
108: constraintsPanel.add(constraintLabel);
109: }
110:
111: refreshConstraintColors();
112:
113: pack();
114: setLocation(70, 70);
115: setVisible(true);
116: }
117:
118: private boolean valueIsExact(TypeSchemeConstraint constraint) {
119: SetOfTypeSchemeVariable vars = constraint.getFreeVars();
120: IteratorOfTypeSchemeVariable it = vars.iterator();
121: while (it.hasNext()) {
122: if (!it.next().valueIsExact()) {
123: return false;
124: }
125: }
126:
127: return true;
128: }
129:
130: private void refreshConstraintColors() {
131: IteratorOfTypeSchemeConstraint constraintsIt = constraints
132: .iterator();
133: Iterator labelsIt = constraintLabels.iterator();
134: while (constraintsIt.hasNext()) {
135: Debug.assertTrue(labelsIt.hasNext());
136: TypeSchemeConstraint constraint = constraintsIt.next();
137: JLabel label = (JLabel) labelsIt.next();
138:
139: if (!constraint.evaluate()) {
140: label.setBackground(COLOR_FALSE);
141: } else {
142: if (valueIsExact(constraint)) {
143: label.setBackground(COLOR_TRUE);
144: } else {
145: label.setBackground(COLOR_UNDECIDED);
146: }
147: }
148: }
149: }
150:
151: private class VarComboListener implements ActionListener {
152: private final TypeSchemeVariable var;
153:
154: public VarComboListener(TypeSchemeVariable var) {
155: this .var = var;
156: }
157:
158: public void actionPerformed(ActionEvent e) {
159: JComboBox varCombo = (JComboBox) e.getSource();
160: Object newValue = varCombo.getSelectedItem();
161: if (newValue instanceof TypeSchemeUnion) {
162: var.assignValue((TypeSchemeUnion) newValue);
163: } else {
164: var.assignValue((TypeScheme) newValue);
165: }
166:
167: refreshConstraintColors();
168: }
169: }
170: }
|