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: package de.uka.ilkd.key.gui;
009:
010: import java.awt.*;
011: import java.util.Arrays;
012: import java.util.Comparator;
013: import java.util.Iterator;
014: import java.util.List;
015:
016: import javax.swing.*;
017: import javax.swing.border.Border;
018: import javax.swing.border.TitledBorder;
019: import javax.swing.event.ListSelectionListener;
020:
021: import de.uka.ilkd.key.proof.ProofAggregate;
022: import de.uka.ilkd.key.proof.mgt.Contract;
023: import de.uka.ilkd.key.proof.mgt.ContractSet;
024: import de.uka.ilkd.key.proof.mgt.OldOperationContract;
025: import de.uka.ilkd.key.proof.mgt.ProofStatus;
026:
027: public class ContractSelectionPanel extends JPanel {
028:
029: static final Icon keyIcon = IconFactory.keyHole(20, 20);
030: static final Icon keyClosedIcon = IconFactory.keyHoleClosed(20, 20);
031: static final Icon keyAlmostClosedIcon = IconFactory
032: .keyHoleAlmostClosed(20, 20);
033:
034: private JList list;
035: private JComponent comp;
036:
037: public ContractSelectionPanel(ContractSet ctSet, boolean dlchooser) {
038: if (ctSet != null)
039: list = new JList(sortContracts(ctSet));
040: else
041: list = new JList();
042: list.setSelectedIndex(0);
043: if (!dlchooser) {
044: list.setPreferredSize(new Dimension(800, list.getHeight()));
045: comp = new JScrollPane(list);
046: } else {
047: comp = list;
048: }
049: add(comp);
050: list.setCellRenderer(new ContractListCellRenderer());
051: }
052:
053: public void setContracts(ContractSet ctSet) {
054: remove(comp);
055: list = new JList(sortContracts(ctSet));
056: list.setSelectedIndex(0);
057: comp = list;
058: add(comp);
059: list.setCellRenderer(new ContractListCellRenderer());
060: }
061:
062: private Object[] sortContracts(ContractSet ctSet) {
063: Object[] cl = ctSet.toArray();
064: Arrays.sort(cl, new ContractComparator());
065: return cl;
066: }
067:
068: public Contract getCurrentSelection() {
069: if (list.getSelectedIndex() < 0) {
070: return null;
071: }
072: return (Contract) list.getSelectedValue();
073: }
074:
075: public void addListSelectionListener(ListSelectionListener listener) {
076: list.addListSelectionListener(listener);
077: }
078:
079: class ContractListCellRenderer extends DefaultListCellRenderer {
080:
081: JPanel panel;
082: JLabel text;
083: private Color selBgColor;
084:
085: public ContractListCellRenderer() {
086: setOpaque(true);
087: FlowLayout lay = new FlowLayout();
088: lay.setAlignment(FlowLayout.LEFT);
089: panel = new JPanel(lay);
090: text = new JLabel();
091: panel.add(text);
092: }
093:
094: public Component getListCellRendererComponent(JList list,
095: Object value, int index, boolean isSelected,
096: boolean cellHasFocus) {
097: if (value instanceof OldOperationContract) {
098: if (isSelected && selBgColor == null) {
099: Component sup = super .getListCellRendererComponent(
100: list, value, index, isSelected,
101: cellHasFocus);
102: selBgColor = sup.getBackground();
103: }
104: OldOperationContract mc = (OldOperationContract) value;
105: text.setText(mc.getHTMLText());
106: panel.setBorder(new StatusTitledBorder(BorderFactory
107: .createEtchedBorder(), mc.getName(), value));
108: text.setVerticalAlignment(SwingConstants.TOP);
109: if (isSelected) {
110: text.setBackground(selBgColor);
111: panel.setBackground(selBgColor);
112: } else {
113: text.setBackground(Color.white);
114: panel.setBackground(Color.white);
115: }
116: } else {
117: return super .getListCellRendererComponent(list, value,
118: index, isSelected, cellHasFocus);
119: }
120: return panel;
121: }
122: }
123:
124: class StatusTitledBorder extends TitledBorder {
125:
126: private Object value;
127:
128: StatusTitledBorder(Border b, String s, Object value) {
129: super (b, s);
130: this .value = value;
131: }
132:
133: public void paintBorder(Component c, Graphics g, int x, int y,
134: int width, int height) {
135: title = " " + title;
136: super .paintBorder(c, g, x, y, width, height);
137: List proofs = ((OldOperationContract) value).getProofs();
138: Iterator it = proofs.iterator();
139: while (it.hasNext()) {
140: ProofAggregate pl = (ProofAggregate) it.next();
141: ProofStatus ps = pl.getStatus();
142: x = x + 6;
143: g.setColor(c.getBackground());
144: g.fillRect(x, y, keyClosedIcon.getIconWidth(),
145: keyClosedIcon.getIconHeight());
146: if (ps.getProofClosedButLemmasLeft()) {
147: keyAlmostClosedIcon.paintIcon(c, g, x, y);
148: } else if (ps.getProofClosed()) {
149: keyClosedIcon.paintIcon(c, g, x, y);
150: } else if (ps.getProofOpen()) {
151: keyIcon.paintIcon(c, g, x, y);
152: }
153: }
154: }
155:
156: }
157:
158: private class ContractComparator implements Comparator {
159: public int compare(Object o1, Object o2) {
160: if (!(o1 instanceof Contract & o2 instanceof Contract))
161: return 0;
162: return ((Contract) o1).getName().compareTo(
163: ((Contract) o2).getName());
164: }
165: }
166:
167: }
|