- // the labels at the top of an environment.
- // More or less for bibliography
- } else if (is_seq &&
- (layout->labeltype == LABEL_TOP_ENVIRONMENT ||
- layout->labeltype == LABEL_BIBLIO ||
- layout->labeltype == LABEL_CENTERED_TOP_ENVIRONMENT)) {
- Font font = getLabelFont();
- if (!par_.getLabelstring().empty()) {
- docstring const str = par_.getLabelstring();
- double spacing_val = 1.0;
- if (!parparams.spacing().isDefault())
- spacing_val = parparams.spacing().getValue();
- else
- spacing_val = buffer.params().spacing().getValue();
-
- FontMetrics const & fm = theFontMetrics(font);
-
- int const labeladdon = int(fm.maxHeight()
- * layout->spacing.getValue() * spacing_val);
-
- int maxdesc =
- int(fm.maxDescent() * layout->spacing.getValue() * spacing_val
- + (layout->labelbottomsep * defaultRowHeight()));
-
- double x = x_;
- if (layout->labeltype == LABEL_CENTERED_TOP_ENVIRONMENT) {
- if (is_rtl)
- x = leftMargin();
- x += (width_ - text_metrics_.rightMargin(pm_) - leftMargin()) / 2;
- x -= fm.width(str) / 2;
- } else if (is_rtl) {
- x = width_ - leftMargin() - fm.width(str);
- }
- pain_.text(int(x), yo_ - maxdesc - labeladdon, str, font);
+ int const labeladdon = int(fm.maxHeight() * layout.spacing.getValue() * spacing_val);
+
+ int const maxdesc = int(fm.maxDescent() * layout.spacing.getValue() * spacing_val)
+ + int(layout.parsep) * defaultRowHeight();
+
+ if (is_rtl) {
+ x = width_ - leftMargin() -
+ fm.width(str);
+ }
+
+ pi_.pain.text(int(x), yo_ - maxdesc - labeladdon, str, font);
+ } else {
+ if (is_rtl) {
+ x = width_ - leftMargin()
+ + fm.width(layout.labelsep);
+ } else {
+ x = x_ - fm.width(layout.labelsep)
+ - fm.width(str);
+ }
+
+ pi_.pain.text(int(x), yo_, str, font);
+ }
+}
+
+
+void RowPainter::paintTopLevelLabel()
+{
+ BufferParams const & bparams = pi_.base.bv->buffer().params();
+ bool const is_rtl = text_.isRTL(par_);
+ ParagraphParameters const & pparams = par_.params();
+ Layout const & layout = par_.layout();
+ FontInfo const font = labelFont();
+ docstring const str = par_.labelString();
+ if (str.empty())
+ return;
+
+ double spacing_val = 1.0;
+ if (!pparams.spacing().isDefault())
+ spacing_val = pparams.spacing().getValue();
+ else
+ spacing_val = bparams.spacing().getValue();
+
+ FontMetrics const & fm = theFontMetrics(font);
+
+ int const labeladdon = int(fm.maxHeight()
+ * layout.spacing.getValue() * spacing_val);
+
+ int maxdesc =
+ int(fm.maxDescent() * layout.spacing.getValue() * spacing_val
+ + (layout.labelbottomsep * defaultRowHeight()));
+
+ double x = x_;
+ if (layout.labeltype == LABEL_CENTERED_TOP_ENVIRONMENT) {
+ if (is_rtl)
+ x = leftMargin();
+ x += (width_ - text_metrics_.rightMargin(pm_) - leftMargin()) / 2;
+ x -= fm.width(str) / 2;
+ } else if (is_rtl) {
+ x = width_ - leftMargin() - fm.width(str);
+ }
+ pi_.pain.text(int(x), yo_ - maxdesc - labeladdon, str, font);
+}
+
+/** 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;