Keep the useful parts of reverted commits

Keep from 907f0207 the introduction of BufferView::top/bottomMargin()
and the setting of the top/bottom margin of the document. The
difference is that the extra height is still added to the relevant
rows, and not only to the paragraph metrics.

Keep from f41ca959 the reduction of top/bottom margin for Adv F&R
workareas.

diff --git a/src/BufferView.cpp b/src/BufferView.cpp
index 6063168380f7236060fabf7a67165da29e7f95f3..0025277e5330406ae1d33eda3113ebf668c3884b 100644 (file)
--- a/src/BufferView.cpp
+++ b/src/BufferView.cpp
@@ -349,6 +349,20 @@ int BufferView::leftMargin() const
 }
 
 
+int BufferView::topMargin() const
+{
+       // Original value was 20px at 100dpi. For internal buffers like in
+       // advanced search and replace, a value of 5px is enough.
+       return zoomedPixels(buffer().isInternal() ? 5 : 20);
+}
+
+
+int BufferView::bottomMargin() const
+{
+       return topMargin();
+}
+
+
 int BufferView::inPixels(Length const & len) const
 {
        Font const font = buffer().params().getFont();

diff --git a/src/BufferView.h b/src/BufferView.h
index 462bf0e9d606e85cb8a1a8c0c4bc6b981f4f58b7..830c2d738d1d3d52e2b411839b279a3df8b2f420 100644 (file)
--- a/src/BufferView.h
+++ b/src/BufferView.h
@@ -102,9 +102,12 @@ public:
 
        /// right margin
        int rightMargin() const;
-
        /// left margin
        int leftMargin() const;
+       /// top margin
+       int topMargin() const;
+       /// bottom margin
+       int bottomMargin() const;
 
        docstring const & searchRequestCache() const;
        void setSearchRequestCache(docstring const & text);

diff --git a/src/TextMetrics.cpp b/src/TextMetrics.cpp
index d3242f9ea4ffbb1b6d88a4eed5f898383307e52a..3154f0d6034804b00fdfccee106eb93b76d1f7dd 100644 (file)
--- a/src/TextMetrics.cpp
+++ b/src/TextMetrics.cpp
@@ -581,37 +581,29 @@ bool TextMetrics::redoParagraph(pit_type const pit, bool const align_rows)
                }
        }
 
+       // The space above and below the paragraph.
+       int top = parTopSpacing(pit);
+       int bottom = parBottomSpacing(pit);
+
+       // Top and bottom margin of the document (only at top-level)
        // FIXME: It might be better to move this in another method
        // specially tailored for the main text.
-       // Top and bottom margin of the document (only at top-level)
        if (text_->isMainText()) {
-               // original value was 20px, which is 0.2in at 100dpi
-               int const margin = bv_->zoomedPixels(20);
-               if (pit == 0) {
-                       pm.rows().front().dim().asc += margin;
-                       /* coverity thinks that we should update pm.dim().asc
-                        * below, but all the rows heights are actually counted as
-                        * part of the paragraph metric descent see loop above).
-                        */
-                       // coverity[copy_paste_error]
-                       pm.dim().des += margin;
-               }
-               ParagraphList const & pars = text_->paragraphs();
-               if (pit + 1 == pit_type(pars.size())) {
-                       pm.rows().back().dim().des += margin;
-                       pm.dim().des += margin;
+               if (pit == 0)
+                       top += bv_->topMargin();
+               if (pit + 1 == pit_type(text_->paragraphs().size())) {
+                       bottom += bv_->bottomMargin();
                }
        }
 
-       // The space above and below the paragraph.
-       int const top = parTopSpacing(pit);
+       // Add the top/bottom space to rows and paragraph metrics
        pm.rows().front().dim().asc += top;
-       int const bottom = parBottomSpacing(pit);
        pm.rows().back().dim().des += bottom;
        pm.dim().des += top + bottom;
 
-       pm.dim().asc += pm.rows()[0].ascent();
-       pm.dim().des -= pm.rows()[0].ascent();
+       // Move the pm ascent to be the same as the first row ascent
+       pm.dim().asc += pm.rows().front().ascent();
+       pm.dim().des -= pm.rows().front().ascent();
 
        changed |= old_dim.height() != pm.dim().height();