e.inset->drawBackground(pi_, x1, yo_);
e.inset->drawSelection(pi_, x1, yo_);
e.inset->draw(pi_, x1, yo_);
+ paintTextDecoration(e);
// Restore full_repaint status.
pi_.full_repaint = pi_full_repaint;
}
-/** Check if the current paragraph is the last paragraph in a
- proof environment */
-static int getEndLabel(pit_type p, Text const & text)
-{
- ParagraphList const & pars = text.paragraphs();
- pit_type pit = p;
- depth_type par_depth = pars[p].getDepth();
- while (pit != pit_type(pars.size())) {
- Layout const & layout = pars[pit].layout();
- int const endlabeltype = layout.endlabeltype;
-
- if (endlabeltype != END_LABEL_NO_LABEL) {
- if (p + 1 == pit_type(pars.size()))
- return endlabeltype;
-
- depth_type const next_depth =
- pars[p + 1].getDepth();
- if (par_depth > next_depth ||
- (par_depth == next_depth && layout != pars[p + 1].layout()))
- return endlabeltype;
- break;
- }
- if (par_depth == 0)
- break;
- pit = text.outerHook(pit);
- if (pit != pit_type(pars.size()))
- par_depth = pars[pit].getDepth();
- }
- return END_LABEL_NO_LABEL;
-}
-
-
void RowPainter::paintLast() const
{
- int const endlabel = getEndLabel(row_.pit(), text_);
-
- // paint imaginary end-of-paragraph character
-
- Change const & change = par_.lookupChange(par_.size());
- if (change.changed()) {
- FontMetrics const & fm =
- theFontMetrics(pi_.base.bv->buffer().params().getFont());
- int const length = fm.maxAscent() / 2;
- Color col = change.color();
-
- pi_.pain.line(int(x_) + 1, yo_ + 2, int(x_) + 1, yo_ + 2 - length, col,
- Painter::line_solid, 3);
-
- if (change.deleted()) {
- pi_.pain.line(int(x_) + 1 - length, yo_ + 2, int(x_) + 1 + length,
- yo_ + 2, col, Painter::line_solid, 3);
- } else {
- pi_.pain.line(int(x_) + 1 - length, yo_ + 2, int(x_) + 1,
- yo_ + 2, col, Painter::line_solid, 3);
- }
- }
-
- // draw an endlabel
-
+ int const endlabel = text_.getEndLabel(row_.pit());
switch (endlabel) {
case END_LABEL_BOX:
case END_LABEL_FILLED_BOX: {
case Row::INSET:
paintInset(e);
- paintTextDecoration(e);
break;
case Row::SPACE: