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.Color;
014: import java.awt.Component;
015: import java.awt.FlowLayout;
016: import java.awt.Font;
017: import java.awt.event.MouseAdapter;
018: import java.awt.event.MouseEvent;
019: import java.awt.event.MouseListener;
020: import java.util.Iterator;
021: import java.util.List;
022:
023: import javax.swing.*;
024:
025: import de.uka.ilkd.key.gui.configuration.Config;
026: import de.uka.ilkd.key.proof.ProofAggregate;
027: import de.uka.ilkd.key.proof.ProofTreeAdapter;
028: import de.uka.ilkd.key.proof.mgt.Contract;
029: import de.uka.ilkd.key.proof.mgt.OldOperationContract;
030: import de.uka.ilkd.key.proof.mgt.ProofStatus;
031: import de.uka.ilkd.key.util.Debug;
032:
033: public class MethodContractList extends JList implements
034: java.io.Serializable {
035:
036: /** the model used by this view */
037: private MethodContractListModel methodContractListModel;
038:
039: MouseListener mouseListener = new MethodContractListMouseListener();
040:
041: static final JLabel keyIcon = new JLabel(IconFactory
042: .keyHole(20, 20));
043: static final JLabel keyClosedIcon = new JLabel(IconFactory
044: .keyHoleClosed(20, 20));
045: static final JLabel keyAlmostClosedIcon = new JLabel(IconFactory
046: .keyHoleAlmostClosed(20, 20));
047:
048: class MethodContractListMouseListener extends MouseAdapter
049: implements java.io.Serializable {
050: public void mouseClicked(MouseEvent e) {
051: }
052: }
053:
054: public MethodContractList(List ctList) {
055: setSelectionMode(ListSelectionModel.SINGLE_SELECTION);
056: methodContractListModel = new MethodContractListModel(ctList);
057: if (methodContractListModel.getSize() > 0) {
058: setSelectedIndex(0);
059: }
060: setModel(methodContractListModel);
061: setCellRenderer(new IconCellRenderer());
062: addMouseListener(mouseListener);
063: updateUI();
064: }
065:
066: public void updateUI() {
067: super .updateUI();
068: Font myFont = UIManager.getFont(Config.KEY_FONT_GOAL_LIST_VIEW);
069: if (myFont != null) {
070: setFont(myFont);
071: } else {
072: Debug
073: .out(
074: "goallist: Warning: Use standard font. Could not find font:",
075: Config.KEY_FONT_GOAL_LIST_VIEW);
076: }
077: }
078:
079: public de.uka.ilkd.key.proof.ProofAggregate getProofForCurrentContract() {
080: if (getSelectedIndex() < 0) {
081: return null;
082: }
083: Contract mC = (Contract) methodContractListModel
084: .getElementAt(getSelectedIndex());
085: List mCL = mC.getProofs();
086: if (mCL.size() != 0) {
087: return (de.uka.ilkd.key.proof.ProofAggregate) mCL.get(0);
088: }
089: return null;
090: }
091:
092: public Contract getCurrentContract() {
093: if (getSelectedIndex() < 0) {
094: return null;
095: }
096: return (Contract) methodContractListModel
097: .getElementAt(getSelectedIndex());
098:
099: }
100:
101: public static Component makeMethodContractDisplay(
102: OldOperationContract mc, JPanel panel, JTextArea text,
103: JPanel statusPanel, Color c) {
104: String mcString = mc.toString();
105: text.setText(mcString);
106: List proofs = mc.getProofs();
107: Iterator it = proofs.iterator();
108: statusPanel.removeAll();
109: while (it.hasNext()) {
110: ProofAggregate pl = (ProofAggregate) it.next();
111: ProofStatus ps = pl.getStatus();
112: JLabel lab = null;
113: if (ps != null) {
114: if (ps.getProofClosed()) {
115: lab = keyClosedIcon;
116: }
117: if (ps.getProofClosedButLemmasLeft()) {
118: lab = keyAlmostClosedIcon;
119: }
120: if (ps.getProofOpen()) {
121: lab = keyIcon;
122: }
123: }
124: statusPanel.add(lab);
125: }
126: text.setBackground(c);
127: panel.setBackground(c);
128: statusPanel.setBackground(c);
129: return panel;
130: }
131:
132: //INNER CLASSES
133:
134: static class MethodContractListModel extends AbstractListModel {
135:
136: private List ctList;
137:
138: MethodContractListModel(List ctList) {
139: this .ctList = ctList;
140: }
141:
142: public int getSize() {
143: return ctList.size();
144: }
145:
146: public Object getElementAt(int i) {
147: return ctList.get(i);
148: }
149:
150: class MethodContractListProofTreeListener extends
151: ProofTreeAdapter implements java.io.Serializable {
152:
153: /** invoked if all goals of the proof are closed
154: */
155: // public void proofClosed(ProofTreeEvent e) {
156: // setAttentive(true);
157: // clear();
158: // }
159: }
160: }
161:
162: class IconCellRenderer extends DefaultListCellRenderer implements
163: ListCellRenderer, java.io.Serializable {
164:
165: JPanel panel;
166: JPanel statusPanel;
167: JTextArea text;
168: private Color selBgColor;
169:
170: public IconCellRenderer() {
171: FlowLayout lay = new FlowLayout();
172: lay.setAlignment(FlowLayout.LEFT);
173: panel = new JPanel(lay);
174: statusPanel = new JPanel(lay);
175: text = new JTextArea();
176: MethodContractList.this .setToolTipText("Method Contract");
177: panel.add(text);
178: panel.add(statusPanel);
179: text.setEditable(false);
180: text.setCaretPosition(0);
181: }
182:
183: public Component getListCellRendererComponent(JList list,
184: Object value, // value to display
185: int index, // cell index
186: boolean isSelected, // is the cell selected
187: boolean cellHasFocus) // the list and the cell have the focus
188: {
189: if (value instanceof OldOperationContract) {
190: if (isSelected && selBgColor == null) {
191: Component sup = super .getListCellRendererComponent(
192: list, value, index, isSelected,
193: cellHasFocus);
194: selBgColor = sup.getBackground();
195: }
196: OldOperationContract mc = (OldOperationContract) value;
197: return makeMethodContractDisplay(mc, panel, text,
198: statusPanel, isSelected ? selBgColor
199: : Color.white);
200: } else {
201: return super.getListCellRendererComponent(list, value,
202: index, isSelected, cellHasFocus);
203: }
204: }
205:
206: }
207:
208: }
|