- if (kind_ == DEFSKIP)
- default_skip = bv->buffer()->params.getDefSkip().inPixels(bv);
-
- // Height of a normal line in pixels (zoom factor considered)
- int height = default_height; // [pixels]
-
- // Zoom factor specified by user in percent
- double const zoom = lyxrc.zoom / 100.0; // [percent]
-
- // DPI setting for monitor: pixels/inch
- double const dpi = lyxrc.dpi; // screen resolution [pixels/inch]
-
- // We want the result in pixels
- double result;
- double value;
-