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.Component;
014: import java.awt.event.ActionEvent;
015: import java.awt.event.ActionListener;
016: import java.awt.event.FocusAdapter;
017: import java.awt.event.FocusEvent;
018:
019: import javax.swing.*;
020: import javax.swing.border.TitledBorder;
021:
022: import de.uka.ilkd.key.java.Services;
023: import de.uka.ilkd.key.proof.ApplyTacletDialogModel;
024: import de.uka.ilkd.key.proof.IfChoiceModel;
025: import de.uka.ilkd.key.proof.ProofSaver;
026: import de.uka.ilkd.key.rule.IfFormulaInstantiation;
027: import de.uka.ilkd.key.util.Debug;
028:
029: /**
030: * this dialog appears if a rule is selected to be applied and the rule has an
031: * if sequent. The dialog offers the possibility to select the wanted match of
032: * the if sequent or to enter the if-sequent instantiation manually
033: */
034: public class TacletIfSelectionDialog extends JPanel {
035:
036: private JPanel ifPanel = new JPanel();
037: private ApplyTacletDialogModel model;
038: private TacletMatchCompletionDialog owner;
039:
040: /** creates a new dialog
041: * @param model the model to be displayed
042: */
043: public TacletIfSelectionDialog(ApplyTacletDialogModel model,
044: TacletMatchCompletionDialog owner) {
045:
046: this .model = model;
047: this .owner = owner;
048: layoutDialog();
049: setVisible(true);
050: }
051:
052: private void layoutDialog() {
053: setLayout(new BoxLayout(this , BoxLayout.Y_AXIS));
054:
055: ifPanel = createIfPanel();
056: add(ifPanel);
057: }
058:
059: /** creates the panel used to select the wanted if instantiation */
060: private JPanel createIfPanel() {
061: JPanel panel = new JPanel();
062: panel.setLayout(new BoxLayout(panel, BoxLayout.Y_AXIS));
063: panel.setBorder(new TitledBorder(
064: "Please instantiate the taclet's assumptions:"));
065:
066: // If the if-sequent matches to diffferent parts of the sequent
067: // the user is given the possibility to choose the right one
068: // or to enter an instantiation manually in which case a cut
069: // is performed if the manual entry does not match any other
070: // part in the sequent. The list of possible the
071: // if-instantiations is shown in a combo box model that is
072: // created here.
073: for (int i = 0; i < model.ifChoiceModelCount(); i++) {
074: final JPanel p = new JPanel();
075: p.setLayout(new BoxLayout(p, BoxLayout.X_AXIS));
076: JLabel label = new JLabel(ProofSaver.printAnything(model
077: .ifFma(i), model.proof().getServices())) {
078: public java.awt.Dimension getPreferredSize() {
079: return new java.awt.Dimension(100, 10);
080: }
081: };
082: p.add(label);
083: JComboBox ifChoice = new JComboBox(model.ifChoiceModel(i)) {
084: public java.awt.Dimension getPreferredSize() {
085: return new java.awt.Dimension(800, (int) super
086: .getPreferredSize().getHeight());
087: }
088: };
089: IfComboRenderer rend = new IfComboRenderer(ifChoice
090: .getRenderer(), model.proof().getServices());
091: ifChoice.setRenderer(rend);
092: ifChoice.addActionListener(new ActionListener() {
093: public void actionPerformed(ActionEvent e) {
094: JComboBox cb = (JComboBox) e.getSource();
095: updateInputField(p, cb);
096: }
097: });
098: p.add(ifChoice);
099:
100: updateInputField(p, ifChoice);
101: panel.add(p);
102: }
103: return panel;
104: }
105:
106: /** the if selecton dialog is attached to exact one model */
107: protected int current() {
108: return 0;
109: }
110:
111: /**
112: * requests focus for the the field-th input field and sets the cursor at the
113: * given position
114: */
115: public void requestFocusAt(int field, int col) {
116: ifPanel.setVisible(true);
117: ifPanel.requestFocus();
118:
119: JTextField tf = (JTextField) ((JPanel) ifPanel
120: .getComponent(field * 2)).getComponent(2);
121: Debug.outIfEqual(
122: "tacletifselectiondialog:: none existing field"
123: + " requested", null, tf);
124: if (tf != null && col >= 0 && col < tf.getColumns()) {
125: try {
126: tf.setCaretPosition(col - 1);
127: } catch (IllegalArgumentException iae) {
128: Debug
129: .out("tacletifselectiondialog:: something is wrong with "
130: + "the caret position calculation.");
131: } finally {
132: tf.requestFocus();
133: tf.validate();
134: }
135: }
136: ifPanel.validate();
137: }
138:
139: private void updateInputField(JPanel parent, JComboBox cb) {
140: IfChoiceModel icm = (IfChoiceModel) cb.getModel();
141: JTextField inp = new JTextField(40);
142: inp.addFocusListener(new FocusAdapter() {
143: public void focusLost(FocusEvent e) {
144: pushAllInputToModel();
145: owner.setStatus();
146: }
147: });
148: inp.addActionListener(new ActionListener() {
149: public void actionPerformed(ActionEvent e) {
150: pushAllInputToModel();
151: owner.setStatus();
152: }
153: });
154:
155: int nr = parent.getComponentCount();
156: if (cb.getSelectedItem() == icm.manualText() && (nr == 2)) {
157: parent.add(inp);
158: inp.setEnabled(true);
159: }
160: if (cb.getSelectedItem() != icm.manualText() && (nr == 3)) {
161: parent.remove(parent.getComponent(2));
162: }
163: parent.revalidate();
164: pushAllInputToModel();
165: owner.setStatus();
166: }
167:
168: /** transfers input to the model */
169: protected void pushAllInputToModel() {
170: for (int i = 0; i < ifPanel.getComponentCount(); i++) {
171: JPanel pan = (JPanel) ifPanel.getComponent(i);
172: if ((pan.getComponentCount() == 3)
173: && (((JTextField) pan.getComponent(2)).getText() != null)) {
174: model.setManualInput(i, ((JTextField) pan
175: .getComponent(2)).getText());
176: } else {
177: model.setManualInput(i, "");
178: }
179: }
180: }
181:
182: static class IfComboRenderer extends JLabel implements
183: ListCellRenderer {
184:
185: private final Services services;
186: private final ListCellRenderer defaultRenderer;
187:
188: public IfComboRenderer(ListCellRenderer renderer,
189: Services services) {
190: setOpaque(true);
191: this .services = services;
192: this .defaultRenderer = renderer;
193: }
194:
195: public Component getListCellRendererComponent(JList list,
196: Object value, int index, boolean isSelected,
197: boolean cellHasFocus) {
198: final String valStr = value instanceof IfFormulaInstantiation ? ((IfFormulaInstantiation) value)
199: .toString(services)
200: : value.toString();
201:
202: if (isSelected) {
203: list.setToolTipText(valStr);
204: }
205:
206: Component c = defaultRenderer.getListCellRendererComponent(
207: list, valStr, index, isSelected, cellHasFocus);
208: return c;
209: }
210: }
211:
212: }
|