+// Returns the total height of the paper, including margins and
+// space for the header/footer. This is an upper bound on
+// page_height, and it doesn't depend on the current page.
+Real
+Page_breaking::paper_height () const
+{
+ return paper_height_;
+}
+