commit 283ac91aa739215fc084d57cdec62a27eb5f2f30
Author: Jean-Marc Lasgouttes <[email protected]>
Date: Wed Apr 3 11:06:43 2019 +0200
Put end label on own row after display inset
This corresponds to what is done on display. The same should be done
for start label too (e.g. beginning of a proof), but this requires more
work.
This required to move the static function getEndLabel to Text.
Fixes bug #11536.
---
src/RowPainter.cpp | 34 +---------------------------------
src/Text.cpp | 29 +++++++++++++++++++++++++++++
src/Text.h | 2 ++
src/TextMetrics.cpp | 12 +++++++++---
4 files changed, 41 insertions(+), 36 deletions(-)
diff --git a/src/RowPainter.cpp b/src/RowPainter.cpp
index a88ac2a..a486c0e 100644
--- a/src/RowPainter.cpp
+++ b/src/RowPainter.cpp
@@ -472,41 +472,9 @@ void RowPainter::paintTopLevelLabel() const
}
-/** 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_);
+ int const endlabel = text_.getEndLabel(row_.pit());
switch (endlabel) {
case END_LABEL_BOX:
case END_LABEL_FILLED_BOX: {
diff --git a/src/Text.cpp b/src/Text.cpp
index c3c2108..98cedcc 100644
--- a/src/Text.cpp
+++ b/src/Text.cpp
@@ -288,6 +288,35 @@ Font const Text::outerFont(pit_type par_offset) const
}
+int Text::getEndLabel(pit_type p) const
+{
+ 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 = outerHook(pit);
+ if (pit != pit_type(pars_.size()))
+ par_depth = pars_[pit].getDepth();
+ }
+ return END_LABEL_NO_LABEL;
+}
+
+
static void acceptOrRejectChanges(ParagraphList & pars,
BufferParams const & bparams, Text::ChangeOp op)
{
diff --git a/src/Text.h b/src/Text.h
index f3cd844..dc96d83 100644
--- a/src/Text.h
+++ b/src/Text.h
@@ -345,6 +345,8 @@ public:
/// Get the font of the "environment" of paragraph \p par_offset in \p
pars.
/// All font changes of the paragraph are relative to this font.
Font const outerFont(pit_type pit_offset) const;
+ /// Return the label type at the end of paragraph \c pit.
+ int getEndLabel(pit_type pit) const;
private:
/// The InsetText owner shall have access to everything.
diff --git a/src/TextMetrics.cpp b/src/TextMetrics.cpp
index 9bb116d..6ce580c 100644
--- a/src/TextMetrics.cpp
+++ b/src/TextMetrics.cpp
@@ -983,11 +983,17 @@ bool TextMetrics::breakRow(Row & row, int const
right_margin) const
Inset const * inset = 0;
if (par.isNewline(i) || par.isEnvSeparator(i)
|| (i + 1 < end && (inset = par.getInset(i + 1))
- && inset->display())
+ && inset->display())
|| (!row.empty() && row.back().inset
- && row.back().inset->display())) {
+ && row.back().inset->display())) {
row.flushed(true);
- need_new_row = par.isNewline(i);
+ // We will force a row creation after either
+ // - a newline;
+ // - a display inset followed by a end label.
+ need_new_row =
+ par.isNewline(i)
+ || (inset->display() && i + 1 == end
+ && text_->getEndLabel(row.pit()) !=
END_LABEL_NO_LABEL);
++i;
break;
}
