summary |
shortlog |
log |
commit | commitdiff |
tree
raw |
patch |
inline | side by side (from parent 1:
68614e9)
This spacing was wrongly removed at
361bd53b as part of the
introduction of proper spacing btween elements, but it only introduces
some breathing space around the delimiters. This will not be necessary
anymore when/if we use proper delimiters from the cmex10 font.
dw_ = 8;
if (dw_ < 4)
dw_ = 4;
dw_ = 8;
if (dw_ < 4)
dw_ = 4;
- dim.wid = dim0.width() + 2 * dw_;
+ dim.wid = dim0.width() + 2 * dw_ + 2 * mathed_thinmuskip(mi.base.font);
dim.asc = max(a0, d0) + h0;
dim.des = max(a0, d0) - h0;
}
dim.asc = max(a0, d0) + h0;
dim.des = max(a0, d0) - h0;
}
Changer dummy = pi.base.changeEnsureMath();
Dimension const dim = dimension(*pi.base.bv);
int const b = y - dim.asc;
Changer dummy = pi.base.changeEnsureMath();
Dimension const dim = dimension(*pi.base.bv);
int const b = y - dim.asc;
- cell(0).draw(pi, x + dw_, y);
- mathed_draw_deco(pi, x, b, dw_, dim.height(), left_);
- mathed_draw_deco(pi, x + dim.width() - dw_,
+ int const skip = mathed_thinmuskip(pi.base.font);
+ cell(0).draw(pi, x + dw_ + skip, y);
+ mathed_draw_deco(pi, x + skip / 2, b, dw_, dim.height(), left_);
+ mathed_draw_deco(pi, x + dim.width() - dw_ - skip / 2,
b, dw_, dim.height(), right_);
}
b, dw_, dim.height(), right_);
}