001: package visualdebugger.draw2d;
002:
003: import java.util.HashMap;
004: import java.util.Iterator;
005: import java.util.LinkedList;
006:
007: import org.eclipse.draw2d.*;
008: import org.eclipse.draw2d.geometry.Rectangle;
009: import org.eclipse.swt.widgets.Display;
010:
011: import de.uka.ilkd.key.logic.*;
012: import de.uka.ilkd.key.visualdebugger.VisualDebugger;
013: import de.uka.ilkd.key.visualdebugger.statevisualisation.SymbolicArrayObject;
014: import de.uka.ilkd.key.visualdebugger.statevisualisation.SymbolicObject;
015: import de.uka.ilkd.key.visualdebugger.statevisualisation.SymbolicObjectDiagram;
016:
017: public class ArrayObjectFigure extends ObjectFigure {
018:
019: private final IndexLabel[] indexColumns;
020:
021: private Label[] indexConstrColumns;
022:
023: private LinkedList sos;
024:
025: public ArrayObjectFigure(SymbolicArrayObject sao,
026: MouseListener listener, SymbolicObjectDiagram symbState,
027: boolean pre) {
028: super (sao, listener, symbState, pre);
029: this .sos = symbState.getSymbolicObjects();
030: createConstr(listener);
031: SetOfTerm indexes = sao.getAllIndexTerms();
032: indexes = indexes.union(sao.getAllPostIndex());
033:
034: indexColumns = new IndexLabel[indexes.size()];
035: final IFigure compColumns = new Figure();
036: int i = 0;
037: for (IteratorOfTerm it = indexes.iterator(); it.hasNext();) {
038: final Term pv = it.next();
039: indexColumns[i] = new IndexLabel(sao, pv, sos);
040: indexColumns[i].addMouseListener(listener);
041: i++;
042: }
043: sort(indexColumns);
044: for (i = 0; i < indexColumns.length; i++) {
045: compColumns.add(indexColumns[i]);
046: }
047:
048: ToolbarLayout tbl = new ToolbarLayout(false);
049: tbl.setMinorAlignment(ToolbarLayout.ALIGN_CENTER);
050: tbl.setSpacing(5);
051: compColumns.setLayoutManager(tbl);
052: compColumns.setBorder(new SeparatorBorder());
053: add(compColumns);
054:
055: }
056:
057: private SetOfTerm disj(SetOfTerm s1, SetOfTerm s2) {
058: SetOfTerm result = SetAsListOfTerm.EMPTY_SET;
059: for (IteratorOfTerm it = s1.iterator(); it.hasNext();) {
060: Term t = it.next();
061: if (s2.contains(t))
062: result = result.add(t);
063: }
064: return result;
065:
066: }
067:
068: private SetOfTerm exclude(SetOfTerm s1, SetOfTerm s2) {
069: SetOfTerm result = s1;
070: for (IteratorOfTerm it = s2.iterator(); it.hasNext();) {
071: Term t = it.next();
072: if (s1.contains(t))
073: result = result.remove(t);
074: }
075: return result;
076:
077: }
078:
079: private void createConstr(MouseListener listener) {
080: LinkedList indexTermPos = ((SymbolicArrayObject) this
081: .getSymbolicObject())
082: .getPossibleIndexTermConfigurations();
083: if (indexTermPos.size() <= 1)
084: return;
085: SetOfTerm cut = SetAsListOfTerm.EMPTY_SET;
086: if (indexTermPos.size() > 0) {
087: Iterator it = indexTermPos.iterator();
088: cut = (SetOfTerm) it.next();
089: while (it.hasNext()) {
090: cut = disj(cut, (SetOfTerm) it.next());
091: }
092: }
093:
094: // System.out.println("Indizes "+attributes);
095: indexConstrColumns = new Label[indexTermPos.size()];
096: final IFigure compColumns = new Figure();
097: int i = 0;
098: for (Iterator it = indexTermPos.iterator(); it.hasNext();) {
099:
100: final SetOfTerm indexConstr = (SetOfTerm) it.next();
101: // System.out.println("Term asfasfdagsfdasgfdsdf "+pv);
102: indexConstrColumns[i] = new IndexConstraintLabel(
103: (SymbolicArrayObject) so, indexConstr, exclude(
104: indexConstr, cut), sos);
105: indexConstrColumns[i]
106: .setTextAlignment(PositionConstants.CENTER);
107: indexConstrColumns[i].setFont(Display.getCurrent()
108: .getSystemFont());
109: indexConstrColumns[i].addMouseListener(listener);
110:
111: if (indexConstr.subset(((SymbolicArrayObject) this
112: .getSymbolicObject()).getIndexConfiguration())) {
113: indexConstrColumns[i]
114: .setForegroundColor(ColorConstants.blue);
115: }
116:
117: // indexConstrColumns[ i ].addMouseListener(listener);
118:
119: compColumns.add(indexConstrColumns[i]);
120:
121: i++;
122: }
123:
124: // column labels are placed in separate compartment
125:
126: compColumns.setLayoutManager(new ToolbarLayout(false));
127: compColumns.setBorder(new SeparatorBorder());
128:
129: add(compColumns);
130:
131: }
132:
133: public SymbolicObject getSymbolicObject() {
134: return (SymbolicArrayObject) so;
135: }
136:
137: public HashMap getIndexY() {
138: HashMap result = new HashMap();
139: for (int i = 0; i < indexColumns.length; i++) {
140: Term index = indexColumns[i].getIndex();
141: Rectangle bounds = indexColumns[i].getBounds().getCopy();
142: int p = bounds.y + bounds.height / 2 - this .getBounds().y;
143: result.put(index, new Integer(p));
144:
145: }
146:
147: return result;
148: }
149:
150: public static void sort(IndexLabel[] a) {
151: if (a == null)
152: return;
153: boolean sorted = false;
154: IndexLabel help;
155: while (!sorted) {
156: sorted = true;
157: for (int i = 0; i < a.length - 1; i++) {
158: if (a[i].getKeY() > a[i + 1].getKeY()) {
159: help = a[i];
160: a[i] = a[i + 1];
161: a[i + 1] = help;
162: sorted = false;
163: }
164: }
165:
166: }
167: }
168:
169: public class IndexLabel extends Figure {
170: private final SymbolicArrayObject so;
171: private final Term pv;
172: private boolean selected = false;
173: private String text;
174:
175: public IndexLabel(SymbolicArrayObject so, Term index,
176: LinkedList sos) {
177: super ();
178: this .so = so;
179: this .pv = index;
180: ToolbarLayout layout = new ToolbarLayout();
181: layout.setMinorAlignment(ToolbarLayout.ALIGN_CENTER);
182: layout.setVertical(false);
183: layout.setStretchMinorAxis(false);
184: layout.setSpacing(2);
185:
186: this .setLayoutManager(layout);
187:
188: text = VisualDebugger.getVisualDebugger().prettyPrint(
189: SLListOfTerm.EMPTY_LIST.append(index), sos, so);
190: final Label l = new Label(text);
191: l.setLabelAlignment(PositionConstants.CENTER);
192: this .add(l);
193: l.setBorder(new LineBorder(ColorConstants.black));
194: if (so.getAllPostIndex().contains(index)) {
195: this
196: .add(new Label(
197: " := "
198: + VisualDebugger
199: .getVisualDebugger()
200: .prettyPrint(
201: SLListOfTerm.EMPTY_LIST
202: .append(so
203: .getValueTermForIndex(index)),
204: sos, so)));
205: }
206:
207: setFont(Display.getCurrent().getSystemFont());
208: l.setFont(Display.getCurrent().getSystemFont());
209:
210: }
211:
212: public Term getIndex() {
213: return pv;
214: }
215:
216: private int getKeY() {
217: int key = -1;
218: try {
219: key = Integer.valueOf(
220: text.substring(0, text.length() - 1))
221: .intValue();
222: } catch (NumberFormatException e) {
223: key = -1;
224: }
225: return key;
226: }
227:
228: public SymbolicArrayObject getSo() {
229: return so;
230: }
231:
232: public void setSelected(boolean value) {
233: this .selected = value;
234: if (selected)
235: setForegroundColor(ColorConstants.blue);
236: else
237: setForegroundColor(null);
238: repaint();
239: }
240:
241: }
242:
243: public class IndexConstraintLabel extends Label {
244: private final SymbolicArrayObject so;
245: private final SetOfTerm con;
246: private boolean selected = false;
247:
248: public IndexConstraintLabel(SymbolicArrayObject so,
249: SetOfTerm index, SetOfTerm index2, LinkedList sos) {
250: super ();
251: this .so = so;
252: this .con = index;
253: String text = VisualDebugger.getVisualDebugger()
254: .prettyPrint(index2, sos, so);
255:
256: this .setText(text);
257: setFont(Display.getCurrent().getSystemFont());
258: }
259:
260: public SetOfTerm getIndexConstraints() {
261: return con;
262: }
263:
264: public SymbolicArrayObject getSo() {
265: return so;
266: }
267:
268: public void setSelected(boolean value) {
269: this.selected = value;
270: if (selected)
271: this.setForegroundColor(ColorConstants.blue);
272: else
273: this.setForegroundColor(null);
274: repaint();
275: }
276:
277: }
278:
279: }
|