001: package de.uka.ilkd.key.casetool.eclipse;
002:
003: /*
004: * This file is part of KeY - Integrated Deductive Software Design
005: * Copyright (C) 2001-2005 Universitaet Karlsruhe, Germany
006: * Universitaet Koblenz-Landau, Germany
007: * Chalmers University of Technology, Sweden
008: *
009: * The KeY system is protected by the GNU General Public License.
010: */
011:
012: import java.util.Vector;
013:
014: import org.eclipse.jface.dialogs.Dialog;
015: import org.eclipse.jface.dialogs.MessageDialog;
016: import org.eclipse.jface.viewers.IStructuredContentProvider;
017: import org.eclipse.jface.viewers.IStructuredSelection;
018: import org.eclipse.jface.viewers.LabelProvider;
019: import org.eclipse.jface.viewers.ListViewer;
020: import org.eclipse.jface.viewers.Viewer;
021: import org.eclipse.swt.SWT;
022: import org.eclipse.swt.widgets.Button;
023: import org.eclipse.swt.widgets.Composite;
024: import org.eclipse.swt.widgets.Control;
025: import org.eclipse.swt.widgets.Label;
026: import org.eclipse.swt.widgets.List;
027: import org.eclipse.swt.widgets.Shell;
028:
029: /**
030: * @author Marius Hillenbrand
031: *
032: */
033: public class MethodPOSelectionDialog extends Dialog {
034:
035: ListViewer viewer;
036: IStructuredSelection selectionOnOK;
037: Button allInvariantsButton;
038: Button addInvariantsToPostConditionButton;
039: boolean allInvariants;
040: boolean addInvariantsToPostCondition;
041: Vector methodPOInput;
042:
043: private final class MethodPOSelectionLabelProvider extends
044: LabelProvider {
045:
046: /* (non-Javadoc)
047: * @see org.eclipse.jface.viewers.ILabelProvider#getText(java.lang.Object)
048: */
049: public String getText(Object element) {
050:
051: // quick-and-dirty beautification of the selection dialog
052:
053: String fullProofDescription = element.toString();
054:
055: StringBuffer out = new StringBuffer(fullProofDescription);
056:
057: int recentLineLength = 0;
058:
059: boolean eraseRemainingLine = false;
060:
061: for (int pos = 0; pos < out.length();) {
062: char c = out.charAt(pos);
063:
064: if (eraseRemainingLine) {
065:
066: if (c != '\n') {
067: out.deleteCharAt(pos);
068:
069: } else {
070: out.insert(pos, "...");
071: eraseRemainingLine = false;
072: recentLineLength = 0;
073: pos += 4;
074: }
075:
076: } else {
077:
078: if (c == '\n') {
079: recentLineLength = 0;
080: pos++;
081:
082: } else {
083: recentLineLength++;
084: pos++;
085:
086: if (recentLineLength >= 70)
087: eraseRemainingLine = true;
088: }
089: }
090: }
091: return out.toString();
092: }
093: }
094:
095: /**
096: * A StructuredContentProvider is used in the eclipse jface viewer framework to feed
097: * model data into a viewer.
098: * In this case we provide the list of selectable proof obligations for a list viewer
099: */
100: private class MethodPOContentProvider implements
101: IStructuredContentProvider {
102:
103: ListViewer viewer;
104:
105: public MethodPOContentProvider() {
106: super ();
107: }
108:
109: /* (non-Javadoc)
110: * @see org.eclipse.jface.viewers.IContentProvider#dispose()
111: */
112: public void dispose() {
113: // nothing to do here
114: }
115:
116: /* (non-Javadoc)
117: * @see org.eclipse.jface.viewers.IContentProvider#inputChanged(org.eclipse.jface.viewers.Viewer, java.lang.Object, java.lang.Object)
118: * Does nothing, since we do not need to store/process the input element ourself.
119: */
120: public void inputChanged(Viewer viewer, Object oldInput,
121: Object newInput) {
122:
123: }
124:
125: /* (non-Javadoc)
126: * @see org.eclipse.jface.viewers.IStructuredContentProvider#getElements(java.lang.Object)
127: * Here we extract the possible proof obligations from the input vector.
128: * This method will be called by the ListViewer after the input vector has been fed
129: * via setInput()
130: */
131: public Object[] getElements(Object inputElement) {
132:
133: if (inputElement instanceof Vector) {
134: Vector v = (Vector) inputElement;
135: Object entries[] = new Object[v.size()];
136:
137: for (int i = 0; i < v.size(); i++) {
138: entries[i] = v.get(i);
139: }
140:
141: return entries;
142:
143: } else {
144: return null;
145: }
146: }
147: }
148:
149: /**
150: * @param parentShell
151: * @param methodPOInput the vector of possible proof obligations the user shall choose from
152: */
153: public MethodPOSelectionDialog(Shell parentShell,
154: Vector methodPOInput) {
155: super (parentShell);
156: this .methodPOInput = methodPOInput;
157: }
158:
159: /* (non-Javadoc)
160: * @see org.eclipse.jface.dialogs.Dialog#okPressed()
161: */
162: protected void okPressed() {
163: // preserve for evaluation after the dialog has been closed and the viewer
164: // widget is possibly disposed
165: selectionOnOK = (IStructuredSelection) viewer.getSelection();
166:
167: allInvariants = allInvariantsButton.getSelection();
168: addInvariantsToPostCondition = addInvariantsToPostConditionButton
169: .getSelection();
170:
171: // if no PO has been selected, display an error
172: // otherwise close dialog (normal way of operation)
173: if (selectionOnOK.size() == 0) {
174: MessageDialog
175: .openError(getShell(),
176: "No proof obligation selected",
177: "Select one of the provided proof obligations first.");
178: } else {
179: super .okPressed();
180: }
181: }
182:
183: /* (non-Javadoc)
184: * @see org.eclipse.jface.window.Window#configureShell(org.eclipse.swt.widgets.Shell)
185: */
186: protected void configureShell(Shell newShell) {
187: // that much effort for a simple window title
188: super .configureShell(newShell);
189: newShell
190: .setText("Select desired proof obligation for this method");
191: }
192:
193: /* (non-Javadoc)
194: * @see org.eclipse.jface.dialogs.Dialog#createDialogArea(org.eclipse.swt.widgets.Composite)
195: */
196: protected Control createDialogArea(Composite parent) {
197:
198: Composite composite = (Composite) super
199: .createDialogArea(parent);
200:
201: Label label = new Label(composite, SWT.NONE);
202: label.setText("JML specifications for selected method:");
203:
204: List list = new List(composite, SWT.BORDER | SWT.SINGLE
205: | SWT.H_SCROLL);
206: viewer = new ListViewer(list);
207:
208: //new ListViewer()
209:
210: // use our own content provider
211: viewer.setContentProvider(new MethodPOContentProvider());
212: // use predefined label provider which uses toString() as text and null as image
213: viewer.setLabelProvider(new MethodPOSelectionLabelProvider());
214:
215: viewer.setInput(methodPOInput);
216:
217: allInvariantsButton = new Button(composite, SWT.CHECK);
218: allInvariantsButton.setText("Use all applicable invariants");
219: allInvariantsButton.setSelection(true);
220: addInvariantsToPostConditionButton = new Button(composite,
221: SWT.CHECK);
222: addInvariantsToPostConditionButton
223: .setText("Add invariants to postcondition");
224:
225: composite.layout();
226:
227: return composite;
228: }
229:
230: /**
231: * @return Returns the selectionOnOK.
232: */
233: public IStructuredSelection getSelectionOnOK() {
234: return selectionOnOK;
235: }
236:
237: /**
238: * @return Returns the addInvariantsToPostCondition.
239: */
240: public boolean isAddInvariantsToPostConditionSelected() {
241: return addInvariantsToPostCondition;
242: }
243:
244: /**
245: * @return Returns the allInvariants.
246: */
247: public boolean isAllInvariantsSelected() {
248: return allInvariants;
249: }
250:
251: }
|