1 package fr.ove.openmath.jome.ctrlview.bidim;
2
3 import java.awt.*;
4 import java.util.*;
5 import fr.ove.openmath.jome.ctrlview.bidim.Display;
6 import fr.ove.openmath.jome.ctrlview.bidim.DisplayLayout;
7 import fr.ove.openmath.jome.ctrlview.bidim.selection.events.SelectionEvent;
8 import fr.ove.openmath.jome.model.*;
9 import fr.ove.utils.FontInfo;
10
11 /***
12 * Layout manager that lays the display of the absolute value operator
13 *
14 * @author © 1999 DIRAT Laurent
15 * @version 2.0 15/12/1999
16 */
17 public class AbsoluteLayout extends EnclosingLayout {
18 /***
19 * Returns the opening
20 */
21 public SymbolDisplay createOpening() {
22 SymbolDisplay bar = new SymbolDisplay(displayToLay.getGraphicContext(), new Bar());
23
24 bar.setIsSymbolOperatorDisplay(true);
25 return bar;
26 }
27
28 /***
29 * Returns the closing
30 */
31 public SymbolDisplay createClosing() {
32 return createOpening();
33 }
34
35 /***
36 * Computes the size of the display according to its children size (if any),
37 * and its different attributes.
38 * @return the size of the display.
39 */
40 public Dimension computeAttributes() {
41 Display display = null;
42
43
44 display = (Display) displayToLay.getComponent(2);
45 display.setSize(display.getPreferredSize());
46
47 display.setShiftX(2);
48
49 int width = display.getShiftX() + display.getWidth();
50 int height = display.getShiftY() + display.getHeight();
51 int ascent = display.getAscent();
52 int descent = display.getDescent();
53 int thickness = FontInfo.getLineThickness(displayToLay, displayToLay.getFont());
54
55
56
57 SymbolDisplay opening = getOpening();
58 Bar bar = (Bar) opening.getSymbol();
59 bar.setHeight(display.getHeight());
60 bar.setWidth(thickness);
61 bar.setAscent(ascent);
62 bar.setDescent(descent);
63 opening.setComputeAttributes(true);
64 opening.invalidate();
65 opening.setSize(opening.getPreferredSize());
66
67 width += opening.getWidth();
68
69 SymbolDisplay closing = getClosing();
70 bar = (Bar) closing.getSymbol();
71 bar.setHeight(display.getHeight());
72 bar.setWidth(thickness);
73 bar.setAscent(ascent);
74 bar.setDescent(descent);
75 closing.setComputeAttributes(true);
76 closing.invalidate();
77 closing.setSize(closing.getPreferredSize());
78
79 closing.setShiftX(2);
80
81 width += closing.getShiftX() + closing.getWidth();
82
83 displayToLay.setAscent(ascent);
84 displayToLay.setDescent(descent);
85 displayToLay.setSize(width, height);
86
87 displayToLay.setComputeAttributes(false);
88
89
90 closing.setShiftX(width - 2*closing.getWidth());
91
92 display.setShiftX(display.getShiftX() - closing.getShiftX() - closing.getWidth());
93
94 return new Dimension(width, height);
95 }
96 }