Idris2Doc : Text.Measure

Text.Measure

(source)
Measuring the visible bounds of text is incredibly hard
and tons of material have been written about this.

In this module, we take a pragmatic approach that produces
reasonable results without having to load and parse font files.
The drawback of this: The steps described below have to be repeated
for every new font we'd like to support.

A detailed introduction to typography and how fonts are specified
can be found [here](https://learn.microsoft.com/en-us/typography/opentype/spec/otff).

In general, we need to know the height and width of a piece of printed text
to properly align it with the rest of the drawing.

Text height:
  there are different types of "height" when it comes to text, and I won't go
  into the details here. Suffice to say that we are interested in vertically aligning
  atom labels, charges, implicit hydrogen count and mass numbers in a
  way that feels natural. For this, wir are mostly interested in "capHeight" of
  a font: The height of capital letters (without descenders). This, together
  with the Em-square size can be read from font files.

Text width:
  While computing the height of a piece of text is non-trivial, computing its
  width is insane. Every glyph has its own specific width, sometimes depending
  on its neighbouring glyphs (see ligatures and kerning). Fortunately, there
  is a quite simple method to get good approximations without being overly
  complicated. It is described on [stackoverflow](https://stackoverflow.com/questions/16007743/roughly-approximate-the-width-of-a-string-of-text-in-python)
  We use Python (because it has support for almost everything) to parse
  the true type font file we are interested in and generate a dictionary
  of the glyphs and their widths we are interested in. Using this to compute
  the width of a piece of text at a given font size is efficient and simple
  but not perfectly exact because it ignores kerning. It also requires large
  dictionaries if we want to support lots of unicode characters.

Note: The Python script used to extract the glyph widths can be found in the
      `resources` directory.

Definitions

recordTextDims : Type
  Metrics of a piece of text.

Totality: total
Visibility: public export
Constructor: 
TD : Double->Double->Double->TextDims

Projections:
.capHeight : TextDims->Double
.lineHeight : TextDims->Double
.txtWidth : TextDims->Double
.lineHeight : TextDims->Double
Totality: total
Visibility: public export
lineHeight : TextDims->Double
Totality: total
Visibility: public export
.capHeight : TextDims->Double
Totality: total
Visibility: public export
capHeight : TextDims->Double
Totality: total
Visibility: public export
.txtWidth : TextDims->Double
Totality: total
Visibility: public export
txtWidth : TextDims->Double
Totality: total
Visibility: public export
recordMeasure : Type
  Utility for measuring text metrics.

Totality: total
Visibility: public export
Constructor: 
M : (Nat->String->String->TextDims) ->Measure

Projection: 
.measure : Measure->Nat->String->String->TextDims
.measure : Measure->Nat->String->String->TextDims
Totality: total
Visibility: public export
measure : Measure->Nat->String->String->TextDims
Totality: total
Visibility: public export
defaultMeasure : Measure
  This is a primitive but efficient implementation of `Measure`, which
is described in the module docs. A more exact implementation could
make use of a browser canvas and use text metrics from the DOM, but
this is not available when we are not drawing molecules in the browser.

This implementation assumes a typical roman font similar to Arial.
It is based on the metrics of "Liberation Sans", which should have the
same layout as Arial or Helvetica.

About magic numbers: 2048 is the Em square size, 1409 the cap height,
307 the line height. These have to be multiplied with the font size.
Text widths are approxiamted by summing up glyph width stored in a
dictionary.

Totality: total
Visibility: export