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.rule.soundness;
012:
013: import java.awt.*;
014: import java.awt.event.ActionEvent;
015: import java.awt.event.ActionListener;
016: import java.util.Vector;
017:
018: import javax.swing.*;
019: import javax.swing.border.TitledBorder;
020:
021: import de.uka.ilkd.key.gui.KeYMediator;
022: import de.uka.ilkd.key.rule.IteratorOfNoPosTacletApp;
023: import de.uka.ilkd.key.rule.NoPosTacletApp;
024: import de.uka.ilkd.key.rule.SetOfNoPosTacletApp;
025:
026: public class POSelectionDialog extends JDialog {
027:
028: private JList tacletList;
029:
030: private final SetOfNoPosTacletApp tacs;
031: private boolean okPressed = false;
032:
033: public POSelectionDialog(KeYMediator mediator,
034: SetOfNoPosTacletApp tacs) {
035: super (mediator.mainFrame() == null ? new JFrame() : mediator
036: .mainFrame(), "Load Taclets", true);
037:
038: this .tacs = tacs;
039:
040: layoutPODialog();
041:
042: pack();
043: setLocation(70, 70);
044: setVisible(true);
045: }
046:
047: private Object[] createTacletListContents() {
048: Vector res = new Vector();
049: IteratorOfNoPosTacletApp it = tacs.iterator();
050:
051: while (it.hasNext())
052: res.add(it.next());
053:
054: Object[] taclets = res.toArray();
055: // Arrays.sort(taclets);
056:
057: return taclets;
058: }
059:
060: public NoPosTacletApp[] getSelectedTaclets() {
061: if (!okPressed)
062: return new NoPosTacletApp[0];
063: Object[] sels = tacletList.getSelectedValues();
064: NoPosTacletApp[] res = new NoPosTacletApp[sels.length];
065: System.arraycopy(sels, 0, res, 0, sels.length);
066: return res;
067: }
068:
069: /** lays out the configuration dialog */
070: private void layoutPODialog() {
071: JPanel listPanel = new JPanel();
072: listPanel.setBorder(new TitledBorder(
073: "Select the Taclets to Load"));
074:
075: tacletList = new JList(createTacletListContents());
076: tacletList
077: .setSelectionMode(ListSelectionModel.MULTIPLE_INTERVAL_SELECTION);
078: tacletList.setSelectionInterval(0, tacletList.getModel()
079: .getSize() - 1);
080: tacletList
081: .setPrototypeCellValue("just_quite_a_long_taclet_name");
082: tacletList.setCellRenderer(new DefaultListCellRenderer() {
083:
084: public Component getListCellRendererComponent(JList list,
085: Object value, // value to display
086: int index, // cell index
087: boolean isSelected, // is the cell selected
088: boolean cellHasFocus) // the list and the
089: //cell have the focus
090: {
091: if (value instanceof NoPosTacletApp) {
092: value = ((NoPosTacletApp) value).taclet().name();
093: }
094: return super .getListCellRendererComponent(list, value,
095: index, isSelected, cellHasFocus);
096: }
097: });
098: listPanel.add(new JScrollPane(tacletList));
099:
100: JButton ok = new JButton("OK");
101: ok.addActionListener(new ActionListener() {
102: public void actionPerformed(ActionEvent ae) {
103: okPressed = true;
104: dispose();
105: }
106: });
107: JButton cancel = new JButton("Cancel");
108: cancel.addActionListener(new ActionListener() {
109: public void actionPerformed(ActionEvent ae) {
110: dispose();
111: }
112: });
113:
114: JPanel p = new JPanel(new GridBagLayout());
115: GridBagConstraints c = new GridBagConstraints();
116:
117: c.insets = new Insets(5, 20, 5, 20);
118: c.gridx = 0;
119: p.add(ok, c);
120:
121: c.gridx = 1;
122: p.add(cancel, c);
123: p.setAlignmentY(JPanel.BOTTOM_ALIGNMENT);
124:
125: p.add(ok);
126: p.add(cancel);
127:
128: getContentPane().setLayout(new BorderLayout());
129: getContentPane().add(listPanel, BorderLayout.CENTER);
130: getContentPane().add(p, BorderLayout.SOUTH);
131:
132: }
133:
134: }
|