125 |
|
|
126 |
try |
try |
127 |
{ |
{ |
128 |
text = elem.getDocument().getText(elem.getStartOffset(), |
text = elem.getDocument().getText(elem.getStartOffset(), |
129 |
elem.getEndOffset()); |
elem.getEndOffset()); |
130 |
} |
} |
131 |
catch (BadLocationException e) |
catch (BadLocationException e) |
132 |
{ |
{ |
133 |
// This should never happen. |
assert false : e.toString(); |
134 |
text = ""; |
text = ""; |
135 |
} |
} |
136 |
|
|
137 |
return fm.stringWidth(text) + 30; |
return fm.stringWidth(text); |
138 |
} |
} |
139 |
|
|
140 |
public int getResizeWeight(int axis) |
public int getResizeWeight(int axis) |