2021-11-18 20:09:09 +01:00
|
|
|
type glue =
|
|
|
|
|
{glen : float;
|
2021-11-20 00:21:37 +01:00
|
|
|
gstretch : float}
|
2021-11-18 20:09:09 +01:00
|
|
|
|
2021-11-18 23:48:25 +01:00
|
|
|
type element =
|
2021-11-20 00:21:37 +01:00
|
|
|
Text of string
|
2021-11-18 20:09:09 +01:00
|
|
|
| HGlue of glue
|
|
|
|
|
| VGlue of glue
|
|
|
|
|
| NewLine
|
|
|
|
|
| NewPage
|
2021-11-20 00:21:37 +01:00
|
|
|
| Font of (Pdftext.font * float)
|
2021-11-18 20:09:09 +01:00
|
|
|
|
2021-11-18 23:48:25 +01:00
|
|
|
type t = element list
|
2021-11-16 02:42:17 +01:00
|
|
|
|
2021-11-18 23:48:25 +01:00
|
|
|
val typeset : float -> float -> float -> float -> Pdfpaper.t -> Pdf.t -> t -> Pdfpage.t list
|
