001: package visualdebugger.draw2d;
002:
003: import java.util.LinkedList;
004:
005: import org.eclipse.draw2d.*;
006: import org.eclipse.draw2d.geometry.Insets;
007: import org.eclipse.draw2d.geometry.Point;
008: import org.eclipse.draw2d.geometry.Rectangle;
009: import org.eclipse.swt.SWT;
010: import org.eclipse.swt.graphics.Color;
011: import org.eclipse.swt.graphics.Font;
012: import org.eclipse.swt.widgets.Display;
013:
014: import de.uka.ilkd.key.java.JavaInfo;
015: import de.uka.ilkd.key.java.abstraction.ArrayType;
016: import de.uka.ilkd.key.java.abstraction.ClassType;
017: import de.uka.ilkd.key.java.abstraction.KeYJavaType;
018: import de.uka.ilkd.key.logic.IteratorOfTerm;
019: import de.uka.ilkd.key.logic.ListOfTerm;
020: import de.uka.ilkd.key.logic.SLListOfTerm;
021: import de.uka.ilkd.key.logic.Term;
022: import de.uka.ilkd.key.logic.op.*;
023: import de.uka.ilkd.key.logic.sort.Sort;
024: import de.uka.ilkd.key.visualdebugger.VisualDebugger;
025: import de.uka.ilkd.key.visualdebugger.statevisualisation.SymbolicObject;
026: import de.uka.ilkd.key.visualdebugger.statevisualisation.SymbolicObjectDiagram;
027:
028: public class ObjectFigure extends Figure {
029: private Figure instanceName;
030:
031: private Label[] attrColumns;
032:
033: protected final SymbolicObject so;
034:
035: private MouseListener listener;
036:
037: private Figure compAttributes;
038:
039: private LinkedList sos;
040:
041: private Figure methodComp;
042:
043: private boolean pre;
044: private final VisualDebugger vd = VisualDebugger
045: .getVisualDebugger();
046:
047: private Label[] paramColumns; //TODO make prameter selectable
048:
049: private SymbolicObjectDiagram symbState;
050:
051: static Font BOLD = new Font(null, "", 12, SWT.BOLD);
052:
053: static Font BOLD_SMALL = new Font(null, "", 10, SWT.BOLD);
054:
055: //static Font BOLD_UNERLINE = new Font(null, "", 10, SWT.BOLD || SWT.);
056:
057: static Font qmFont = new Font(null, "", 30, SWT.BOLD);
058:
059: static final Color instanceNameBackGround = new Color(null, 222,
060: 222, 255);
061:
062: public ObjectFigure(SymbolicObject so, MouseListener listener,
063: SymbolicObjectDiagram symbState, boolean pre) {
064: this .so = so;
065: this .sos = symbState.getSymbolicObjects();
066: this .symbState = symbState;
067: this .pre = pre;
068: this .listener = listener;
069: this .prepare();
070: this .createInstanceName();
071: add(instanceName);
072: createCompAttributes();
073: add(compAttributes);
074: createMethodComp();
075: if (methodComp != null) {
076: add(methodComp);
077: }
078:
079: }
080:
081: private void createMethodComp() {
082: if (so.getMethod() == null && !pre)
083: return;
084:
085: if (pre
086: && !
087:
088: ((vd.isStaticMethod() && so.isStatic() && so.getType()
089: .equals(vd.getType())) ||
090:
091: (!vd.isStaticMethod() && so.getTerms().contains(
092: vd.getSelfTerm()))))
093: return;
094:
095: this .methodComp = new Figure();
096: ToolbarLayout l = new ToolbarLayout(false);
097: methodComp.setLayoutManager(l);
098:
099: final ProgramMethod method = pre ? VisualDebugger
100: .getVisualDebugger().getDebuggingMethod() : this .so
101: .getMethod();
102:
103: Label methodSectionLabel = new Label("Current Method: ");
104: if (pre)
105: methodSectionLabel = new Label(
106: "Upcoming Method Invocation:");
107:
108: methodSectionLabel.setFont(BOLD_SMALL);
109: methodComp.add(methodSectionLabel);
110:
111: Label mLabel = new Label(VisualDebugger.getMethodString(method
112: .getMethodDeclaration()));
113: mLabel.setFont(Display.getCurrent().getSystemFont());
114: methodComp.add(mLabel);
115:
116: Label parameterSectionLabel = new Label("Input Values: ");
117: parameterSectionLabel.setFont(BOLD_SMALL);
118: methodComp.add(parameterSectionLabel);
119:
120: if (!pre) {
121: final ListOfProgramVariable parameters = so.getParameter();
122: if (parameters != null) {
123: this .paramColumns = new Label[parameters.size()];
124:
125: for (IteratorOfProgramVariable it = parameters
126: .iterator(); it.hasNext();) {
127: ProgramVariable p = it.next();
128: Object val = so.getValueOfParameter(p);
129: if (val instanceof Term) {
130: Term t = (Term) val;
131: Label pvLabel = new Label(p.toString()
132: + " := "
133: + VisualDebugger.getVisualDebugger()
134: .prettyPrint(
135: SLListOfTerm.EMPTY_LIST
136: .append(t),
137: sos, so));
138:
139: //= new AttributeLabel(so, p, sos);
140: //System.out.println("AAAAAAAAAAA");
141: //pvLabel.addMouseListener(listener);
142:
143: pvLabel.setFont(Display.getCurrent()
144: .getSystemFont());
145: methodComp.add(pvLabel);
146: }
147: }
148: }
149:
150: } else {
151:
152: final ListOfTerm parameters = VisualDebugger
153: .getVisualDebugger().getSymbolicInputValuesAsList();
154:
155: this .paramColumns = new Label[parameters.size()];
156: method.getParameterDeclarationCount();
157: IteratorOfTerm it = parameters.iterator();
158: for (int i = 0; i < method.getParameterDeclarationCount(); i++) {
159: Term p = it.next();
160: Label pvLabel = // new Label(method.getParameterDeclarationAt(i).getVariables().getVariableSpecification(0).toString()
161: //+" := "+vd.prettyPrint(SLListOfTerm.EMPTY_LIST.append(p),sos,so));
162: //= new Label(p.toString()+" := "+VisualDebugger.getVisualDebugger().prettyPrint(SLListOfTerm.EMPTY_LIST.append(t),sos,so));
163: new AttributeLabel(so, (ProgramVariable) method
164: .getParameterDeclarationAt(i).getVariables()
165: .getVariableSpecification(0)
166: .getProgramVariable(), p, sos);
167: //if ()
168: if (!referenceSort(p.sort()))
169: pvLabel.addMouseListener(listener);
170: // System.out.println(" bb "+(ProgramVariable)method.getParameterDeclarationAt(i).getVariables().getVariableSpecification(0).getProgramVariable() + " "+p);
171:
172: pvLabel.setFont(Display.getCurrent().getSystemFont());
173: methodComp.add(pvLabel);
174:
175: }
176:
177: }
178:
179: methodComp.setBorder(new SeparatorBorder());
180:
181: }
182:
183: private boolean referenceSort(Sort s) {
184: JavaInfo info = vd.getMediator().getJavaInfo();
185: KeYJavaType kjt = info.getKeYJavaType(s);
186: // System.out.println("KJT "+kjt);
187: if (kjt == null)
188: return false;
189: if (kjt.getJavaType() instanceof ClassType)
190: return true;
191:
192: return false;
193: }
194:
195: private void prepare() {
196: ToolbarLayout layout = new ToolbarLayout(false);
197: layout.setStretchMinorAxis(true);
198: layout.setMinorAlignment(ToolbarLayout.ALIGN_CENTER);
199: setLayoutManager(layout);
200: setBorder(new LineBorder(ColorConstants.black, 1));
201: setBackgroundColor(ColorConstants.white);
202: setForegroundColor(ColorConstants.black);
203: setOpaque(true);
204: }
205:
206: private void createInstanceName() {
207: if (so.getType() instanceof ArrayType) {
208:
209: final String arrayType = ((ArrayType) so.getType())
210: .getAlternativeNameRepresentation().toString();
211: final String baseType = ((ArrayType) so.getType())
212: .getBaseType().getName().toString();
213: instanceName = new Label(baseType + "Array_" + so.getId()
214: + ":" + arrayType);
215:
216: } else
217: instanceName = new Label(so.getInstanceName() + ":"
218: + so.getType().getName());
219:
220: ((Label) instanceName)
221: .setTextAlignment(PositionConstants.CENTER);
222: instanceName.setFont(Display.getCurrent().getSystemFont());
223: instanceName.setFont(BOLD);
224: if (so.isStatic())
225: instanceName.setBorder(new MarginBorder(3, 5, 3, 5));
226: else
227: instanceName.setBorder(new UnderlineBorder());
228: instanceName.setBackgroundColor(instanceNameBackGround);
229: // instanceName.setForegroundColor(instanceNameBackGround);
230: instanceName.setOpaque(true);
231: // create column labels
232: }
233:
234: private void createCompAttributes() {
235: if (so.isUnknownObject()) {
236: compAttributes = new Figure();
237: Label qmLabel = new Label("?");
238: qmLabel.setFont(qmFont);
239: compAttributes.add(qmLabel);
240: ToolbarLayout qmlayout = new ToolbarLayout(false);
241: qmlayout.setMinorAlignment(ToolbarLayout.ALIGN_CENTER);
242: compAttributes.setBorder(new SeparatorBorder());
243: compAttributes.setLayoutManager(this .getLayoutManager());
244: return;
245:
246: }
247: SetOfProgramVariable attributes = so.getAttributes().union(
248: so.getAllModifiedPrimitiveAttributes());
249: attrColumns = new Label[attributes.size()];
250: compAttributes = new Figure();
251: int i = 0;
252: for (IteratorOfProgramVariable it = attributes.iterator(); it
253: .hasNext();) {
254: final ProgramVariable pv = it.next();
255: attrColumns[i] = new AttributeLabel(so, pv, sos);
256: attrColumns[i].addMouseListener(listener);
257: compAttributes.add(attrColumns[i]);
258: i++;
259: }
260:
261: //add ref attributes that are null
262: final SetOfProgramVariable pvs = so.getNonPrimAttributes();
263: for (IteratorOfProgramVariable it = pvs.iterator(); it
264: .hasNext();) {
265: final ProgramVariable pv = it.next();
266: if (so.getAssociationEnd(pv).isNull()) {
267: final Label l = new Label(pv.getProgramElementName()
268: .getProgramName()
269: + " := null");
270: l.setFont(Display.getCurrent().getSystemFont());
271: compAttributes.add(l);
272: }
273:
274: }
275:
276: // column labels are placed in separate compartment
277:
278: compAttributes.setLayoutManager(new ToolbarLayout(false));
279: compAttributes.setBorder(new SeparatorBorder());
280:
281: }
282:
283: public SymbolicObject getSymbolicObject() {
284: return so;
285: }
286:
287: public class SeparatorBorder extends MarginBorder {
288:
289: boolean down = false;
290: private int lw = 1;
291:
292: SeparatorBorder() {
293: super (3, 5, 3, 5);
294: }
295:
296: SeparatorBorder(boolean down) {
297: this ();
298: this .down = down;
299: }
300:
301: SeparatorBorder(int lw) {
302: super (3, 5, 3, 5);
303: this .lw = lw;
304:
305: }
306:
307: public void paint(IFigure figure, Graphics graphics,
308: Insets insets) {
309: Rectangle where = getPaintRectangle(figure, insets);
310: graphics.setLineWidth(lw);
311: if (down) {
312: graphics.setLineWidth(2);
313: graphics.drawLine(where.getBottomLeft().getTranslated(
314: 0, -3), where.getBottomRight().getTranslated(0,
315: -3));
316: } else
317: graphics.drawLine(where.getTopLeft(), where
318: .getTopRight());
319:
320: }
321:
322: }
323:
324: public class UnderlineBorder extends MarginBorder {
325:
326: UnderlineBorder() {
327: super (3, 7, 3, 7);
328:
329: }
330:
331: public void paint(IFigure figure, Graphics graphics,
332: Insets insets) {
333: // Rectangle where = getPaintRectangle(figure, insets);
334: graphics.setLineWidth(2);
335: Label l = (Label) figure;
336: Rectangle tb = l.getTextBounds();
337:
338: Point left = tb.getBottomLeft().translate(0, 0);
339: Point right = tb.getBottomRight().translate(0, 0);
340: graphics.drawLine(left, right);
341:
342: //graphics.drawLine(where.getBottomLeft().getTranslated(0, -3), where.getBottomRight().getTranslated(0, -3));
343:
344: }
345:
346: }
347:
348: public class AttributeLabel extends Label {
349: private final SymbolicObject so;
350: private final ProgramVariable pv;
351: private boolean selected = false;
352: private Term valueterm;
353:
354: public AttributeLabel(SymbolicObject so, ProgramVariable pv,
355: LinkedList sos) {
356: super ();
357: this .so = so;
358: this .pv = pv;
359: String text = pv.getProgramElementName().getProgramName();
360: if (so.getAllModifiedPrimitiveAttributes().contains(pv)) {
361: text = text
362: + " := "
363: + VisualDebugger
364: .getVisualDebugger()
365: .prettyPrint(
366: SLListOfTerm.EMPTY_LIST
367: .append(so
368: .getValueTerm(pv)),
369: sos, so);
370: } else if (so.getValueOfParameter(pv) != null)
371: text = text
372: + " := "
373: + VisualDebugger
374: .getVisualDebugger()
375: .prettyPrint(
376: SLListOfTerm.EMPTY_LIST
377: .append(so
378: .getValueOfParameter(pv)),
379: sos, so);
380: setText(text);
381: setFont(Display.getCurrent().getSystemFont());
382: }
383:
384: public AttributeLabel(SymbolicObject so, ProgramVariable pv,
385: Term value, LinkedList sos) {
386: super ();
387: this .so = so;
388: this .pv = pv;
389: this .valueterm = value;
390: String text = pv.getProgramElementName().getProgramName();
391: text = text
392: + " := "
393: + VisualDebugger.getVisualDebugger().prettyPrint(
394: value, sos, so);
395: setText(text);
396: setFont(Display.getCurrent().getSystemFont());
397: }
398:
399: public ProgramVariable getPv() {
400: return pv;
401: }
402:
403: public SymbolicObject getSo() {
404: return so;
405: }
406:
407: public void setSelected(boolean value) {
408: this .selected = value;
409: if (selected)
410: this .setForegroundColor(ColorConstants.blue);
411: else
412: this .setForegroundColor(null);
413: repaint();
414: }
415:
416: public Term getValueterm() {
417: return valueterm;
418: }
419:
420: }
421:
422: }
|